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 development of a cross-domain attestation example; further development of appraisal and evidence semantics; and development of evidence types.  Additionally, we successfully published one paper and submitted a second.

Cross Domain System Demonstration

During the current reporting period we worked with our colleagues and MITRE to develop a significant layered attestation demonstration. The Cross Domain System demonstration uses layered attestation to appraise a system that moves email among domains at different security levels.  Specifically, lt performs email filtering by checking addresses against a rule-base.  The CDS is implemented as a controller, three processes, two buffers and an accompanying SELinux policy.  The three processes inject email messages, perform rule-based filtering, and output filtered results.  The processes communicate using two buffers between the three processes.  SELinux policy enforces information flow requirements by specifying read and write access to  buffers by the three processes.  This is a classic mechanism for implementing secure information flows.

The filtering sequence is run independently for each message.  When a message arrives a controller starts the filtering sequence by kicking off the intake process.  The intake process inputs and writes each message to the first communication buffer.  The intake process then terminates and the filter process starts, reading the message from the buffer.  Filtering is performed using a rule set, results output to the second buffer, and the filter process terminates after writing.  Finally, the output process reads the output message from the second buffer, processes it accordingly, and terminates.

Information flow is enforced by a simple SELinux policy.  Only the intake process can write to the first buffer and only the filter process can read from the first buffer.  Similarly, only the filter process can write to the second buffer and only the output process can read from it.  If the SELinux policy is properly enforced, we know that any processes message flows through the three processes in order.

Attestation will establish remotely that the Cross Domain system is implemented from good parts configured with a good policy. The attestation system is being implemented using the MAESTRO system running multiple attestation protocols.  The first protocol runs an Invary LKIM ASP that gathers evidence for kernel appraisal.  This measurement helps establish that the underlying Linux system is running with integrity.  Once the LKIM measurement is taken, a second protocol runs to measure the CDS.  The protocol begins by gathering the SELinux configuration of each process in sequence.  It then hashes the controller image followed by images of the three processes.  The result is signed by the attestation manager and returned.  Appraisal check the signature, checks hashes of the four binaries, and performs analysis on the SELinux configurations to ensure correct properties are enforced.

As of this report we have implemented the two attestation protocols, several ASPs gathering measurements, and the cross domain system processes and buffers.  The appraisal routines are automatically generated from ASPs and the attestation protocol.  Remaining to be written are the controller, policy appraisal, and additional ASPs.  We anticipate completing this experiment in November and will formally begin experimentation at that time.  We intend to examine ASP ordering and measurement caching to determine if our analytical studies correspond to the implementation.  We will run the experimental system over an extended period to evaluate robustness of MAESTRO tools.  Finally, we will develop a website memorializing the experiment as a working example.  To our knowledge, this will represent the first empirical evaluation of a layered attestation system.

Evidence Semantics

Our work defining evidence semantics made significant strides during the current reporting period.  We defined an appraisal certificate that captures evidence and its appraisal in a signed, replay-able structure.  An appraisal certificate consists of an appraisal policy, evidence, and an appraisal proof all signed by the appraiser.  A relying party receiving the certificate can establish provenance of the appraisal, see evidence, and reply a proof of the appraisal result.

Appraisal policies are recursive in that they can refer to other appraisal certificates.  This tree structure is how a flexible mechanism can define a complex appraisal.  Specifically, the appraisal policy can include evidence and appraisals produced by arbitrarily complex Copland protocols.  Policies like this walk complex evidence structures much like LKIM policies define properties over composite LKIM evidence.

A part of the appraisal certificate's evidence representation is an evidence type.  In a traditional type system, a type statically predicts a construct's type to determine validity of operations.  The Copland evidence type is similar, specifying how raw evidence is interpreted during the appraisal process.  In an attestation result, each evidence value is accompanied by an associated evidence type that defines a static type system over evidence.  Importantly the evidence type describes how the evidence is to be handled, not a set of judgements over all values of that type.

Evidence types support two new kinds of operations critical for appraisal and statically analyzing protocols.  First, we introduce a new Copland primitive for performing appraisal in a Copland protocol.  The new primitive, `appr` or `?`, operates over evidence using the evidence value's type to determine an appraisal mechanism. In the protocol `a->?` evidence generated by `a` is appraised by examining its type in `?` and producing an appraisal result.  This feature reduces the complexity of writing Copland protocols significantly.

Second, new protocol static analysis techniques determine relative protocol quality with respect to attestation goals.  For example, It can be important that attestation information is not lost during protocol execution.  Examples of such loss include returning the empty evidence value, `[]`, dropping all prior evidence, or using the nothing evidence options (-) on both arms of branches. In both cases protocols execute without error, but they lose all information prior to returning nothing.  The resulting appraisals are potentially not as strong because the lost information plans no role in the appraisal.  We anticipate various kinds of analysis such as this resulting from using evidence types.

Accomplishments

Accomplishments for this quarter include:

• Significant progress on a Cross Domain System layered attestation demonstration 
• Continued refinement of an appraisal certificate capturing evidence, policy and appraisal results
• Continued development of a type system for appraisal that supports automated appraisal and protocol analysis
• Acceptance of “Verified Configuration and Deployment of Layered Attestation Managers” at SEFM'24 on MAESTRO system configuration
• Submitted "Ordering Attestation Protocols" to CPP'25 on a formal definition of Copland attestation protocol ordering

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.

Next Quarter

Next quarter we will:

• Complete the initial implementation of our Cross Domain demonstration
• Develop the attestation certificate and work on certificate morphisms
• 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.

Scott, S., A. Fritz and P. Alexander, "Ordering Attestation Protocols," submitted to Certified Programs and Proofs (CPP'25), January 20-21, 2025, Denver, CO.