One challenge of building software systems that handle sensitive information is ensuring that their components meet certain security policies, describing what information each component is allowed to access and pass on. In complex systems where information may flow through many different components, it’ s difficult to reason about all possible flows of information and check that a policy is satisfied in every case. This project aims to develop a framework to specify security policies, build larger systems from user-provided implementations of components, and automatically verify that these systems adhere to their policies. This framework will be formalized in the Coq proof assistant, allowing users to derive machine-checked formal proofs showing that the security policies are satisfied.

I became interested in formal verification and interactive theorem proving after doing a UROP project with Professor Chlipala. Through this SuperUROP project, I hope to learn more about the different ideas and challenges in applying formal methods to larger-scale problems.