Layered Attestation of a Cross-Domain System

### Overview Perry Alexander from the University of Kansas presents work developed alongside students, MITRE collaborators (Josh Guttman, Paul Rowe), and NSA colleagues (Jim Carter, Steve Smalley, Daniel DeGraaf) on building an end-to-end, layered semantic remote attestation architecture. The goal of the project was to construct a functioning system spanning from hardware boot through runtime measurement and empirical testing. To validate their approach, the team targeted a realistic, third-party cross-domain email cleansing pipeline written in OCaml, designing an attestation framework that binds boot-time guarantees directly to runtime evidence collection.

### Key Topics - **Layered Architecture & Roots of Trust:** Grounded in principles outlined by Coker et al., the system builds upward from a hardware root of trust (TPM 2.0 and EFI firmware) through an operating system layer (Linux, SELinux, IMA), up to a Measurement and Attestation (M&A) subsystem, and ultimately the target application. - **Attestation Manager & Copeland Language:** Attestation workflows are specified using the Copeland attestation protocol language and executed by a formally verified attestation manager within the Maestro framework. - **The Attestation Manager Signing Key:** A foundational mechanism linking boot state to runtime attestation by sealing an attestation manager signing key to specific TPM Platform Configuration Registers (PCRs). - **Design for Attestation:** Structuring target software components (such as rewrite and filter stages) to start, process, and terminate rather than running persistent daemon processes, significantly simplifying runtime state appraisal by shifting the verification burden to configuration files and static binaries. - **Empirical Attack Testing & Analysis:** Using MITRE's Chase tool to enumerate protocol attack paths and validate detection capabilities against configuration and binary tampering.

### Technical Details - **Boot Chain and PCR Measurements:** EFI firmware initializes measurement into PCR 4 (bootloader), while the bootloader measures initramfs into PCR 9 and the command line into PCR 8. Inside initramfs, a specialized script hashes the IMA policy and SELinux policy into PCR 11. PCR 10 is populated by IMA but excluded from sealing due to unpredictable runtime variation. - **Key Protection and Sealing:** The attestation manager signing key blob resides in user space, protected by SELinux and IMA. The key is sealed to PCRs 4, 8, 9, and 11 in the TPM 2.0. The TPM unseals and loads the key only if the bootloader, initramfs, command line, and security policies match expected values. Consequently, any signature produced with this key cryptographically proves that the attestation manager ran on a correctly booted system. - **Measurement Pipeline:** The runtime protocol invokes Attestation Service Providers (ASPs) strictly ordered via Copeland sequential semantics: first verifying kernel/SELinux integrity with Invariant Corporation's LKIM (Linux Kernel Integrity Measurement) tool, appraising running SELinux policy, hashing configuration files, and finally hashing statically linked application binaries before signing the evidence bundle. ASPs are constrained to read-only operations and verified via IMA.

### Takeaways & Future Directions - **Formal Verification Benefits:** Formally verifying the compact attestation manager proved far more tractable than verifying complex target applications, ensuring that Copeland protocols execute with strict fidelity. - **Bridging Boot and Runtime:** Binding user-space signing capabilities directly to TPM-sealed PCR states provides a robust bridge from boot-time measurements to runtime attestation bundles. - **Open Challenges:** Significant engineering challenges remain in provisioning and distributing known-good reference hashes across heterogeneous hardware, managing updates/live patching without breaking PCR states, conducting runtime memory introspection for dynamic processes, and scaling layered attestation across broader enterprise environments.