MAESTRO: Measurement and Attestation Execution and Synthesis Toolkit for Remote Orchestration

ABSTRACT

The ultimate goal of a sound attestation process is to establish the integrity of a target of measurement - one or more components on a target system whose integrity is of interest to the consumer of an attestation. Copland is a domain- speci c-language for specifying remote attestation protocols with primitives for layered measurement, remote requests, and cryptographic evidence bundling. While the explicit semantics of Copland provide a vital shared vocabulary for attestation, its high-level nature leaves many details of component deployment, protocol execution, and trust analysis under-specified. In this work, we present the design and implementation of a Copland-based toolsuite called Maestro that supports an end-to-end attestation pipeline from protocol negotiation through evidence appraisal. Formal analysis and synthesis techniques play a key role throughout to justify soundness and deploy executable artifacts on real systems.

A fundamental challenge of protocol negotiation is the tension between the target's desire for constrained disclosure and the requester's desire for comprehensive measurement. To address these and other challenges, we introduce a Copland-based negotiation scheme and its goals of sound and su cient protocol selection. Owing to the distributed nature of negotiation, we discuss initial efforts to synthesize CakeML implementations of local policy engines that guarantee protocol executability and evidence disclosure. Moving from negotiation to attestation, the Copland Virtual Machine (CVM) and its dual appraisal procedure interpret arbitrary Copland language terms by dispatching measurements, then bundling, reporting, and unbundling evidence during appraisal. Proofs in Coq ensure precise ordering of measurement traces and cryptographic strength of the procedures that handle intricate, layered evidence structures.

While the formal semantics of protocol negotiation and execution support soundness for a wide range of attestation scenarios, each makes assumptions about the safety and sufficiency of the environment in which they operate. For example, negotiation must reason about available measurement services and their interaction; the CVM should be con gured likewise to access measurement re- sources. To make these architectural assumptions explicit, we propose a Copland manifest that denotes a componentized security architecture and con guration items necessary for initializing attestation managers (or collections of AMs). An accompanying manifest compiler aims to ease deployment of common attestation patterns by transforming high-level architecture descriptions into system images that provably support Copland executions. We will conclude with a survey of formal results about manifests that cross-cut protocol negotiation, deployment, execution, appraisal, and trust analysis.

Author

Adam Petz is an Assistant Research Professor of Computer Science at the University of Kansas and the Institute for Information Sciences (I2S).  His research interests lie at the intersection of formal methods, programming language semantics, functional programming, trusted computing, and systems security.  During his time as a student and professional researcher, he has contributed to a number of successful federally-funded research efforts that include the DARPA Cyber Assured Systems Engineering (CASE) effort, and the NSA Science of Security lablet.  Adam completed his PhD at the University of Kansas in June 2022, and prior to that a Master's in CS in 2016 and two B.S. degrees in CS and Mathematics at Emporia State University in 2014.