An Infrastructure for Faithful Execution of Remote Attestation Protocols
This work provides a formally verified infrastructure for faithfully executing remote attestation protocols, which is critical for establishing trust in remote computing systems for security-conscious domains.
This paper defines and verifies a Copland Compiler and Virtual Machine for executing Copland protocols, a domain-specific language for remote attestation. The compiler translates Copland into instructions for the virtual machine, both implemented and verified in Coq, and an Attestation Manager Monad is introduced to manage protocol execution.
Remote attestation is an emerging technology for establishing trust in a remote computing system. Copland is a domain-specific language for specifying layered attestation protocols, characterizing attestation-relevant system events, and describing evidence bundling. In this work we formally define and verify a Copland Compiler and Copland Virtual Machine for executing Copland protocols. The compiler translates Copland into instructions that are executed on the virtual machine. The compiler and virtual machine are implemented as monadic, functional programs in the Coq proof assistant and verified with respect to the Copland event and evidence semantics. In addition we introduce the Attestation Manager Monad as an environment for managing Copland term execution providing support for managing nonces, binding results of Copland protocols to variables, and appraising evidence results.