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.

[ arXiv | http ]

@techreport{darais19obliv,
  title = {A Language for Probabilistically Oblivious Computation},
  author = {David Darais and Ian Sweet and Chang Liu and Michael Hicks},
  institution = {CoRR},
  number = {abs/1711.09305},
  year = {2019},
  archiveprefix = {arXiv},
  eprint = {1711.09305},
  month = jul
}

This file was generated by bibtex2html 1.99.