John Michael Grosen

John Michael Grosen
MIT EECS | Undergraduate Research and Innovation Scholar
Advisor: Adam Chlipala
Department: EECS
Years: 2018-2019
Research Project Title:

Security Policies for Applications

abstract: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."