Micro-Policies: Formally Verified Tagging Schemes for Safety and Security (Extended Abstract)

ABSTRACT. Today's computer systems are distressingly insecure. A host of vulnerabilities arise from the violation of known, but in-practice unenforceable, safety and security policies, including high-level programming models and critical invariants of low-level programs. This project is aimed at showing that a rich and valuable set of _micro-policies_ can be efficiently enforced by a new generic hardware-software mechanism and result in more secure and robust computer systems. In particular we aim to come up with a clean formal framework in Coq for expressing, composing, and verifying arbitrary micro-policies, and to instantiate this framework on a diverse set of interesting examples.