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.
Type de document :
Communication dans un congrès
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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01265666
Contributeur : Bruno Blanchet <>
Soumis le : lundi 1 février 2016 - 13:58:24
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Lien texte intégral

Identifiants

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〉

Partager

Métriques

Consultations de la notice

113