This research project is building a new way to specify security policies for complex applications and prove that implementations fit the applications’ policies. This involves building semantics for describing policies and implementations in Coq, a runtime system, tooling to support proving properties about policies, and providing example applications to demonstrate its usefulness. Previous work in information flow control focuses on scenarios where programmers just want to improve confidence that their system does not leak data. However, users are increasingly interested in strong guarantees of their privacy, rather than blindly trusting third parties. Our system achieves the best of both worlds, protecting against untrusted application builders while allowing for performance on par with traditional methods.

“This project is the marriage between my two favorite things: formal methods and protecting people’ s privacy. Coming from my background in binary analysis, I’m excited to learn more about applying formal reasoning to complex systems and push the field forward. SuperUROP gives me the opportunity to dedicate a large portion of my time to intensive research.”