micro-policies/micro-policies-coq

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors

Micro-Policies in Coq

Description

Coq formalization accompanying the paper:

• Micro-Policies: A Framework for Verified, Tag-Based Security Monitors. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach. In 36th IEEE Symposium on Security and Privacy (Oakland S&P), May 2015. (http://prosecco.gforge.inria.fr/personal/hritcu/publications/micro-policies.pdf)

Prerequisites

• Coq version v8.9 (https://coq.inria.fr/download)
• The Mathematical Components library v1.9 (http://www.msr-inria.fr/projects/mathematical-components-2/)
• The Extensional Structures library v0.2 (https://github.com/arthuraa/extructures)
• The CoqUtils library, commit ce97408b (https://github.com/arthuraa/coq-utils)

Compiling

make -j

License

This development is distributed under the MIT license (see LICENSE)