Skip to Main content Skip to Navigation
New interface
Conference papers

Micro-Policies: Formally Verified, Tag-Based Security Monitors

Abstract : 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.
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Bruno Blanchet Connect in order to contact the contributor
Submitted on : Thursday, September 6, 2018 - 10:37:27 AM
Last modification on : Friday, November 18, 2022 - 9:23:16 AM
Long-term archiving on: : Friday, December 7, 2018 - 3:43:08 PM


Files produced by the author(s)



Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, et al.. Micro-Policies: Formally Verified, Tag-Based Security Monitors. 2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, ⟨10.1109/SP.2015.55⟩. ⟨hal-01265666⟩



Record views


Files downloads