Spotlight on Lablet Research #17 - Scalable Trust Semantics and Infrastructure

Spotlight on Lablet Research #17 -

Project: Scalable Trust Semantics and Infrastructure

Lablet: University of Kansas

Remote attestation has enormous potential for establishing trust in highly distributed IoT and cyber-physical systems. However, significant work remains to define a unifying semantics of remote attestation that precisely defines guarantees that scales to large, heterogeneous systems. Successful completion of this project will result in a science of trust and remote attestation, and prototype infrastructure for building remote attestation systems.

Remote attestation provides boot and run-time capabilities for attesting to system behavior and establishing trust. When using remote attestation, an appraiser requests evidence from a target that responds by performing measurement to gather evidence and adding cryptographic signatures to assure integrity and authenticity. The appraiser receives and appraises evidence to determine if the target is who it claims to be and is behaving as expected.

University of Kansas (KU) researchers, led by Principal Investigator (PI) Perry Alexander, developed an initial specification of an Attestation Monad that describes the formal semantics of attestation. The Attestation Monad is defined as a state monad with exceptions that provide a stateful environment for executing Copland phrases. The Attestation Monad serves as the basic building block for constructing various elements of remote attestation systems. Specified in Coq, the Attestation Monad has well-defined formal semantics that defines requirements for specifying and verifying systems.

Progress on formalizing the Attestation Monad resulted in significant changes in the overall architecture. Each place in a Copland phrase has consistently been defined as an attestation manager modeled as an Attestation Monad. As the research team began modeling attestation patterns and examples, they realized that a place is actually a collection of such monads for negotiation, attestation, and appraisal. Thus, each attestation manager is a collection of these negotiation, attestation, and appraisal services. Decomposing the definition of place and attestation manager in this way maximizes flexibility allowing an attestation manager to only perform a subset of attestation and appraisal operations or use a collection of Attestation Monads to provide flexible infrastructure. Initial models of attestation patterns suggest this approach has great promise in achieving our goal of scalable trust. Researchers extended the attestation manager design to include late launch via key release where attestation manager boot releases keys as trust is established.

KU researchers continued the development and verification of the Attestation Virtual Machine and a compiler from Copland to the AVM. The basic compiler is largely complete and verified in Coq.

Working with MITRE, JHUAPL, and NSA, the KU team has identified an initial set of attestation architecture constructs that include: a) delegated appraisal; b) cached; c) layered; and d) mutual attestation. The expanded team has been working with a set of specific architectures and is moving towards a collection of architecture building-blocks that assemble to define architectures. For example, a layered attestation involves an appraiser delegating appraisal tasks to its subsystems. A cached attestation involves evidence gathered prior to the attestation request. Composing layered and cached attestation results in an architecture where subcomponents update an attestation agent rather than waiting for requests. A layered mutual attestation allows for several mutual attestation steps to build a full attestation result. Researchers are working to identify and specify a set of such architecture constructions that allow defining attestation systems over large systems.

The team has made significant progress on attestation protocol negotiation and policies for defining negotiation and selection. The goal is assuring that the best protocol is negotiated for both appraiser and target that satisfies their local policy. Researchers began defining a lattice of protocols where the lattice partial ordering defines preference for the appraiser or target. Given an attestation request, the best protocol is the local maxima of the intersection of the sublattices formed by those protocols that satisfy the attestation request while respecting local policy. This is important because it captures formally what "best" means, providing a verification condition as we move forward to a more complete model.

Additional details on the project can be found here.