Trust from Explicit Evidence: Integrating Digital Signatures and Formal Proofs
Investigator: Elsa Gunter
This project proposed to develop a common logical framework that accounts for two principal sources of trust in software: digital signatures and explicit proof. Such a framework will allow us to rigorously specify, enforce, and analyze security policies that rely on multiple modes and sources of trust. Based on recent work by the PI and collaborators, the framework will be cast as a modal type theory which comes equipped with a notation for programs and proofs. We exploit this relationship to guarantee composability and usability form the programmers point of view.
Hard Problem Addressed
- Scalability and Composability
- Dennis Griffith and Elsa L. Gunter, “LiquidPi: Inferable Dependent Session Types”, 5th International NASA Formal Methods (NFM 2013), Moffett Field, CA May 14-16, 2013. [full text]