Memory Trace Oblivious Program Execution

Cloud computing allows users to delegate data and computation to cloud service providers, at the cost of giving up physical control of their computing infrastructure. An attacker (e.g., insider) with physical access to the computing platform can perform various physical attacks, including probing memory buses and cold-boot style attacks. Previous work on secure (co-)processors provides hardware support for memory encryption and prevents direct leakage of sensitive data over the memory bus. However, an adversary snooping on the bus can still infer sensitive information from the memory access traces. Existing work on Oblivious RAM (ORAM) provides a solution for users to put all data in an ORAM; and accesses to an ORAM are obfuscated such that no information leaks through memory access traces. This method, however, incurs significant memory access overhead. In this work, we are among the first to leverage programming language techniques to offer efficient memory-trace oblivious program execution, while providing formal security guarantees. We first formally define the notion of memory-trace obliviousness, and provide a type system for verifying that a program satisfies this property. We then design a compiler that transforms a program into one that satisfies memory trace obliviousness. To achieve optimal efficiency, our compiler aims to minimize the usage of ORAM whenever possible, and would partition variables in smaller ORAM banks (which are faster to access than larger ORAM banks) without risking security. We use several example programs to demonstrate the efficiency gains our compiler achieves in comparison with the naive method of placing all variables in the same ORAM