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.

Galois Connections have long been used as a model for abstraction in static analysis.  They provide a semantics for modeling when an abstraction from a concrete domain to a abstract domain maintains the semantics of the property being modeled.  Sound abstractions are critical for developing measurements that produce evidence from attestation targets.  This work is critical to our understanding of evidence and evidence over time.  We are doing all our exploration in Coq allowing automation and integration with our work examining protocol ordering.

The flexible mechanisms form the heart of our attempts to scale runtime remote attestation to larger systems.  The flexible mechanisms represent common idioms for attestation and while useful, they are currently organized in an ad hoc fashion.  We are working on a ontology for flexible mechanisms that will define a base set of building blocks and canonical mechanisms for assembling and scaling out attestation environments.

Protocol ordering is a mechanism for determining when one attestation protocol constrains an adversary more than another.  It is used to select from among numerous protocols available for an attestation request.  Our approach is based on collecting attack graphs allowed by a protocol and using a pre-order to select a "best" protocol for a given situation based on that set.  We assume that an attacker chooses the easiest attack to perform and use that attack in a set to rank the associated protocol.

Accomplishments

This is our initial report, thus no formal milestones were defined for this period.  Milestones for next period include:

• Refinement of protocol ordering and Galois Connection models
• Progress towards flexible mechanism taxonomy and attestation adversary modeling

Contributions to foundation cybersecurity research include completion of initial protocol ordering research.  We defined a mechanism for determining when one attestation protocol constrains an adversary more than another.  The approach is based on generating attack graphs associated with protocol using MITRE's CHASE tool and defining a pre-order over those graphs.  This work will be submitted to _Formal Methods 2024_ next month and is the topic of Anna Fritz's recently defended PhD Dissertation.

Broader Impacts of our work currently include support of Invary, a start-up company focused on commercializing LKIM.  We are evaluating their LKIM implementation by integrating into our work while they are using our MAESTRO tool flow as a high-level example of attestation management.

Publications and presentations

Fritz, Anna, "A Formally Verified Infrastructure for Negotiating Remote Attestation Protocols", PhD Dissertation, The University of Kansas, February, 2024