Cryptographic primitives, such as encryption, decryption, and key generation, are vital to the security of many of today's applications, but are difficult to reason about in an information-flow setting. In particular, they conflict with the notion of noninterference, the property that observable outputs are uninfluenced by secret inputs in an information-flow secure program. Not only do ciphertexts often rely on secure data (and thus would be ruled out in a typical information-flow setting), the use of nondeterminism in their generation may serve as a source of information-flow leak (called occlusion). Logical relations are a technique which can be used to prescribe properties of a program based on its computational behavior, rather than relying on static well-formedness. Through this semantic approach, one can not only validate well-typed terms by showing their inhabitation of the logical relation (via the "fundamental theorem"), but also validate ill-typed terms which behave "correctly" with respect to the definition of the logical relation. In this thesis, we extend a version of the simply-typed lambda calculus with cryptographic primitives, and define an information-flow control type system to statically enforce safe usage of said primitives. We then use the technique of logical relations to define a semantic verification method for noninterference. In particular, to combat occlusion, we define a possibilistic logical relation, which considers the set of all possible values an expression could evaluate to.

111 pages

Thesis Committee:
Stephanie Balzer (Chair)
Robert Harper

Jignesh Patel, Interim Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: School of Computer Science

This page maintained by reports@cs.cmu.edu