Research Team Status

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

Project Goals

Our current goals include exploration of Galois Connection models of evidence; exploring semantics of the remote attestation flexible mechanisms; and developing orderings over protocols.

We completed verification of an ordering over protocols based on the difficulty of attack.  An attestation protocol succeeds if it returns evidence that accurately reflects its target's state.  The goal of the adversary is causing attestation to return unrepresentative evidence.  Our goal in examining protocol ordering is establishing when one protocol makes it harder for the adversary than another.  Our ordering uses the Chase model finder to enumerate allowed attacks on two protocols.  Attacks are then compared to determine which protocol is associated with the most difficult attacks.  The ordering is modeled in Coq and verified to be a partial order.  The results of this work have been submitted for publication at FM'23 (see reference below).

We began exploring inclusion of mutually dependent systems in our attestation semantics.  Existing trust models assume an acyclic dependency graph when establishing system trust.  In fact many systems have mutually dependent components.  We began modeling of such mutually dependent systems with the intent of extending our semantics.  The current approach is to isolate mutual dependencies and establish trust in the entire subsystem as a single trust component.  This work is ongoing.

Active exploration of flexible mechanisms continues by working to define a taxonomy for classification.  Currently defined flexible mechanism form an ad hoc collection that we are attempting to organize and extend.  Our current approach considers: (i) who is trusted to handle evidence and perform appraisal; (ii) evidence freshness and caching; and (iii) attestation decomposition.  We are certain these are not exhaustive and are exploring other protocol shapes including mutual attestation and composition.  This work is ongoing with a paper being written.

Accomplishments

Accomplishments for this quarter include:

- Submission of the FM'24 paper on protocol ordering
- Completion of the partial ordering proof for the protocol order.
- New work looking at attestation in the presence of mutually dependent systems
- Progress towards flexible mechanism taxonomy and attestation adversary modeling

Work on the Galois Connection definition for measurement semantics was put on hold for the protocol ordering work.

Adam Petz served as Program Chair for HoTSoS'24.

KU SoS researchers supported the FBI & KU Cybersecurity Conference (https://research.ku.edu/fbi-ku-cybersecurity-conference) April 4.  Featured speakers included Christopher Wray, FBI Director and Senator Jerry Moran. Over 425 participants attended the 1-day event. 

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

Fritz, Anna, Sarah Johnson and Perry Alexander "An Ordering over Attestation Protocols", submitted to 26th International Symposium on Formal Methods (FM'24), September 9th - 13th 2024, Milan, Italy.