lthms/speccert

speccert

src
Files
LICENSE
Makefile
README.md
_CoqProject
README.md

SpecCert

SpecCert is a framework for specifying and verifying Hardware-based Security Enforcement (HSE) mechanisms against hardware architecture models. HSE mechanisms form a class of security enforcement mechanism such that a set of trusted software components relies on hardware functions to enforce a security policy.

SpecCert has been described in an academic paper accepted to Formal Methods 2016 conference.

You can compile SpecCert using Coq v8.5pl1 or more. Using a previous version of the proof assistant will probably cause the build to fail.

make       # verify the SpecCert implementation