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.  We recently established a research agreement between KU and Invary, LLC to commercialize layered attestation infrastructure.

Project Goals

Our project goals include exploration of evidence semantics, flexible mechanisms, and empirical studies.  This quarter we focused primarily on completion of a Cross Domain System (CDS) layered attestation demonstration and automated analysis of protocols from the CDS demonstration. Additionally, we presented one paper, submitted a HoTSoS presentation, and prepared a proposal for an HCSS presentation.

Cross Domain System Demonstration

During the current reporting period we worked with our colleagues at MITRE and our NSA Champions to complete development of a significant layered attestation demonstration. 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 will ensure the CDS dataflow is not compromised by attacks on the CDS or attestation infrastructure.

The updated CDS is implemented as four processes.  It includes buffers between processes and accompanying configuration files and SELinux policy. The processes inject messages, perform rule-based sanitizing, perform address filtering, and output filtered results.  The processes communicate using buffers between the filtering processes with SELinux policy enforcing information flow requirements by specifying read and write access to  buffers by the processes.

A number of design changes were implemented this quarter.  Each CDS component is configured using a separate configuration file and the original controller has been eliminated.  Configuration files define rules for rewriting and addresses for filtering and are read each time the process runs.  The controller is eliminated by adopting a continuation passing style mechanism in the filter processes.  The filtering sequence is run independently for each message and remains largely unchanged.  When a message arrives the intake component starts the filtering sequence.  The intake process inputs and writes each message to the first communication buffer and invokes the rewriter.  The rewriter processes the message, outputs to the second buffer, and starts the address filter.  The address filter writes to a third buffer that is read by the output process.  Finally, and output process writes to the receiving domain. Information flow is enforced by a simple SELinux policy as described last quarter.

This quarter we implemented attestation that establishes the Cross Domain System is implemented from good parts configured with a good policy.  We used our MAESTRO tools to implement an attestation system that includes: (i) trusted boot using a TPM and IMA; (ii) kernel integrity checks using Invary's LKIM; (iii) SELinux policy integrity checks; (iv) integrity checks of all binaries; and (v) integrity checks of configuration files.

Trusted boot measures the initial system and establishes a signing key for the attestation manager.  The signing key is a TPM key sealed to a system boot record generated by the Integrity Measurement Architecture (IMA).  The IMA policy captures hashes of components as they start and creates composite in a TPM PCR.  Because the signing key is sealed to the IMA measurement the key cannot be used if the system boots with bad components.  This includes the attestation manager itself.  An encrypted credential is generated for the attestation manager that authorizes the TPM to use the attestation manager's signing key.  The TPM key never leaves the TPM.  The credential is protected by SELinux policy and never leaves the attestation manager. This initialization ensures a signature using attestation manager's key ensures: (i) data integrity; (ii) boot integrity; and (iii) authenticity because only correct attestation manager could generate the signed evidence.

Following boot, the attestation protocol runs an Invary LKIM ASP that gathers evidence for kernel appraisal.  This measurement establishes that the underlying Linux system is in a good runtime state.  To maximize trust, LKIM does a fresh measurement of the kernel.  If system resources or time are an issue, LKIM can use cached measurements.  IMA ensures the right SELinux system started while LKIM ensures the system stays in a good state at runtime.

Once the LKIM measurement is taken CDS components are measured. The protocol begins by gathering the SELinux configuration for comparison to a golden value.  This ensures the correct MAC policy is loaded and enforced.  It then hashes images of the CDS processes and their associated configuration files.

The attestation results are bundled together and signed by the attestation manager for external appraisal.  This signed evidence bundle represents a picture of the CDS runtime state.  Appraisal first checks the signature produced by the attestation manager to ensure a good protocol execution and bundling.  It then checks the LKIM measurement using Invary appraisal tools.  The SELinux policy hash is checked to ensure good policy enforcement.  Finally, the hashes of each binary and configuration file in the CDS are compared with golden hashes.  These golden values are required for each measurement and are generated during a provisioning boot.

As of this reporting period we have completed a full implementation of the CDS and its associated attestation system.  The CDS is implemented as a collection of OCaml programs written by MITRE and the attestation system is generated using MAESTRO tools around our verified attestation manager.   Attestation Service Providers (ASPs) for the attestation manager are written in Rust using our standard ASP templet.  The demonstration is operational and will detect a broad collection of simple attacks.

The demonstration is significant as a concrete demonstration of layered attestation and evidence bundling.  Specifically, the TPM serves as a root-of-trust for key establishment and storage.  The IMA boot attestation process builds an appraisable measurement of the operating platform that is protected by the TPM.  LKIM builds from attested boot to establish runtime trust in the underlying operating system and SELinux.  Finally, the CDS measurements depend on trust in SELinux enforcement and Linux functionality to perform sound attestation.  This layering is reflected in evidence bundling.

It is our intent to demonstrate the CDS attestation system and provide an overview at the January VI meeting.

Evidence Semantics

To accompany our CDS demonstration we used results from CHASE analysis to understand attacks that could evade our attestation process.  CHASE is a model finder written by MITRE with a library that processes Copland protocols.  Starting with a collection of assumptions and dependencies it evaluates a Copland protocol to find sequences of actions that result in undetected attacks.  CHASE is being used on our CDS protocol and the CDS system to find attacks we can use to exercise our attestation implementation.

CHASE work is ongoing with only preliminary results to report.  We have generated a set of attack graphs and are working to translate those graphs into attack implementations in the form of shell scripts.  This collection of attacks will then serve as an evaluation suite for the attestation system.  It is anticipated we will have results from this analysis in the first quarter of 2025.

Accomplishments

Accomplishments for this quarter include:

• Completed a layered attestation demonstration for a Cross Domain System (CDS).
• Performed initial formal analysis of protocols for the CDS demonstration
• Presented “Verified Configuration and Deployment of Layered Attestation Managers” at SEFM'24 on verified MAESTRO system configuration
• Submitted "Verified Configuration and Deployment of Layered Attestation Managers" to HoTSoS'25 as a works already published presentation.
• Prepared "An Experiment Using Layered Attestation" to HCSS'25 as a full presentation.  To be formally submitted January 31.

Next Quarter

Next quarter we will:

• Develop a set of attacks for evaluating the CDS demonstration using CHASE analysis
• Develop a public facing tutorial-style CDS demonstration presentation on the Copland website
• Document evidence types and begin identifying automated analysis
• Continue development and maintenance of the MAESTRO infrastructure

Publications and presentations

Petz, A., W. Thomas, A. Fritz, T. Barclay, L. Schmalz, and P. Alexander, “Verified Configuration and Deployment of Layered Attestation Managers,” 22nd International Conference on Software Engineering and Formal Methods (SEFM’24), November 4–8, 2024, Aveiro, Portugal.