An Infrastructure for Faithful Execution of Remote Attestation Protocols

Security decisions often rely on trust.  An emerging technology for gaining trust in a remote computing system is remote attestation.  Remote attestation is the activity of making a claim about properties of a target by supplying evidence to an appraiser over a network.  Although many existing approaches to remote attestation wisely adopt a layered architecture–where the bottom layers measure layers above–the dependencies between components remain static and measurement orderings fixed.  Further, they are often restricted to a specialized embedded platform, or only perform shallow measurements on a component of interest without considering the trustworthiness of its context or the attestation mechanism itself.  For modern computing environments with diverse topologies, we can no longer fix a target architecture any more than we can fix a protocol to measure that architecture.

Copland is a domain-specific language and formal framework that provides a vocabulary for specifying the goals of layered attestation protocols.  It remains configurable by measurement capability, participants, and platform topology, yet provides a precise reference semantics that characterizes system measurement events and evidence handling; a foundation for comparing protocol alternatives.  The aim of this work is to refine the Copland semantics to a more fine-grained notion of attestation manager execution–a high-privilege thread of control responsible for invoking attestation services and bundling evidence results.  This refinement consists of two cooperating components called the Copland Compiler and the Attestation Virtual Machine (AVM).  The Copland Compiler translates a Copland specification into a sequence of primitive attestation instructions to be executed in the AVM.  These components are implemented as functional programs in the Coq proof assistant and proved correct with respect to the Copland reference semantics.  This formal connection is critical in order to trust that protocol specifications are faithfully carried out by the attestation manger implementation.  We also explore synthesis of appraisal routines that leverage the same formally verified infrastructure to interpret evidence generated by Copland protocols and make trust decisions.