Oblivious Program Execution and Path-Sensitive Non-interference

Abstract

Various cryptographic constructions allow an untrusted cloud server to compute over encrypted data, without decrypting the data. However, this prevents the cloud server from branching according to encrypted values. We study the constraints imposed by this important scenario by formulating and solving an equivalent information-flow problem, based on assuming an adversary could observe the control path. We develop a type system that prevents control-path information leaks, prove soundness, and compare with traditional implicit information-flow. Because simply preventing programs that leak information severely restricts the language, we define alternate (and easily implemented) semantics that execute multiple paths and combine the results using data operations. This produces a termination problem which we address with a more refined type system that characterizes a useful class of obliviously executable programs. We prove fundamental results about this language, semantics, and type system and conclude by comparing with traditional timing-based information-flow.