-
Corps: A Core Calculus of Hierarchical Choreographic Programming
Authors:
Andrew K. Hirsch
Abstract:
Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and communication changes that modality. However, we must find an appropriate modal logic for the other side of the propositions-as-types correspondence. This paper argues f…
▽ More
Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and communication changes that modality. However, we must find an appropriate modal logic for the other side of the propositions-as-types correspondence. This paper argues for doxastic logics, or logics of belief. In particular, authorization logics -- doxastic logics with explicit communication -- appear to represent hierarchical choreographic programming. This paper introduces hierarchical choreographic programming and presents Corps, a language for hierarchical choreographic programming with a propositions-as-types interpretation in authorization logic.
△ Less
Submitted 3 June, 2024;
originally announced June 2024.
-
Alice or Bob?: Process Polymorphism in Choreographies
Authors:
Eva Graversen,
Andrew K. Hirsch,
Fabrizio Montesi
Abstract:
We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type a…
▽ More
We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type and \emph{process} polymorphism inspired by System F$_ω$. That is, PolyChor$λ$ is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor$λ$ processes to communicate \emph{distributed values}, leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor$λ$ give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programs are deadlock-free by design.
△ Less
Submitted 8 March, 2023;
originally announced March 2023.
-
Pirouette: Higher-Order Typed Functional Choreographies
Authors:
Andrew K. Hirsch,
Deepak Garg
Abstract:
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system…
▽ More
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system to its own. Message type soundness also guarantees deadlock freedom. All of our results are verified in Coq.
△ Less
Submitted 9 November, 2021; v1 submitted 5 November, 2021;
originally announced November 2021.
-
Giving Semantics to Program-Counter Labels via Secure Effects
Authors:
Andrew K. Hirsch,
Ethan Cecchetti
Abstract:
Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effe…
▽ More
Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effects to give semantics to program-counter labels. This framework leads to three results about program-counter labels. First, we develop a new proof technique for noninterference, the core security theorem for information-flow control in effectful languages. Second, we unify notions of security for different types of effects, including state, exceptions, and nontermination. Finally, we formalize the folklore that program-counter labels are a lower bound on effects. We show that, while not universally true, this folklore has a good semantic foundation.
△ Less
Submitted 10 December, 2020; v1 submitted 25 October, 2020;
originally announced October 2020.
-
First-Order Logic for Flow-Limited Authorization
Authors:
Andrew K. Hirsch,
Pedro H. Azevedo de Amorim,
Ethan Cecchetti,
Ross Tate,
Owen Arden
Abstract:
We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connective…
▽ More
We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connectives of first-order logic. Furthermore, this guarantee is the first to combine the notions of non-interference from both authorization logic and information-flow systems. All theorems in this paper are proven in Coq.
△ Less
Submitted 28 January, 2020;
originally announced January 2020.
-
Belief Semantics of Authorization Logic
Authors:
Andrew K. Hirsch,
Michael R. Clarkson
Abstract:
Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke seman…
▽ More
Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke semantics. A proof system is given for the logic; that system is proved sound with respect to the belief and Kripke semantics. The soundness proof for the belief semantics, and for a variant of the Kripke semantics, is mechanized in Coq.
△ Less
Submitted 3 August, 2013; v1 submitted 8 February, 2013;
originally announced February 2013.
-
Nexus Authorization Logic (NAL): Logical Results
Authors:
Andrew K. Hirsch,
Michael R. Clarkson
Abstract:
Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq.
Nexus Authorization Logic (NAL) [Schneider et al. 2011] is a logic for reasoning about authorization in distributed systems. A revised version of NAL is given here, including revised syntax, a revised proof theory using localized hypotheses, and a new Kripke semantics. The proof theory is proved sound with respect to the semantics, and that proof is formalized in Coq.
△ Less
Submitted 15 November, 2012; v1 submitted 15 November, 2012;
originally announced November 2012.
