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.
Liste complète des métadonnées

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01265666
Contributor : Bruno Blanchet <>
Submitted on : Thursday, September 6, 2018 - 10:37:27 AM
Last modification on : Wednesday, February 27, 2019 - 2:36:01 PM
Document(s) archivé(s) le : Friday, December 7, 2018 - 3:43:08 PM

File

micro-policies.pdf
Files produced by the author(s)

Identifiers

Citation

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin 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, 2015, 2015 IEEE Symposium on Security and Privacy. 〈10.1109/SP.2015.55〉. 〈hal-01265666〉

Share

Metrics

Record views

227

Files downloads

63