The view, opinions, and/or findings contained in this report are those of The MITRE Corporation and should not be construed as an official Government position, policy, or decision, unless designated by other documentation.
Copyright 2018 The MITRE Corporation. This technical data deliverable was developed using contract funds under Basic Contract No. W15P7T-13-C-A802.
Approved for Public Release; Distribution Unlimited. Public Release Case Number 18-3576.
Copland Attestation Terms (CATs) provide a means for specifying layered attestations. The terms are designed to bridge the gap between formal analysis of attestation security guarantees and concrete implementations. We therefore provide two semantic interpretations of terms in our language. The first is a denotational semantics in terms of partially ordered sets of events. This directly connects CATs to prior work on layered attestation. The second is an operational semantics detailing how the data and control flow are executed. This gives explicit implementation guidance for attestation frameworks.
This document is generated from Coq sources that contain the proofs of the connection between the two semantics ensuring that any execution according to the operational semantics is consistent with the denotational event semantics. This ensures that formal guarantees resulting from analyzing the event semantics will hold for executions respecting the operational semantics.
Copland Attestation Terms (CATs) provide a means for specifying layered attestations. The terms are designed to bridge the gap between formal analysis of attestation security guarantees and concrete implementations. We therefore provide two semantic interpretations of terms in our language. The first is a denotational semantics in terms of partially ordered sets of events. This directly connects CATs to prior work on layered attestation. The second is an operational semantics detailing how the data and control flow are executed. This gives explicit implementation guidance for attestation frameworks.
This document is generated from a set of proof scripts for the Coq proof assistant. Library Copland.Preamble contains a few tactics that are used throughout the proofs that follow. Library Copland.More_lists contains facts about generic lists in Coq. Many of the lemmas are in support of particular proofs, so the motivation for some is obscure. A notable exception is the definition and lemmas about whether an element x is earlier than y in list l. This will be used to discuss event orderings in traces. A trace is a list of events.
Library Copland.Term precisely specifies CATs and the events that are generated when an CAT is executed. The script also defines annotated terms. To properly distinguish events, each event is associated with a natural number. Annotated terms are used to produce unique natural numbers for events.
Library Copland.Event_system shows our representation of strict partially ordered sets of abstract events. The events are only required to have a function that produces its natural number. Proofs include a demonstration that the relation used to order events is, in fact, a strict partial order. Library Copland.Term_system specializes the event system to the case of CATs and their events.
Library Copland.Trace defines a big-step semantics for CATs. The semantics associates a term, a place, and some initial evidence with a trace. The semantics is specified inductively, mirroring the structure of CATs. The chapter concludes by showing that the order of events in a trace specified by the big-step semantics is compatible with the partial order given by the CAT event system.
Library Copland.LTS defines a small-step semantics for CATs using a labeled transition system (LTS). The proofs in this chapter demonstrate that the LTS (1) computes the correct evidence associated with a term; (2) can always proceed unless it is in a halt state; and (3) always terminates.
Library Copland.Main contains a proof of the main theorem of this work: a trace generated by the small-step semantics is compatible with the partial order given by the associated CAT event system. The main lemma is that every trace generated by the small-step semantics is a trace of the big-step semantics.