  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.
