The project proposes "manifest security" as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure software and to demonstrate its feasibility in practice.
Manifest security applies to extensible software platforms, where it addresses two fundamental problems: (1) how to specify policies about what resources an extension may use and how it can handle sensitive data, and (2) how to enforce such policies. The project is developing a novel high-level logical specification language, encompassing both authorization properties for access control and information flow properties to restrict the use of sensitive data. Adherence to the specification is enforced by a combination of static and dynamic methods, and trustworthiness of the code is established by the explicit representation and verification of formal proofs. Such proofs make the security properties manifest.
Because extensible systems are in widespread use (for example, in web browsers, office software, media players, games, virtual communities, and operating systems) the concept of manifest security has significant potential for broad impact. Rigorous verification methods based on logic and type theory are increasingly important to the software industry; the project advances the use of these methods to ensure security. Results from the research are released via publications and a software platform for secure browser extension, making advances accessible to researchers and practitioners. Results are being integrated into graduate and undergraduate teaching materials as well as courses at summer schools.
