Formally Verified Bundling and Appraisal of Layered Attestation Protocols

Remote attestation is a technology for establishing trust in a remote computing system.  Core to the integrity of the attestation mechanisms themselves are components that orchestrate, cryptographically bundle, and appraise measurements of the target system.  Copland is a domain-specific language for specifying attestation protocols that operate in diverse, layered measurement topologies.  In this work we formally define and verify the Copland Compiler and Copland Virtual Machine for executing Copland protocols to produce evidence.  Appraisal is a dual un-bundling procedure over the raw evidence segments produced by arbitrary Copland-based attestations.  All artifacts are implemented as monadic, functional programs in the Coq proof assistant and verified with respect to a Copland reference semantics that characterizes attestation-relevant event traces and cryptographic evidence shapes.  Appraisal soundness is positioned within a novel end-to-end workflow that leverages formal properties of the attestation components to discharge assumptions about honest Copland participants.  These assumptions inform an existing model-finder tool that analyzes a Copland scenario in the context of an active adversary attempting to subvert attestation.  An initial case study exercises this workflow through the iterative design and analysis of a Copland protocol and accompanying security architecture for an Unmanned Air Vehicle DARPA demonstration platform.  We conclude by instantiating a more diverse benchmark of attestation patterns called the “Flexible Mechanisms for Remote Attestation”, leveraging Coq's built-in code synthesis to integrate the formal artifacts within an executable attestation environment.