An oblivious program is one that is free of direct and indirect information leaks, e.g., due to observable differences in the content, timing, or pattern of direct outputs, or even network messages and memory access patterns. The latter may be exploited when an attacker has physical access to the machine, or remote access to hardware traces (e.g. through a remotely exposed debug interface). Our approach uses type systems to ensure that all well-typed programs are oblivious.
Our initial work focused on deterministic obliviousness. This form of obliviousness reasons that traces produced by a program are identical. Two signature results are GhostRider (ASPLOS 2015 Best Paper), which is a hardware/software co-design which the former includes an Oblivious RAM (ORAM) controller; and Blazer, a program analysis tool for proving the absence of timing channels using a trace-based decomposition strategy.
Our current work aims to expand the expressiveness of the Ghostrider-style approach. In particular, Ghostrider’s type system models the actions of the ORAM as opaque and deterministic, based on the assumption that the ORAM is correct. We would like to avoid making this assumption, and instead allow the type system to reason about the ORAM implementation directly. Unfortunately, efficient (logarithmic) implementations of Oblivious RAM (ORAM), such as Tree ORAM require the use of probabilistic choice. In the presence of probability, the memory traces produced by a program will not be identical but may still be probabilistically oblivious. Our recent work develops a language, λ-obliv, whose type system enforces probabilistic obliviousness. This ensures that the distributions of memory traces produced by programs are identical. We have automatically proved that various efficient ORAM schemes and oblivious data structures are oblivious by showing they are well-typed in λ-obliv.
In ongoing work, we are considering how to extend λ-obliv’s type system to accept implementations of oblivious data structures, thereby proving them to be probabilistically oblivious.
Past publications from (current and former) members of this project:
- A Language for Probabilistically Oblivious Computation, POPL 2020. David Darais, Ian Sweet, Chang Liu, and Michael Hicks.
- Evaluating Design Tradeoffs in Numeric Static Analysis for Java, ESOP 2018. Shiyi Wei, Piotr Mardziel, Andrew Ruef, Jeffrey S. Foster, and Michael Hicks.
- Languages for Oblivious Computation, PLAS 2017. Michael Hicks.
- A Counterexample-guided Approach to Finding Numerical Invariants, FSE 2017. ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks.
- Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels, PLDI 2017. Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei.
- GhostRider: A Hardware-Software System for Memory Trace Oblivious Computation, ASPLOS 2015. (best paper). Chang Liu, Austin Harris, Martin Maas, Michael Hicks, Mohit Tiwari, and Elaine Shi.
- Memory Trace Oblivious Program Execution, CSF 2013 (Winner of NSA’s Best Scientific Cybersecurity Paper competition). Chang Liu, Michael Hicks, and Elaine Shi.