Software

Copland AVM

Copland AVM - The Copland Attestation Virtual Machine (AVM) repository includes an implementation in Coq of a formally verified attestation manager. It includes a formal execution environment for attestation protocols specified in Copland along with a proof of refinement from the Copland reference semantics.

Visit on github: https://github.com/ku-sldg/copland-avm

Haskell AM

Haskell AM - A prototype implementation of an attestation manager in Haskell. It is intended more as an experimental platform for rapid prototyping of new features/Copland language extensions (thus is typically ahead of the formal model in the Copland AVM repo)

Visit on github: https://github.com/ku-sldg/haskell-am

CakeML AM

CakeML AM - A (yet-to-be) formally-verified implementation of an attestation manager in CakeML. Includes a set of core attestation services, and also some custom measurers written in C and invoked through the CakeML FFI.

Visit on github: https://github.com/ku-sldg/am-cakeml