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. This paper presents λ_obliv, a core language whose type system enforces obliviousness. Prior work on type-enforced oblivious computation has focused on deterministic programs. λ_obliv is new in its consideration of programs that implement probabilistic algorithms, such as those involved in cryptography. λ_obliv employs a substructural type system and a novel notion of probability region to ensure that information is not leaked via the distribution of visible events. The use of regions was motivated by a source of unsoundness that we discovered in the type system of ObliVM, a language for implementing state of the art oblivious algorithms and data structures. We prove that λ_obliv's type system enforces obliviousness and show that it is expressive enough to typecheck advanced tree-based oblivious RAMs.

[ http ]

@inproceedings{darais20obliv,
  title = {A Language for Probabilistically Oblivious Computation},
  booktitle = {Proceedings of the {ACM} Conference on Principles of Programming Languages (POPL)},
  author = {David Darais and Ian Sweet and Chang Liu and Michael Hicks},
  year = {2020},
  month = jan
}

This file was generated by bibtex2html 1.99.