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 we focused on improvements to MAESTRO, our attestation infrastructure, to enable testbed experiments, flexible mechanisms demonstrations, and use by others.

We completed work on the MAESTRO attestation manager to simplify fielding attestation systems.  A common JSON format for Copland protocols is replacing the Copland concrete syntax for tool interfaces to simplify integration.  A common JSON format for attestation requests and evidence replaces existing ad hoc, tool-specific definitions.  Most significantly, the attestation manager libraries use JSON to define mappings from ASPs to implementations allowing plug-and-play libraries of ASPs.  Finally, a collection of C interfaces is now available for writing ASPs compatible with Copland execution.  Rust interfaces are under development and other languages will be supported upon request. Documentation for the new interfaces may be found at: https://github.com/ku-sldg/copland-avm/wiki

An important property of an attestation manager is the confidentiality and integrity of its signing key.  This key is used primarily for signing evidence to ensure it is reported unmodified by the correct source.  If this key is compromised all attestation results signed with it cannot be trusted.  During this reporting period we completed definition and began implementation of a mechanism to ensure the attestation manager's key cannot be used unless the platform booted SELinux correctly and started a good attestation manager.  IMA is used to gather measurements of the system during boot and extend a TPM PCR with the result.  The signing key is a TPM key that cannot be unsealed unless that PCR holds the correct IMA boot result.  Once running the TPM key will be protected using SELinux policy enforcement.  We are looking at more general alternatives to SELinux, but initial prototypes will take that approach.

Changes to MAESTRO enable both experimentation on our attestation testbed and use of MAESTRO outside our lab.  We can now develop and deliver standard measurement libraries, researchers unfamiliar with CakeML can use the MAESTRO core components without extensive preparation, and the JSON interfaces require little infrastructure support and are available for extending and interfacing with MAESTRO components.

Working with our project champions and colleagues at MITRE we defined an attestation example to be used in demonstrations.  The demonstration target is boot and run-time attestation and appraisal of a cross-domain system.  The demonstration will use Copland and MAESTRO to appraise boot state, appraise Linux with Invary LKIM and perform runtime appraisal of information flow in a cross-domain system.  This demonstration is in the early stages of development, but should be completed during our next reporting period.

Exploration of flexible mechanisms continues defining a taxonomy and a base set of composable mechanisms. This quarter we continued that work, completing an initial taxonomy.  While incomplete, this taxonomy is a solid first step and serves to guide discussion. We identified several attestation styles and began defining mutual attestation as the composition of multiple protocols rather than a protocol itself.  Additionally we began defining an attestation session and the extent of a nonce.  Work will continue on this in the coming quarter.

With the initial MAESTRO updates completed this quarter we will shift our focus to demonstrations and flexible mechanisms next quarter.  We will complete our cross-domain demonstration with MITRE and work with our champions to define additional meaningful demonstrations.  We will complete our trusted boot implementation using TPM keys and SELinux.  We will begin defining standard ASP libraries.  Finally we will continue to explore the flexible mechanisms and our measurement semantics work.

Accomplishments

Accomplishments for this quarter include:

• Completed definition and implementation of JSON interfaces to MAESTRO components
• Completed definition of AM Library formats
• Completed definition and began implementation of AM trusted boot
• Submission of the SEFM'24 paper on MAESTRO system configuration
• Participated in the SoS VI PI meeting in Berkeley, CA

We continue collaborating with our colleagues from MITRE, JHUAPL, and NSA on Copland and the flexible mechanisms. We continue to meet with our NSA Champions on a regular basis.

Publications and presentations

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

Tahat, A., D. Hardin, A. Petz and P. Alexander, “Proof Repair Utilizing Large Language Models: A Case Study on the Copland Remote Attestation Proofbase,” submitted to AI and Programming track at AISOLA 2024, March 10-11, 2024, Aldemar Knossos Royal Resort, Crete.