IEEE Symposium on Security and Privacy 2015
Cache memory, Computer security
Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level “symbolic machine,” and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy’s rules embodies a high-level specification characterizing a useful security property. Last, we show how the symbolic machine itself can be implemented in terms of a hardware rule cache and a software controller.
Azevedo de Amorim, Arthur; Denes, Maxime; Giannarakis, Nick; Hritcu, Catalin; Pierce, Benjamin C.; Spector-Zabusky, Antal; and Tolmach, Andrew, "Micro-Policies: Formally Verified, Tag-Based Security Monitors" (2015). Computer Science Faculty Publications and Presentations. 145.