Micro-Policies in Coq

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)

make -j

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

Name	Name	Last commit message	Last commit date
Latest commit arthuraa Update to newest versions. Sep 23, 2019 2816316 · Sep 23, 2019 History 1,017 Commits
cfi	cfi	Port to Coq 8.8; use Extensional Structures.	May 16, 2018
common	common	Port to Coq 8.8; use Extensional Structures.	May 16, 2018
compartmentalization	compartmentalization	Port to Coq 8.8; use Extensional Structures.	May 16, 2018
concrete	concrete	Port to Coq 8.8; use Extensional Structures.	May 16, 2018
extraction	extraction	Update to newest versions.	Sep 23, 2019
ifc	ifc	Update to newest versions.	Sep 23, 2019
lib	lib	Port to Coq 8.8; use Extensional Structures.	May 16, 2018
memory_safety	memory_safety	Update to newest versions.	Sep 23, 2019
os	os	Some diagrams of the OS's compartmentalization	Jun 30, 2015
sealing	sealing	Port to Coq 8.8; use Extensional Structures.	May 16, 2018
symbolic	symbolic	Update to newest versions.	Sep 23, 2019
testing	testing	Qualify string library imports.	Feb 19, 2015
.gitignore	.gitignore	Some diagrams of the OS's compartmentalization	Jun 30, 2015
LICENSE	LICENSE	Port to Coq 8.6 and new nominal library.	Mar 15, 2017
Makefile	Makefile	Delete emacs configuration file.	Aug 17, 2016
README.md	README.md	Update to newest versions.	Sep 23, 2019
_CoqProject	_CoqProject	Port to newest version of coq utils.	Sep 19, 2017

Provide feedback