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

Publications