5th Year MS Thesis Presentation - Sonya Simkin
— 3:30pm
Location:
In Person
-
Reddy Conference Room, Gates Hillman 4405 (New Location)
Speaker:
SONYA SIMKIN
,
Master's Student
Computer Science Department
Carnegie Mellon University
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 non-interference, 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 non-determinism 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 non-interference. In particular, to combat occlusion, we define a possibilistic logical relation, which considers the set of all possible values an expression could evaluate to.
Thesis Committee
Stephanie Balzer (Chair)
Robert Harper
Additional Information
For More Information:
amalloy@cs.cmu.edu