A Language for Probabilistically Oblivious Computation. David Darais, Ian Sweet, Chang Liu, and Michael Hicks. In Proceedings of the ACM Conference on Principles of Programming Languages (POPL), January 2020.

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.