ABOUT THE PROJECT:

This project is developing a common logical framework that will account for two principal sources of trust in software: digital signatures and explicit proof. The framework will allow us to rigorously specify, enforce, and analyze security policies that rely on multiple modes and sources of trust. Based on earlier work by the PI and collaborators, the framework is being cast as a modal type theory that comes equipped with a notation for programs and proofs. We will exploit this relationship to guarantee composability (since types govern interfaces between code) and usability from the programmer's point of view (since type checking is effective during software development). The project will proceed in two phases: framework design and metatheoretic study in the first phase, and a testbed implementation in the second phase. A possible third phase may study usability from the end user's point of view.

OUR TEAM:

Frank Pfenning (CSD, CMU) and Elsa L. Gunter