Research Team Status

- Perry Alexander, Principal Investigator
- Adam Petz, Member Technical Staff
- Sarah Johnson, PhD Student
- Will Thomas, PhD Student

Project Goals

Our project goals include exploration of evidence semantics, flexible mechanisms, and empirical studies.  This quarter development and evaluation of a layered attestation system for the Cross Domain System (CDS) demonstration continued, focusing on defining implementation heuristics for runtime attestation systems. A partial fix was implemented to address a vulnerability in boot measurement, and a new automated installation system for MAESTRO was developed. Additionally, work progressed on a static analysis capability for Copland protocols, including defining a type system and semantics for evidence.  Finally, exploring protocol ordering attestation protocols continued with the addition of multi-sets and ordering of attacker actions as proposed earlier.

Accomplishments

Cross Domain System Demonstration

During the current reporting period, we worked with our colleagues at MITRE and our NSA Champions to continue development and evaluation of a layered attestation system. As reported in the previous three quarters, the Cross Domain System (CDS) demonstration uses layered attestation to appraise a system that moves messages among security domains. Specifically, it sanitizes messages using a rewrite rule base and filters messages to determine when they should be released. Appraisal ensures CDS data flow is not compromised by attacks on the CDS itself or its attestation infrastructure.

We worked with MITRE and NSA to define a collection of maxims or rules of thumb for designing and implementing runtime attestation systems:

• Maxim 1. Constrain possible interactions so attested properties depend only on limited, predictable, measurable parts of the system.
• Maxim 2. Short-lived, single-input processes avoid the need for process runtime remeasurement that long-lived services require if they handle untrusted inputs.
• Maxim 3. Attestation should be independent of secrets that could be disclosed by transient corruptions, lest transient corruptions cause permanent attestation failure.
• Maxim 4. Each attestation must display characteristics showing that it originated from our intended attestation software, a process running under a trustworthy system boot.
• Maxim 5. An acyclic dependency relation enables us to measure lower layers before components depending on them.  Only very recent corruptions of underlying components can then undermine attestations, meaning corruptions during the course of attestation.

Our maxims are general and apply to all types of attestations, including the CDS we use as a working example.  We have integrated our new definitions into our working paper on CDS attestation.  Additional attestation cases will be explored in the course of publishing the CDS work.  While the Principles of Remote Attestation provide a definition of what constitutes a good attestation, the maxims define implementation heuristics helpful in achieving good attestation.

Last quarter, we discovered that if a system can be booted into a bad state and the attestation manager successfully accessed, the key blob may be exposed and used by an adversary to sign bad evidence after rebooting into a good state.  We updated our requirements to include TPM policy encryption with a key held by a trusted third party.  Before the blob can be used to reproduce the TPM signing key, the TPM policy must be successfully decrypted and correctly installed.  This is not a fail-safe solution, as this process might still be compromised.  However, it does make accessing the blob in a bad state significantly more difficult.  A simpler and potentially more effective remedy is denial of physical access to the hardware platform.

Continuing to improve MAESTRO's usability, we developed an automated installation system based on `opam` that installs and updates our environment and libraries.  The installer has been used successfully by our DARPA and Honeywell partners.  We largely completed a vscode plugin for Copland protocols that provides traditional syntax checking and highlighting.  We are in the final stages of generating the standard Copland JSON representation from Copland source that will serve as an integration point for all our Copland tools.

The CDS demo and associated publication efforts remain a central focus of our discussions with NSA and MITRE.  We continue to meet bi-weekly to discuss publication and to refine concepts.  One difficulty has been separating attestation from CDS implementation.  The CDS system is an example developed by MITRE for demonstrating remote attestation, not a proposed CDS implementation.  We are working on publications that do a better job of clarifying the distinction between attestation techniques and good CDS implementations.

Static Analysis

Last quarter, we began developing a type system and static analysis capability for Copland protocols.  Recall that the objective of a type system is predicting the behavior of code statically.  In this spirit, our goal is developing a type system and static analysis tools to predict the behavior of Copland protocols in the context of the system they measure.

• Flow Integrity - All evidence comes from the correct source, and none is discarded.
• Appraisability - A measurement target can be fully measured and appraised.
• Roots-of-Trust - Discovering and classifying roots-of-trust.
• Executability - Can run on a target system.
• Sufficiency - Evidence gathered is sufficient for trust analysis.

Two updates to Copland are required to implement a checker for these properties: (i) type annotations for Copland phrases; and (ii) representation of the measurement target.

An initial definition of a Copland type system is proposed that documents information flow through ASPs and defines structural properties of evidence.  ASP information flow is captured in Hoare-style definitions of pre-conditions and post-conditions.  These requirements define how information is manipulated rather than the correctness of measurements.  Integrated in a protocol, these annotations support analysis to determine provenance and sufficiency.  As a part of defining ASP requirements, we also define a semantics for evidence structure.  Prior definitions of Copland said little about the structure of evidence aside from bundling properties.  The new type system allows evidence comparison and composition in principled ways.

Determining measurability and executability requires a representation of the target system.  Copland is thus being extended to include an abstract model of data flow and measurement dependency to accompany a protocol.  Using a system model in this way is referred to as *system-informed analysis* and we believe is unique to Copland.  Specifically, having both the protocol and the target system input to the static type analysis.

Roots-of-trust analysis is a novel way to classify and find roots of trust.  Traditional attestation systems define roots-of-trust as system assumptions.  Components like TPMs or firmware are asserted to be trusted *a priori* and the design proceeds from there.  Additionally, loops in the trust chain are explicitly forbidden.  Our approach will flip the traditional technique and identify roots-of-trust from the system configuration.  One output of static analysis will be a list of components that are trusted implicitly.  The designer may then decide if those components are trustworthy.  Our approach will also allow for cyclic roots-of-trust.  While cycles are not desirable, they often exist in real systems.  We will identify collections of interdependent components that together define a composite, trustworthy subsystem that may be treated as a root-of-trust.

The ultimate objective of this task is implementing a static type checker for Copland protocols and target systems.  The checker will be verified with respect to required properties defined previously.  Initially, we are working on Rocq to develop requirements and basic algorithms with the intent of extracting an implementation.  Such a checker would be a significant contribution to our goal of predictable attestation systems.

Protocol Comparison

During the current reporting period, we worked on further automation and verification of our protocol ordering formalism.  As previously reported, the initial algorithm made two simplifying assumptions: (i) each action taken by the attacker occurs once; and (ii) all actions require the same level of effort by the adversary.  Over the past two reporting periods, we have taken steps to loosen these assumptions to improve the precision of our algorithm.

This quarter, we completed ordering proofs using a multi-set formalism to represent an adversary repeating actions rather than the original set representation.  This required developing a multi-set library for Rocq, including definitions of traditional multi-set operations as well as relations specific to defining the ordering, including supports and covers.  We established that the new multi-set formalism produces the same results as the set formalism in early experiments while extending the ordering to more complex adversaries.  We captured this work in a paper being submitted to *Tools and Algorithms for the Construction and Analysis of Systems*.

This quarter we continued working with orderings of attacker actions.  Recall that early experiments only considered time constraints on actions rather than the complexity of the actions themselves.  This quarter we began including relative complexity of individual attacks.  Each attacker's actions are specified along with a partial order over those attacks to define relative difficulty of executing the action.  Last quarter we established a basic framework for including attack difficulty.  This quarter we began implementing and verifying the framework in our Rocq model.  Thus far work is proceeding as expected, but is not complete.  We remain confident we will complete verification successfully.

Last quarter we reported adding attack action ordering supports defining a maximum effectiveness or fixed point of a protocol.  This quarter we continued to refine this concept, but significant formalization challenges remain.  We hope to complete an initial model and algorithm for finding fixed points in the next reporting period.

Accomplishments

Accomplishments for this quarter include:

• Generalized lessons learned in developing a CDS measurement capability to a collection of attestation design maxims.
• Provided a partial fix to a vulnerability in boot measurement where a bad boot compromised confidentiality of the AMs signing key.
• Continued the use of multi-sets to provide a more flexible model of attacker behavior.
• Continued work to formalize a maximally strong protocol instance in Rocq.
• Began definition of a static checker for Copland protocols.
• Proposed an initial semantics for Copland evidence.
• "Layered Attestation in Action: Attesting to a Cross-Domain Solution" submitted to NDSS'25.
• "Ordering Attestation Protocols" submitted to TACAS’26.

Publications and presentations

We submitted two papers this quarter to NDSS and TACAS.  The NDSS paper was not selected and is being revised.  The TACAS paper is currently under review.