An oblivious computation is one that is free of direct and indirect information leaks, e.g., due to observable differences in timing and memory access patterns. In this talk I will present L-obliv, a core language whose type system enforces obliviousness. Prior work on type-enforced oblivious computation has focused on deterministic programs. Lobliv is new in its consideration of programs that implement probabilistic algorithms, such as those involved in cryptography. I will demonstrate how L-obliv can be used to implement oblivious data structures and software ORAMs.

To read the paper, please check: http://www.cs.umd.edu/~mwh/papers/darais17obliv.html