An Infrastructure for Faithful Execution of Remote Attestation Protocols

Remote attestation is a technology for establishing trust in a remote computing system. Copland is a domain-specific language for specifying attestation protocols that operate in diverse, layered measurement topologies. An accompanying reference semantics characterizes attestation-relevant system events and bundling of cryptographic evidence. In this work we formally define and verify the Copland Compiler and Copland Virtual Machine for executing Copland protocols. The compiler and vm are implemented as monadic, functional programs in the Coq proof assistant and verified with respect to the Copland reference semantics. In addition we introduce the Attestation Manager Monad as an environment for managing attestation freshness, binding results of Copland protocols to variables, and appraising evidence results. These components lay the foundation for a verified attestation stack.