3 papers
cs.PL2020
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…
cs.CR2020
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…
cs.DC2018
Obladi: Oblivious Serializable Transactions in the Cloud
Natacha Crooks, Matthew Burke, Ethan Cecchetti +3
This paper presents the design and implementation of Obladi, the first system to provide ACID transactions while also hiding access patterns. Obladi uses as its building block obli…