uu.seUppsala University Publications
Change search
Refine search result
1 - 27 of 27
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Brandauer, Stephan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Castegren, Elias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Fernandez-Reyes, Kiko
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Johnsen, Einar Broch
    Univ Oslo, Dept Informat, N-0316 Oslo, Norway..
    Pun, Ka I.
    Univ Oslo, Dept Informat, N-0316 Oslo, Norway..
    Tarifa, S. Lizeth Tapia
    Univ Oslo, Dept Informat, N-0316 Oslo, Norway..
    Wrigstad, Tobias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Yang, Albert Mingkun
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parallel Objects for Multicores: A Glimpse at the Parallel Language ENCORE2015In: Formal Methods for Multicore Programming, 2015, p. 1-56Conference paper (Refereed)
    Abstract [en]

    The age of multi-core computers is upon us, yet current programming languages, typically designed for single-core computers and adapted post hoc for multi-cores, remain tied to the constraints of a sequential mindset and are thus in many ways inadequate. New programming language designs are required that break away from this old-fashioned mindset. To address this need, we have been developing a new programming language called Encore, in the context of the European Project UpScale. The paper presents a motivation for the Encore language, examples of its main constructs, several larger programs, a formalisation of its core, and a discussion of some future directions our work will take. The work is ongoing and we started more or less from scratch. That means that a lot of work has to be done, but also that we need not be tied to decisions made for sequential language designs. Any design decision can be made in favour of good performance and scalability. For this reason, Encore offers an interesting platform for future exploration into object-oriented parallel programming.

  • 2.
    Brandauer, Stephan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Wrigstad, Tobias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Disjointness Domains for Fine-Grained Aliasing2015Conference paper (Refereed)
    Abstract [en]

    Aliasing is crucial for supporting useful implementation patterns, but it makes reasoning about programs difficult. To deal with this problem, numerous type-based aliasing control mechanisms have been proposed, expressing properties such as uniqueness. Uniqueness, however, is black-and-white: either a reference is unique or it can be arbitrarily aliased; and global: excluding aliases throughout the entire system, making code brittle to changing requirements. Disjointness domains, a new approach to alias control, address this problem by enabling more graduations between uniqueness and arbitrary reference sharing. They allow expressing aliasing constraints local to a certain set of variables (either stack variables or fields) for instance that no aliasing occurs between variables within some set of variables but between such sets or the opposite, that aliasing occurs within that set but not between different sets. A hierarchy of disjointness domains controls the flow of references through a program, helping the programmer reason about disjointness and enforce local alias invariants. The resulting system supports fine-grained control of aliasing between both variables and objects, making aliasing explicit to programmers, compilers, and tooling. This paper presents a formal account of disjointness domains along with examples. Disjointness domains provide novel means of expressing may-alias kinds of constraints, which may prove useful in compiler optimisation and verification.

  • 3. Broch Johnsen, Einar
    et al.
    Owe, Olaf
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Bjørk, Joakim
    A formal model of service-oriented dynamic object groups2016In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 115–116, p. 3-22Article in journal (Refereed)
  • 4.
    Clarke, Dave
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Helvensteijn, Michiel
    Schaefer, Ina
    Abstract Delta Modelling2015In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 3, p. 482-527Article in journal (Refereed)
  • 5.
    Clarke, Dave
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Wrigstad, Tobias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Vats: A safe, reactive storage abstraction2016In: Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday / [ed] Ábrahám, Erika; Bonsangue, Marcello; Broch Johnsen, Einar, Springer, 2016, p. 140-154Chapter in book (Refereed)
  • 6.
    Daniels, Wilfried
    et al.
    Katholieke Univ Leuven, IMinds DistriNet, B-3001 Leuven, Belgium.
    Proença, José
    Katholieke Univ Leuven, IMinds DistriNet, B-3001 Leuven, Belgium; Univ Minho, HASLab INESC TEC, P-4719 Braga, Portugal.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Joosen, Wouter
    Katholieke Univ Leuven, IMinds DistriNet, B-3001 Leuven, Belgium.
    Hughes, Danny
    Katholieke Univ Leuven, IMinds DistriNet, B-3001 Leuven, Belgium.
    Refraction: Low-cost management of reflective meta-data in pervasive component-based applications2015In: Proc. 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, New York: ACM Press, 2015, p. 27-36Conference paper (Refereed)
    Abstract [en]

    This paper proposes the concept of refraction, a principled means to lower the cost of managing reflective meta-data for pervasive systems. While prior work has demonstrated the bene fits of reflective component-based middleware for building open and reconfigurable applications, the cost of using remote reflective operations remains high. Refractive components address this problem by selectively augmenting application data flows with their reflective meta-data, which travels at low cost to reflective pools, which serve as loci of inspection and control for the distributed application. Additionally reflective policies are introduced, providing a mechanism to trigger reconfigurations based on incoming reflective meta-data. We evaluate the performance of refraction in a case-study of automatic con figuration repair for a real-world pervasive application. We show that refraction reduces network overhead in comparison to the direct use of reflective operations while not increasing development overhead. To enable further experimentation with the concept of refraction, we provide RxCom, an open-source refractive component model and supporting runtime environment.

  • 7. de Boer, Frank
    et al.
    Broch Johnsen, Einar
    Olso University.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Drossopoulou, Sophia
    Imperial College London.
    Yoshida, Nobuko
    Imperial College London.
    Wrigstad, Tobias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Scaling Future Software: The Manycore Challenge2014Other (Other (popular science, discussion, etc.))
    Abstract [en]

    Existing software cannot benefit from the revolutionary potential increases in computational power provided by manycore chips unless their design and code are polluted by an unprecedented amount of low-level, fine-grained concurrency detail. As a consequence, the advent of manycore chips threatens to make current main-stream programming approaches obsolete, and thereby, jeopardizes the benefits gained from the last 20 years of development in industrial software engineering. In this article we put forward an argument for a fundamental breakthrough in how parallelism and concurrency are integrated into the software of the future.

  • 8.
    Fernandez-Reyes, Kiko
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Affine killing: Semantics for stopping the ParT2017In: Proc. 2nd International Workshop on Type-Driven Development, New York: ACM Press, 2017Conference paper (Refereed)
    Abstract [en]

    Speculative, parallel abstractions allow that, once a result is computed, the remaining (unnecessary) speculative computations can be safely stopped. However, it is difficult to know when it is safe to stop an ongoing computation. This paper presents a refinement of the parallel speculative ParT abstraction with an affine type system that allows in-place updates, and killing speculative computations using thread-local reasoning. There is ongoing work to prove the soundness of the calculus and implement it in the Encore language.

  • 9.
    Fernandez-Reyes, Kiko
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Castegren, Elias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Vo, Huu-Phuc
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Forward to a Promising Future2018In: Conference proceedings COORDINATION 2018, 2018Conference paper (Refereed)
    Abstract [en]

    In many actor-based programming models, asynchronous method calls communicate their results using futures, where the fulfilment occurs under-the-hood. Promises play a similar role to futures, except that they must be explicitly created and explicitly fulfilled; this makes promises more flexible than futures, though promises lack fulfilment guarantees: they can be fulfilled once, multiple times or not at all. Unfortunately, futures are too rigid to exploit many available concurrent and parallel patterns. For instance, many computations block on a future to get its result only to return that result immediately (to fulfil their own future). To make futures more flexible, we explore a construct, forward, that delegates the responsibility for fulfilling the current implicit future to another computation. Forward reduces synchronisation and gives futures promise-like capabilities. This paper presents a formalisation of the forward construct, defined in a high-level source language, and a compilation strategy from the high-level language to a low-level, promised-based target language. The translation is shown to preserve semantics. Based on this foundation, we describe the implementation of forward in the parallel, actor-based language Encore, which compiles to C.

  • 10.
    Fernandez-Reyes, Kiko
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    McCain, Daniel S.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    ParT: An asynchronous parallel abstraction for speculative pipeline computations2016In: Coordination Models and Languages / [ed] Lafuente, AL; Proenca, J, Springer, 2016, p. 101-120Conference paper (Refereed)
    Abstract [en]

    The ubiquity of multicore computers has forced programming language designers to rethink how languages express parallelism and concurrency. This has resulted in new language constructs and new combinations or revisions of existing constructs. In this line, we extended the programming languages Encore (actor-based), and Clojure (functional) with an asynchronous parallel abstraction called ParT, a data structure that can dually be seen as a collection of asynchronous values (integrating with futures) or a handle to a parallel computation, plus a collection of combinators for manipulating the data structure. The combinators can express parallel pipelines and speculative parallelism. This paper presents a typed calculus capturing the essence of ParT, abstracting away from details of the Encore and Clojure programming languages. The calculus includes tasks, futures, and combinators similar to those of Orc but implemented in a non-blocking fashion. Furthermore, the calculus strongly mimics how ParT is implemented, and it can serve as the basis for adaptation of ParT into different languages and for further extensions.

  • 11. Jongmans, Sung-Shik T. Q.
    et al.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Proença, José
    A procedure for splitting data-aware processes and its application to coordination2016In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 115–116, p. 47-78Article in journal (Refereed)
  • 12.
    Larmuseau, Adriaan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Formalizing a secure foreign function interface2015In: Software Engineering and Formal Methods, Springer, 2015, p. 215-230Conference paper (Refereed)
    Abstract [en]

    Many high-level functional programming languages provide programmers with the ability to interoperate with untyped and low-level languages such as C and assembly. Research into the security of such interoperation has generally focused on a closed world scenario, one where both the high-level and low-level code are defined and analyzed statically. In practice, however, components are sometimes linked in at run-time through malicious means. In this paper we formalize an operational semantics that securely combines MiniML, a light-weight ML, with a model of a low-level attacker, without relying on any static checks on the attacker. We prove that the operational semantics are secure by establishing that they preserve and reflect the equivalences of MiniML. To that end a notion of bisimulation for the interaction between the attacker and MiniML is developed.

  • 13.
    Larmuseau, Adriaan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Patrignani, Marco
    Katholieke Univ Leuven, iMinds Distrinet, Leuven, Belgium.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A high-level model for an assembly language attacker by means of reflection2015In: Dependable Software Engineering: Theories, Tools, and Applications, Springer, 2015, p. 168-182Conference paper (Refereed)
    Abstract [en]

    Many high-level functional programming languages are compiled to or interoperate with, low-level languages such as C and assembly. Research into the security of these compilation and interoperation mechanisms often makes use of high-level attacker models to simplify formalisations. In practice, however, the validity of such high-level attacker models is frequently called into question. In this paper we formally prove that a light-weight ML equipped with a reflection operator can serve as an accurate model for malicious assembly language programs, when reasoning about the security threats such an attacker model poses to the abstractions of ML programs that reside within a protected memory space. The proof proceeds by relating bisimulations over the assembly language attacker and the high-level attacker.

  • 14.
    Larmuseau, Adriaan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Patrignani, Marco
    Katholieke Univ Leuven, IMinds Distrinet, Leuven, Belgium.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A secure compiler for ML modules2015In: Programming Languages and Systems: APLAS 2015, Springer, 2015, p. 29-48Conference paper (Refereed)
    Abstract [en]

    Many functional programming languages compile to low-level languages such as C or assembly. Numerous security properties of those compilers, however, apply only when the compiler compiles whole programs. This paper presents a compilation scheme that securely compiles a standalone module of ModuleML, a light-weight version of an ML with modules, into untyped assembly. The compilation scheme is secure in that it reflects the abstractions of a ModuleML module, for every possible piece of assembly code that it interacts with. This is achieved by isolating the compiled module through a low-level memory isolation mechanism and by dynamically type checking its interactions. We evaluate an implementation of the compiler on relevant test scenarios.

  • 15.
    Larmuseau, Adriaan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Patrignani, Marco
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Implementing a secure abstract machine2016In: Proc. 31st ACM Symposium on Applied Computing, New York: ACM Press, 2016, p. 2041-2048Conference paper (Refereed)
    Abstract [en]

    Abstract machines are both theoretical models used to study language properties and practical models of language implementations. As with all language implementations, abstract machines are subject to security violations by the context in which they reside. This paper presents the implementation of an abstract machine for ML that preserves the abstractions of ML, in possibly malicious, low-level contexts. To guarantee this security result, we make use of a low-level memory isolation mechanism and derive the formalisation of the machine through a methodology, whose every step is accompanied by formal properties that ensure that the step has been carried out properly. We provide an implementation of the abstract machine and analyse its performance.

  • 16.
    Larmuseau, Adriaan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Patrignani, Marco
    KULeuven.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Operational Semantics for Secure Interoperation2014In: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security, 2014Conference paper (Refereed)
    Abstract [en]

    Modern software systems are commonly programmed in multiple languages. Research into the security and correctness of such multi-language programs has generally relied on static methods that check both the individual components as well as the interoperation between them. In practice, however, components are sometimes linked in at run-time through malicious means. In this paper we introduce a technique to specify operational semantics that securely combine an abstraction-rich language with a model of an arbitrary attacker, without relying on any static checks. The resulting operational semantics, instead, lifts a proven memory isolation mechanism into the resulting multi-language system. We establish the security benefits of our technique by proving that the obtained multi-language system preserves and reflects the equivalences of the abstraction-rich language. To that end a notion of bisimilarity for this new type of multi-language system is developed.

  • 17.
    Muschevici, Radu
    et al.
    KU Leuven, Belgium.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Proenca, José
    KU Leuven, Belgium.
    Executable modelling of dynamic software product lines in the ABS language2013In: Proc. 5th International Workshop on Feature-Oriented Software Development, New York: ACM Press, 2013, p. 17-24Conference paper (Refereed)
    Abstract [en]

    Dynamic software product lines (DSPLs) combine the advantages of traditional SPLs, such as an explicit variability model connected to an integrated repository of reusable code artefacts, with the ability to exploit a system's variability at runtime. When a system needs to adapt, for example to changes in operational environment or functional requirements, DSPL systems are capable of adapting their behaviour dynamically, thus avoiding the need to halt, recompile and redeploy. The field of DSPL engineering is still in formation and general-purpose DSPL development languages and tools are rare. In this paper we introduce a language and execution environment for developing and running dynamic SPLs. Our work builds on ABS, a language and integrated development environment with dedicated support for implementing static software product lines. Our ABS extension advances the scope of ABS to dynamic SPL engineering. Systems developed using ABS are compiled to Java, and are thus executable on a wide range of platforms.

  • 18.
    Muschevici, Radu
    et al.
    Tech Univ Darmstadt, Dept Comp Sci, Darmstadt, Germany.
    Proença, José
    Katholieke Univ Leuven, iMinds Distrinet, Leuven, Belgium; Univ Minho, HASLab INESC TEC, Braga, Portugal.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. Katholieke Univ Leuven, iMinds Distrinet, Leuven, Belgium.
    Feature Nets: Behavioural modelling of software product lines2016In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 15, no 4, p. 1181-1206Article in journal (Refereed)
    Abstract [en]

    Software product lines (SPLs) are diverse systems that are developed using a dual engineering process: (a) family engineering defines the commonality and variability among all members of the SPL, and (b) application engineering derives specific products based on the common foundation combined with a variable selection of features. The number of derivable products in an SPL can thus be exponential in the number of features. This inherent complexity poses two main challenges when it comes to modelling: firstly, the formalism used for modelling SPLs needs to be modular and scalable. Secondly, it should ensure that all products behave correctly by providing the ability to analyse and verify complex models efficiently. In this paper, we propose to integrate an established modelling formalism (Petri nets) with the domain of software product line engineering. To this end, we extend Petri nets to Feature Nets. While Petri nets provide a framework for formally modelling and verifying single software systems, Feature Nets offer the same sort of benefits for software product lines. We show how SPLs can be modelled in an incremental, modular fashion using Feature Nets, provide a Feature Nets variant that supports modelling dynamic SPLs, and propose an analysis method for SPL modelled as Feature Nets. By facilitating the construction of a single model that includes the various behaviours exhibited by the products in an SPL, we make a significant step towards efficient and practical quality assurance methods for software product lines.

  • 19. Patrignani, Marco
    et al.
    Agten, Pieter
    Strackx, Raoul
    Jacobs, Bart
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Piessens, Frank
    Secure compilation to protected module architectures2015In: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 37, no 2, article id 6Article in journal (Refereed)
  • 20. Patrignani, Marco
    et al.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Fully abstract trace semantics for low-level isolation mechanisms2014In: Symposium on Applied Computing, SAC 2014. / [ed] Yookun Cho, Sung Y. Shin, Sang-Wook Kim, Chih-Cheng Hung, Jiman Hong, ACM Press, 2014, p. 1562-1569Conference paper (Refereed)
    Abstract [en]

    Many software systems adopt isolation mechanisms of modernprocessors as software security building blocks. Reasoningabout these building blocks means reasoning aboutelaborate assembly code, which can be very complex due tothe loose structure of the code. A way to overcome this complexityis giving the code a more structured semantics. Thispaper presents one such semantics, namely a fully abstracttrace semantics, for an assembly language enhanced withprotection mechanisms of modern processors. The trace semanticsrepresents the behaviour of protected assembly codewith simple abstractions, unburdened by low-level details, atthe maximum degree of precision. Additionally, it capturesthe capabilities of attackers to protected software and simplifiesproviding a secure compiler targeting that language.

  • 21. Patrignani, Marco
    et al.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Fully abstract trace semantics for protected module architectures2015In: Computer languages, systems & structures, ISSN 1477-8424, E-ISSN 1873-6866, Vol. 42, p. 22-45Article in journal (Refereed)
    Abstract [en]

    Protected module architectures (PMAs) are isolation mechanisms of emerging processors that provide security building blocks for modern software systems. Reasoning about these building blocks means reasoning about elaborate assembly code, which can be very complex due to the loose structure of the code. One way to overcome this complexity is providing the code with a well-structured semantics. This paper presents one such semantics, namely a fully abstract trace semantics, for an assembly language enhanced with PMA. The trace semantics represents the behaviour of protected assembly code with simple abstractions, unburdened by low-level details, at the maximum degree of precision. Furthermore, it captures the capabilities of attackers to protected code and simplifies the formulation of a secure compiler targeting PMA-enhanced assembly language.

  • 22.
    Patrignani, Marco
    et al.
    KU Leuven, Belgium.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Piessens, Frank
    KU Leuven, Belgium.
    Secure compilation of Object-Oriented components to protected module architectures2013In: Programming Languages and Systems, Springer Berlin/Heidelberg, 2013, p. 176-191Conference paper (Refereed)
    Abstract [en]

    A fully abstract compilation scheme prevents the security features of the high-level language from being bypassed by an attacker operating at a particular lower level. This paper presents a fully abstract compilation scheme from a realistic object-oriented language with dynamic memory allocation, cross-package inheritance, exceptions and inner classes to untyped machine code. Full abstraction of the compilation scheme relies on enhancing the low-level machine model with a fine-grained, program counter-based memory access control mechanism. This paper contains the outline of a formal proof of full abstraction of the compilation scheme. Measurements of the overhead introduced by the compilation scheme indicate that it is negligible. 

  • 23.
    Proenca, Jose
    et al.
    INESC TEC, HASLab, Braga, Portugal.;Univ Minho, Braga, Portugal.;Katholieke Univ Leuven, Dept Comp Sci, IMinds DistriNet, Louvain, Belgium..
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Typed Connector Families2016In: Formal Aspects Of Component Software, Springer, 2016, p. 294-311Conference paper (Refereed)
    Abstract [en]

    Typed models of connector/component composition specify interfaces describing ports of components and connectors. Typing ensures that these ports are plugged together appropriately, so that data can flow out of each output port and into an input port. These interfaces typically consider the direction of data flow and the type of values flowing. Components, connectors, and systems are often parameterised in such a way that the parameters affect the interfaces. Typing such connector families is challenging. This paper takes a first step towards addressing this problem by presenting a calculus of connector families with integer and boolean parameters. The calculus is based on monoidal categories, with a dependent type system that describes the parameterised interfaces of these connectors. As an example, we demonstrate how to define n-ary Reo connectors in the calculus. The paper focusses on the structure of connectors-well-connectedness-and less on their behaviour, making it easily applicable to a wide range of coordination and component-based models. A type-checking algorithm based on constraints is used to analyse connector families, supported by a proof-of-concept implementation.

  • 24.
    Proenca, Jose
    et al.
    Univ Minho, Dept Informat, P-4710057 Braga, Portugal;INESC TEC, P-4710057 Braga, Portugal.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Typed connector families and their semantics2017In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 146, p. 28-49Article in journal (Refereed)
    Abstract [en]

    Typed models of connector/component composition specify interfaces describing ports of components and connectors. Typing ensures that these ports are plugged together appropriately, so that data can flow out of each output port and into an input port. These interfaces typically consider the direction of data flow and the type of values flowing. Components, connectors, and systems are often parameterised in such a way that the parameters affect the interfaces. Typing such connector families is challenging. This paper takes a first step towards addressing this problem by presenting a calculus of connector families with integer and boolean parameters. The calculus is based on monoidal categories, with a dependent type system that describes the parameterised interfaces of these connectors. We use families of Reo connectors as running examples, and show how this calculus can be applied to Petri Nets and to BIP systems. The paper focuses on the structure of connectors-well-connectedness-and less on their behaviour, making it easily applicable to a wide range of coordination and component-based models. A type-checking algorithm based on constraints is used to analyse connector families, supported by a proof of-concept implementation.

  • 25.
    Sayaf, Rula
    et al.
    Katholieke Univ Leuven, IMinds DistriNet, Dept Comp Sci, Leuven, Belgium.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. Katholieke Univ Leuven, IMinds DistriNet, Dept Comp Sci, Leuven, Belgium.
    Harper, Richard
    Microsoft Res, Cambridge, England.
    CPS2: a Contextual Privacy Framework for Social Software2014In: 10th International Conference on Security and Privacy in Communication Networks (SECURECOMM2014) / [ed] Tian, J; Jing, J; Srivatsa, M, 2014, Vol. 153, p. 25-32Conference paper (Refereed)
    Abstract [en]

    Social software has become one of the most prominentmeans for communication. Context is essential for managing privacy andguiding communication. However, in social software, context can be ambiguousdue to the overload of data and the mix of various audiences,resulting in privacy issues.To overcome context issues, we analyse the role of context in communicationand privacy management, and propose CPS2, a conceptual frameworkof contextual privacy management. CPS2 identifies the interpretationof data as the ingredient in contextual privacy management thatonce preserved within any disclosure context, contextual privacy can bepreserved. We present how CPS2 can be technically realised, and how itaddresses context issues and offers fine-granular context control.

  • 26. Sayaf, Rula
    et al.
    Rule, James B.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Can users control their data in social software?: An ethical analysis of control systems2013In: Proc. Security and Privacy Workshops 2013, IEEE Computer Society, 2013Conference paper (Refereed)
  • 27.
    ter Beek, Maurice
    et al.
    CNR, ISTI, I-56100 Pisa, Italy.
    Clarke, Dave
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Schafer, Ina
    TU Braunschweig, Braunschweig, Germany.
    Editorial preface for the JLAMP Special Issue on Formal Methods for Software Product Line Engineering2015In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 85, no 1, p. 123-124Article in journal (Other academic)
1 - 27 of 27
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf