Research Team Status

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

We continue collaborating with our colleagues from MITRE and NSA who were instrumental in defining the CDS demonstration.  We continue to meet with our NSA Champions on a bi-weekly basis. 

Project Goals

Our project goals include exploration of evidence semantics, flexible mechanisms, and empirical studies.  This quarter we continued focus on completion of an empirical study of a Cross Domain System (CDS) layered attestation system and developing static analysis tools for attestation protocols. Additionally, we submitted one paper to CCS'25 and had presentations accepted at HCSS'25 and LSS'25.

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 last quarter, 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 by checking addresses. Appraisal ensures CDS dataflow is not compromised by attacks on the CDS itself or its attestation infrastructure.

Last quarter we reported successful implementation of the prototype and attestation system.  This quarter we refined the demonstration, moving to a virtual machine running Fedora for ease of use.  Our most significant results involved experimenting with the system, stressing the attestation system and the CDS itself.  We also revised the boot story to create a stronger chain of trust from system boot to runtime attestation and implemented periodic measurement of installed SELinux policy.

We continued using the MAESTRO tools to build our attestation system including: (i) trusted boot using a TPM, IMA and SELinux; (ii) Linux kernel integrity checking using Invary's LKIM; (iii) SELinux policy integrity checks at runtime; (iv) integrity checks of all CDS binaries; and (v) integrity checks of all CDS component configuration files.  This quarter we added z3 verification of the boot sequence and finalized TPM usage to protect the AM's signing key.

Trusted boot measures the initial system and establishes a signing key for the attestation manager.  This key remains resident in the TPM and is protected by sealing to PCRs.  This quarter we refined the early boot process to ensure the AM can access its key only when good IMA and SELinux policies are installed.  These policies are measured by the boot loader using a simple script that extends PCR 9.  However, we must ensure the boot loader runs that script before starting the rest of the system.

Linux boots from a RAM disk identified as initramfs - Initial RAM File System.  The boot loader measures initramfs as a part of starting the OS.  To ensure the correct policy measurement script runs, it is placed in the initramfs image and included in the boot loader.  If the policy measurement script is modified, the measurement of initramfs will be wrong and PCR 9 used to seal the AM's key will contain a bad value.  Thus, the key will not be available.  This quarter we fully implemented and tested the early boot process to ensure proper key protection.  Additionally, we used the z3 prover to ensure the sequencing of measurements correctly protects the AM's signing key.

Our most important layered attestation accomplishment this quarter is the empirical testing of the CDS attestation system and the beginnings of a Design for Attestation workflow.  Here we summarize attacks against the CDS Target system and whether they are detectable by our Layered Attestation system. The first column lists the major components, ascending from the deep and hard to attack Hardware to the shallow and easier to attack user-space CDS Components.

The second column indicates whether an attack on the Configuration of a component is detectable by our Layered Attestation System. This type of attack primarily manifests as modification of a key input or data dependency of a component; often a policy to specialize the component. The TPM configuration is a somewhat special case, as it is not directly observable by the Layered Attestation System. Rather, proper configuration of the TPM indicates protection of the strongly bound signing key: controlled utilization of the key to the attestation manager ensures that evidence is signed only when the TPM configuration has been measured and verified.

The third and final column indicates whether an attack on the Behavior of the component is detectable by our Layered Attestation System. Such attacks on component behavior are best characterized by changing the component to perform a different function than it was designed to perform. For example, an Attestation Manager binary could be replaced with a different binary that performs measurements that are incomplete or out of order; however such an action would be detected by IMA. In general, it is harder to detect behavior violations the deeper in the system you go; fortunately, in general, the deeper you go, the harder it is to attack.

Of particular note is the tipping point where behavior attacks shift to being undetectable. If LKIM’s behavior is modified such that it does not properly measure the kernel, then the kernel can be modified and the LKIM evidence will not be able to detect it. Evidence from an LKIM measurement where such corruption has occurred will lead the attestation to believe the system is trustworthy, when in reality an adversary managed to perform a timely corruption of a deep system component.

Results of testing and design decisions made yield a non-exhaustive set of
attestation design heuristics:

• Protect a strongly-bound attestation signing key as deep in the system as possible, preferably by a root of trust
• Protect the utilization of the attestation signing key behind evidence of a good boot
• Measure targets in order of dependencies and layers. Components of a deeper layer should be measured before components of a shallower layer
• Start target processes exactly when needed and do not let the process live longer than is necessary. Runtime attestation is simpler when the target process is short-lived and evidence of it starting in a known good state is available
• Utilize well-defined and verified measurement infrastructure and measurement protocols to provide confidence in the integrity of the evidence gathered by running the protocol on said infrastructure
• The target of attestation and the attestation subsystem should be independent. Implicit in each attestation request should be evidence of the attestation subsystem’s integrity

As our work progresses we will continue to gather these heuristics in an attempt to define a Design for Attestation workflow.

We have submitted results from this work to CCS'25 and have accepted presentations at HCSS'25 and LSS'25.

Evidence Semantics

Our use of CHASE analysis to compare attack graphs allowed by attestation protocols yielded significant results this past quarter.  Recall that last quarter we began comparing protocols by looking at attacks that they cannot detect.  Specifically, for each protocol we determined the easiest allowed attack as defined by its allowed attack graphs.  The easiest attack graph is defined as being the simplest for an adversary to execute.  Then we compare protocols by comparing the easiest attack they allow.

During the last quarter we discovered that sets of attacks did not allow for multiple actions of the same type.  While our comparison was sound, it did not extend to all possible attack graphs.  In particular, it did not include attack graphs where the same adversary or target action occurs more than once.  To address the set limitation, we are now working with partially ordered multisets rather than partially ordered sets.  We have updated out theories appropriately and are reverifying ordering properties as needed.

An unanticipated result is that the protocol ordering is algorithmic.  Specifically, there is a decision procedure that determines the ordering over two protocols.  Our intuition was that the ordering was semi-decidable at best.  We were able to implement the ordering decision in Coq and now use it to quickly compare protocols during development.  This result means that when we have completed the theoretical framework we will have an algorithm to integrate into Copland protocol tools to perform comparison.

We are submitting preliminary ordering results to ESORICS'25 this month.

Accomplishments

Accomplishments for this quarter include:

• Completed and verified the early boot trust argument for the CDS layered attestation demonstration.
• Performed initial empirical analysis of attacks on the CDS layered attestation demonstration
• Developed an algorithm for comparing the relative strength of two Copland attestation protocols and implemented the algorithm in Coq

Impacts

We had a number of significant accomplishments impacted by our research:

• 2025 FBI and KU Cybersecurity Conference - Over 420 individuals attended the 3rd annual edition of this conference held at KU.  The conference targets working professionals and has grown each year it has been held.  KU researchers including our VI researchers are active in planning and executing the conference.
• Invary Seed Round - Our attestation spinoff company Invary completed its seed funding round.  Invary is commercializing the LKIM system currently and looks to commercialize results from our VI research.
• MASTRO Users - The first users outside our research group successfully used the MAESTRO tool infrastructure to field a simple layered attestation system.  We are particularly pleased they accomplished this with no input from our team.  More details available upon request.

Publications and presentations

• "An Experiment Using Layered Attestation" accepted to HCSS'25 as a full presentation.
• "Layered Attestation of a Cross-Domain System" accepted to LSS'25 as a full presentation.
• "Layered Attestation in Action: Attesting to a Cross-Domain Solution" submitted to CSS'25.