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

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01265666
Contributeur : Bruno Blanchet <>
Soumis le : jeudi 6 septembre 2018 - 10:37:27
Dernière modification le : vendredi 7 septembre 2018 - 01:10:36
Document(s) archivé(s) le : vendredi 7 décembre 2018 - 15:43:08

Fichier

micro-policies.pdf
Fichiers produits par l'(les) auteur(s)

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

162

Téléchargements de fichiers

11