4 papers
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch, Deepak Garg
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and…
Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch, Ethan Cecchetti
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 com…
First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti +2
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…
Nexus Authorization Logic (NAL): Logical Results
Andrew K. Hirsch, Michael R. Clarkson
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 revis…