|
Securing computing systems is a formidable task that becomes harder as systems become more complex, widespread and intertwined with our daily lives. This is especially true for protection mechanisms that use cryptographic schemes and protocols. This interdisciplinary project strives to combine two complementary approaches to analyzing the security of complex protocols. The first is modularity: The ability to deduce the security of a complex system from the security of its simpler components. The second is mechanization: the use of computer tools in which mathematical proofs are formalized on the computer, eliminating the errors that may lurk in paper-and-pencil proofs. More broadly, the project is working to foster deeper connections between the cryptography community and the programming languages and formal methods community. In particular, it is training graduate students from both sides of this divide in the methodologies of the other side.
Specifically, the project is combining the universally composable (UC) security framework with the EasyCrypt cryptographic proof assistant, so as to obtain a proof assistant and related tools and methodologies enabling security proofs that are rigorous and cryptographically sound, as well as mechanized and modular. In order to find common ground between the UC framework, which was not designed for automation, and the EasyCrypt mechanized proof assistant, the project brings together an interdisciplinary team with expertise in theoretical cryptography, programming languages, and the design and implementation of proof assistants. The project is bridging the gap between the coroutine-based execution model of the UC framework and the traditional procedural execution model of EasyCrypt, developing a domain-specific extension of the EasyCrypt programming language for representing UC protocols and security specifications, and implementing the UC composition operation and theorem within EasyCrypt. The project is progressing through a series of stages, first developing an EasyCrypt architecture supporting UC, and testing this architecture by hand via simple case studies, and then gradually moving toward greater ease of protocol expression and proof automation. The tools and methodologies developed during the project are being evaluated via a series of increasingly complex case studies, working up to real-world systems that combine algorithmic and systems security, such as the Signal messaging system, the OpenStack cloud management framework, and secure multi-party computation systems. Outreach events such as hackathons and tutorials are being used to increase the impact of the developed technology to students and the research community.
|
SaTC: CORE: Medium: Towards Mechanized Proofs of Composable Security Properties