Short Paper: Probabilistically Almost-Oblivious Computation. Ian Sweet, David Darais, and Michael Hicks. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), November 2020.

Memory-trace Obliviousness (MTO) is a noninterference property: programs that enjoy it have neither explicit nor implicit information leaks, even when the adversary can observe the program counter and the address trace of memory accesses. Probabilistic MTO relaxes MTO to accept probabilistic programs. In prior work, we developed λobliv, whose type system aims to enforce PMTO. We showed that λobliv could typecheck (recursive) Tree ORAM, a sophisticated algorithm that implements a probabilistically oblivious key-value store. We conjectured that λobliv ought to be able to typecheck more optimized oblivious data structures (ODSs), but that its type system was as yet too weak.

In this short paper we show we were wrong: ODSs cannot be implemented in λobliv because they are not actually PMTO, due to the possibility of overflow, meaning: a write may silently fail due to a local lack of space. This was surprising to us because Tree ORAM can also overflow but is still PMTO . The paper explains what is going on and sketches the task of adapting the PMTO property, and λobliv's type system, to characterize ODS security.

.pdf ]

  title = {Short Paper: Probabilistically Almost-Oblivious Computation},
  author = {Ian Sweet and David Darais and Michael Hicks},
  booktitle = {Proceedings of the {ACM SIGPLAN} Workshop on Programming Languages and Analysis for Security (PLAS)},
  year = 2020,
  month = nov

This file was generated by bibtex2html 1.99.