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: