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.

We then expanded 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 are oblivious by showing they are well-typed in λ-obliv.

We also investigated automatically proving that oblivious data structures, such as oblivious stacks, are probabilistically oblivious using the type system of λ-obliv. Unfortunately, these programs failed to type check in our language. At first, we believed that this was a limitation of our type system. In other words, we believed that oblivious stacks were probabilistically oblivious but that our type system was too conservative to prove it. Recently, we showed that we were wrong. Oblivious stacks, and oblivious data structures more generally, are not probabilistically oblivious due to the possibility of overflow.

We are currently investigating extending λ-obliv to work in a Secure Multiparty Computation (MPC) setting by integrating it with Symphony, a state of the art programming language for MPC.

Past publications from (current and former) members of this project: