NB: All works are the copyright of their respective authors unless otherwise stated. The ps.gz files are gzip compressed postscript. The pdf files are mostly searchable and sometimes have hyperlinked cross-references. The txt ones do not render the mathematics or ligatures but are convenient for grepping.
We present a compiler for generating custom cryptographic protocols from high-level multiparty sessions.
Sessions specify pre-arranged patterns of message exchanges between distributed participants and their data accesses to a shared store.We define integrity and confidentiality properties of sessions, in a setting where the network and arbitrary compromised parties may be controlled by an adversary. Our compiler enforces these security properties by guarding the sending and receiving of session messages by efficient cryptographic operations and checks. Given a session, our compiler generates an ML module and an interface that exposes send and receive functions that can be called by application code for each party. We prove that this generated code is secure by relying on a recent refinement type system for ML. Functions in the module interface are given dependent types that express invariants of the session state. We typecheck the program against this interface, and complete the proof by a brief, handcrafted argument.
We illustrate and evaluate our implementation on a series of typical protocols, inspired by web services. In comparison with prior work, our source language is more expressive, our implementation more efficient, and our proof technique novel. Most of the proof is performed by mechanized type checking of the generated code, and does not rely on the correctness of our compiler. We obtain the strongest session security guarantees to date in a model that accounts for the actual details of protocol code.
Distributed applications can be structured as parties that exchange messages according to some pre-arranged communication patterns. These ses- sions (or contracts, or protocols) simplify distributed programming: when coding a role for a given session, each party just has to follow the intended message flow, under the assumption that the other parties are also compliant.
In an adversarial setting, remote parties may not be trusted to play their role. Hence, defensive implementations also have to monitor one another, in order to detect any deviation from the assigned roles of a session. This task involves low- level coding below session abstractions, thus giving up most of their benefits.
We explore language-based support for sessions. We extend the ML language with session types that express flows of messages between roles, such that well- typed programs always play their roles. We compile session type declarations to cryptographic communication protocols that can shield programs from any low- level attempt by coalitions of remote peers to deviate from their roles. Our main result is that, when reasoning about programs that use our session implementation, one can safely assume that all session peers comply with their roles---without trusting their remote implementations.
Distributed applications can be structured as parties that exchange messages according to some pre-arranged communication patterns. These sessions (or contracts, or protocols) simplify distributed programming: when coding a role for a given session, each party just has to follow the intended message flow, under the assumption that the other parties are also compliant.
In an adversarial setting, remote parties may not be trusted to play their role. Hence, defensive implementations also have to monitor one another, in order to detect any deviation from the assigned roles of a session. This task involves low-level coding below session abstractions, thus giving up most of their benefits.
We explore language-based support for sessions. We extend the ML language with session types that express flows of messages between roles, such that well-typed programs always play their roles. We compile session type declarations to cryptographic communication protocols that can shield programs from any low-level attempt by coalitions of remote peers to deviate from their roles. Our main result is that, when reasoning about programs that use our session implementation, one can safely assume that all session peers comply with their roles—without trusting their remote implementations.
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming language support for such systems, focussing on their typing and naming issues.
We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately built programs. The main features are: (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type safety of associated values, e.g. values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility.
These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.
A framework is defined within which reactive systems can be studied formally. The framework is based on s-categories, which are a new variety of categories within which reactive systems can be set up in such a way that labelled transition systems can be uniformly extracted. These lead in turn to behavioural preorders and equivalences, such as the failures preorder (treated elsewhere) and bisimilarity, which are guaranteed to be congruential. The theory rests on the notion of relative pushout, which was previously introduced by the authors.
The framework is applied to a particular graphical model, known as link graphs, which encompasses a variety of calculi for mobile distributed processes. The specific theory of link graphs is developed. It is then applied to an established calculus, namely condition-event Petri nets.
In particular, a labelled transition system is derived for condition-event nets, corresponding to a natural notion of observable actions in Petri-net theory. The transition system yields a congruential bisimilarity coinciding with one derived directly from the observable actions. This yields a calibration of the general theory of reactive systems and link graphs against known specific theories.
In most programming languages, type abstraction is guaranteed by syntactic scoping in a single program, but is not preserved by marshalling during distributed communication. A solution is to generate hash types at compile time that consist of a fingerprint of the source code implementing the data type. These hash types can be tupled with a marshalled value and compared efficiently at unmarshall time to guarantee abstraction safety. In this paper, we extend a core calculus of ML-like modules, functions, distributed communication, and hash types, to integrate structural subtyping, user- declared subtyping between abstract types, and bounded existential types. Our semantics makes two contributions: (1) the explicit tracking of the interaction between abstraction boundaries and subtyping; (2) support for user-declared module upgrades with propagation of the resulting subhashing relation throughout the network during communication. We prove type preservation, progress, determinacy, and erasure for our system.
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming-language support for such systems, focussing on their typing and naming issues.
We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. The main features are: (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g. values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkication of threads and mutexes to support computation mobility.
These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented.
Acute extends an OCaml core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. It is expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs, disentangling the language runtime from communication.
This requires a synthesis of novel and existing features: (1) type-safe marshalling of values between programs; (2) dynamic loading and controlled rebinding to local resources; (3) modules and abstract types with abstraction boundaries that are respected by interaction; (4) global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles; (5) versions and version constraints, integrated with type identity; (6) local concurrency and thread thunkification; and (7) second-order polymorphism with a namecase construct. We deal with the interplay among these features and the core, and develop a semantic definition that tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but which still admits an efficient implementation strategy.
Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.
We obtain a namespace for abstract types that is global, i.e. meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.
The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e. unlabelled transition rules--- together with a structural congruence. This form, which I call a reactive system, is highly expressive but is limited in an important way: LTSs lead more naturally to operational equivalences and preorders. This paper shows how to synthesise an LTS for a wide range of reactive systems. A label for an agent (process) `a' is defined to be any context `F' which intuitively is just large enough so that the agent `Fa' (`a' in context `F') is able to perform a reaction step. The key contribution of my work is the precise definition of ``just large enough'' in terms of the categorical notion of relative pushout (RPO). I then prove that several operational equivalences and preorders (strong bisimulation, weak bisimulation, the traces preorder, and the failures preorder) are congruences when sufficient RPOs exist.
This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive systems and how to prove congruence results for operational equivalences and preorders defined above those transitions. The purpose of this paper is (i) to show that the hypotheses required of functorial reactive systems from Part 1, for example the sliding properties of IPO (idem pushout) squares, are indeed satisfied for functors of a general form; (ii) to illustrate an example of a functorial reactive system based on Milner's action calculi, which satisfy the RPO (relative pushout) hypothesis required in the proofs of congruence from Part 1.
The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules --i.e. unlabelled transition rules-- together with a structural congruence. This form, which I call a reactive system, is highly expressive but is limited in an important way: LTSs lead more naturally to operational equivalences and preorders.
So one would like to derive from reaction rules a suitable LTS. This dissertation shows how to derive an LTS for a wide range of reactive systems. A label for an agent (process) a is defined to be any context F which intuitively is just large enough so that the agent Fa (``a in context F'') is able to perform a reaction. The key contribution of my work is the precise definition of ``just large enough'', in terms of the categorical notion of relative pushout (RPO), which ensures that several operational equivalences and preorders (strong bisimulation, weak bisimulation, the traces preorder, and the failures preorder) are congruences when sufficient RPOs exist.
I present a substantial example of a family of reactive systems based on closed, shallow action calculi (those with no free names and no nesting). I prove that sufficient RPOs exist for a category of such contexts. The proof is carried out indirectly in terms of a category of graphs and embeddings and gives precise (necessary and sufficient) conditions for the existence of RPOs. I conclude by arguing that these conditions are satisfied for a wide class of reaction rules. The thrust of this dissertation is, therefore, towards easing the burden of exploring new models of computation by providing a general method for achieving useful operational congruences.
Action calculi, which generalise process calculi such as Petri nets, pi-calculus and ambient calculus, have been presented in terms of action graphs. We here offer linear action graphs as a primitive basis for action calculi. This paper presents the category of embeddings of undirected linear action graphs without nesting, using a novel form of graphical reasoning which simplifies some otherwise complex manipulations in regular algebra. The results are adapted in a few lines to directed graphs. This work is part of a long-term search for a uniform behavioural theory for process calculi.
Action calculi, which have a graphical presentation, were introduced to develop a theory shared among different calculi for interactive systems. The pi-calculus, the lambda-calculus, Petri nets, the Ambient calculus and others may all be represented as action calculi. This paper develops a part of the shared theory.
A recent paper by two of the authors was concerned with the notion of reactive system, essentially a category of process contexts whose behaviour is presented as a reduction relation. It was shown that one can, for any reactive system, uniformly derive a labelled transition system whose associated behavioural equivalence relations (e.g. trace equivalence or bisimilarity) will be congruential, under the condition that certain relative pushouts exist in the reactive system. In the present paper we treat closed, shallow action calculi (those with no free names and no nested actions) as a generic application of these results. We define a category of action graphs and embeddings, closely linked to a category of contexts which forms a reactive system. This connection is of independent interest; it also serves our present purpose, as it enables us to demonstrate that appropriate relative pushouts exist.
Complemented by work to be reported elsewhere, this demonstration yields labelled transition systems with behavioural congruences for a substantial class of action calculi. We regard this work as a step towards comparable results for the full class.
The dynamics of reactive systems, e.g. CCS, has often been defined using a labelled transition system (LTS). More recently it has become natural in defining dynamics to use reaction rules --i.e. unlabelled transition rules-- together with a structural congruence. But LTSs lead more naturally to behavioural equivalences. So one would like to derive from reaction rules a suitable LTS.
This paper shows how to derive an LTS for a wide range of reactive systems. A label for an agent a is defined to be any context F which intuitively is just large enough so that the agent Fa (``a in context F'') is able to perform a reaction. The key contribution of this paper is a precise definition of ``just large enough'', in terms of the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when sufficient RPOs exist. Two examples --a simplified form of action calculi and term-rewriting-- are given, for which it is shown that sufficient RPOs indeed exist. The thrust of this paper is, therefore, towards a general method for achieving useful behavioural congruence relations.
A brief report on my summer internship work done with Greg Nelson and Allan Heydon at the Systems Research Center, Digital Equipment Corp. (now Compaq), Palo Alto, California.
This report describes research on morphisms between control structures (models of action calculi) and how they can be used to classify the expressive power of various process calculi. In particular, I describe a control structure IMGRAPH for classifying mobile action calculi and use it to show that LAMC (the AC encoding of the lambda-calculus) is less expressive than PIC (the AC encoding of the pi-calculus).
This paper is the result of research done as an undergraduate at the Oxford University Computing Lab. It describes a new way of teaching formal deductive logic to students familiar with functional programming and introduces to them metamathematical ideas by exploiting the students' familiarity with freely-generated data-structures and their recursion and induction principles.
This report is a greatly expanded version of the above paper. See the Errata list, the Gofer source-listings extracted from the document, and the JAPE source-listings (which are probably no longer compatible with the latest version of JAPE). ``Just Another Proof Editor'', known as JAPE, is a project of Bernard Sufrin and Richard Bornat. JAPE has a rich language for axiomatizing logics and tactics and provides a fully graphical interface for interactive, goal-directed proof.
This page: http://pauillac.inria.fr/~leifer/research.html.