Specifying and Verifying Hardware-based Security Enforcement
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
src
.gitignore
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