SCS Undergraduate Thesis Topics
|Henry DeYoung||Frank Pfenning||An Authorization Logic for Reasoning with Quantitative Time|
The problem of allowing access to data and resources without compromising their security is a fundamental one in today's increasingly networked society. We believe that proof-carrying authorization, with its basis in logic, can serve as a theoretically sound solution to the access control problem. But, for proof-carrying authorization to be viable, its underlying logic must be sufficiently expressive to support a wide array of natural access control policies, including single-use and time-dependent authorizations. In this project, we will design a linear authorization logic that permits reasoning about time-dependent authorizations. We will also formalize the logic's metatheory, including the admissibility of cut, in the Twelf logical framework and implement a proof checker for the logic. Finally, we hope to explore the non-interference properties of the logic and use them to construct simple policy analysis tools.