39 citations · 86 across the 11 of their papers we have counts for
11 papers
Step in Tine: Forking Processes in Functional Choreographies
Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti
Traditional concurrent-programming techniques require programmers to painstakingly write programs for each participant in a concurrent system. Choreographic programming, in contras…
zkStruDul: Programming zkSNARKs with Structural Duality
Rahul Krishnan, Ashley Samuelson, Emily Yao +1
Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling…
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti
Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs…
Nonmalleable Progress Leakage
Ethan Cecchetti
Information-flow control systems often enforce progress-insensitive noninterference, as it is simple to understand and enforce. Unfortunately, real programs need to declassify resu…
A Language for Smart Contracts with Secure Control Flow (Technical Report)
Siqiu Yao, Haobin Ni, Stephanie Ma +3
Smart contracts are frequently vulnerable to control-flow attacks based on confused deputies, reentrancy, and incorrect error handling. These attacks exploit the complexity of inte…
Computationally Bounded Robust Compilation and Universally Composable Security
Robert Künnemann, Marco Patrignani, Ethan Cecchetti
Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and…
Compositional Security for Reentrant Applications
Ethan Cecchetti, Siqiu Yao, Haobin Ni +1
The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Informatio…
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…
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…
Nonmalleable Information Flow: Technical Report
Ethan Cecchetti, Andrew C. Myers, Owen Arden
Noninterference is a popular semantic security condition because it offers strong end-to-end guarantees, it is inherently compositional, and it can be enforced using a simple secur…