Semantics, languages and tools for layered attestation


Use Cases for Remote Attestation

Ian D. Kretz, John D. Ramsdell, and Paul D. Rowe
The MITRE Corporation

This note presents a series of use cases for remote attestation. Each includes a number of Copland phrases that specify how relevant target components are measured and by whom, the order in which these measurements occur, and how the evidence produced by these measurements is bundled together.

Associated with each example Copland phrase is an XHTML document that visualizes the phrases’s abstract syntax tree and shows how evidence is accumulated as the phrase executes, culminating in the final evidence that characterizes the phrase. These documents can be generated by running make in the directory that contains this README.

The categories of use case are:

We repeatedly rely on an incremental approach to writing Copland phrases, starting from simpler ones whose correctness is easily verified and gradually building up complexity. We generally advocate for such an approach to writing phrases.

What follows is an introduction to Copland phrase syntax and semantics. The section on semantics helps interpret the XHTML document generated from a Copland phrase. We assume the reader is familiar with Orchestrating Layered Attestation. What is presented here is a slight variation of what is described in the paper.

Copland Syntax

A symbol is a lowercase letter optionally followed by letters, digits, and underscores. The syntax of a Copland phrase is



PHRASE  ::= SYMBOL PLACE SYMBOL      -- Measurement (probe place target)
         |  {}                       -- Null
         |  _                        -- Copy
         |  !                        -- Signature
         |  #                        -- Hash
         |  @ PLACE PHRASE           -- At place
         |  @ PLACE [ PHRASE ]       -- At place with brackets
         |  PHRASE -> PHRASE         -- Linear sequencing
         |  PHRASE BRANCH PHRASE     -- Sequential and parallel branching
         |  ( PHRASE )

BRANCH  ::= -<- | +<- | -<+ | +<+    -- Sequential
         |  -~- | +~- | -~+ | +~+    -- Parallel

The initial place P is specified using *P:, and this place defaults to p0 when left unspecified.

The @ operator has the lowest precedence, the branching operator is non-associative and has medium precedence, and linear sequencing operator is right associative and has the highest precedence. Thus

*p0: @p1 kim p2 ker -> ! -<- @p2 (vc p2 sys) -> !

Is equivalent to

*p0: @p1 (((kim p2 ker) -> !) -<- (@p2 ((vc p2 sys) -> !)))

Notice that the largest Copland phrase that follows an @ operator is the one that is associated with it when brackets are omitted.

When a place is a sequence of digits, it is equivalent to the symbol that results from adding the letter p to the beginning of the digits.

The comment character is percent.

Copland Semantics

Associated with each Copland phrase is a term that describes the type of evidence collected by the phrase. Additionally, each Copland phrase has a precise semantics based on partially ordered sets of events, in which events are labeled.

Evidence Types

The syntax of evidence type EVIDENCE is

          |  s(EVIDENCE, EVIDENCE)
          |  p(EVIDENCE, EVIDENCE)

The empty evidence type is mt. The set of possible reports generated by measurement request S Q T at P given previous evidence V is m(msp(S, Q, T), P, V), where msp(S, Q, T) is an event label to be explained later. The evidence gained by signing V at P is g(V, P), and evidence gained by hashing V at P is H(V, P). Evidence of the form s(V1, V2) asserts that the report in V1 was produced before the report in V2, and evidence of the form p(V1, V2) makes no assertion about the ordering of the report in V1 relative to the one in V2.

Event Semantics

Semantically, a Copland phrase specifies the mapping of input evidence to some output evidence via one or more attestation events. Each event occurs at a well defined place. Events involve taking measurements, signing or hashing evidence, or routing evidence so as to produce combinations of evidence.

To describe the semantics of executing Copland phrase C at place P, we describe how it transforms evidence of type V into evidence of type f(V), making use of diagrams of the form:

  V   +-------+   f(V)
----> | LABEL | ------->

The box represents an event, and the arrows show the flow of evidence. The ordering of events respects the flow of evidence. The syntax of an event label is

       |  PLACE:nul | PLACE:cpy | PLACE:sig | PLACE:hsh
       |  PLACE:req(PLACE) | PLACE:rpy(PLACE)
       |  PLACE:BRANCH split | PLACE:join

The initial evidence associated with a phrase is the empty evidence mt.

The most basic Copland phrase is a measurement S Q T, for symbols S and T, and place Q, where S names the measurement, T names the target of the measurement, and Q is the place at which the target resides. When at place P with input evidence V, S Q T means that P should receive V, perform S targeting T at Q, and then emit the resulting evidence f(V).

  V   +--------------+   f(V)
----> | P:msp(S,Q,T) | ------->

where f(V)= m(msp(S, Q, T), P, V). Evidence type m(E, P, V) denotes the type of evidence produced by Measurement SPecification E at P starting with evidence of type V.

Let P:{C} be the events and their orderings associated with executing phrase C at P. Measurements can be combined in a pipeline fashion using the -> operator. Thus when at P with input evidence V, C1 -> C2 means

  V            f1(V)            f2(f1(V))
----> P:{C1} --------> P:{C2} ------------>

Measurements can be taken at a remote locations using the @ operator. When at P with input evidence V, @Q[C] means

  V   +----------+   V           f(V)   +----------+   f(V)
----> | P:req(Q) | ----> Q:{C} -------> | P:rpy(Q) | ------->
      +----------+                      +----------+

Phrases C1 and C2 can be combined using branching. There are several ways of combining phrases using branching, but they all follow the same split-join pattern. When at P with input evidence V, C1 BRANCH C2 means

                           V1           f1(V1)
                         -----> P:{C1} --------->
  V   +----------------+/                        \+--------+   V0
----> | P:BRANCH split |                          | P:join | ----->
      +----------------+\  V2           f2(V2)   /+--------+
                         -----> P:{C2} --------->

There are two dimensions by which branching differs. The split event may pass its input evidence to a phrase or hide it from that phrase by sending the empty evidence. Additionally, the execution of phrase C1 may be required to finish before phrase C2 starts, or both are allowed to execute in parallel.

Three characters make up a branching operator. If the middle character is <, sequential branching is specified, and V0 = s(f1(V1), f2(V2)). Otherwise the middle character is ~, parallel branching is specified, and V0 = p(f1(V1), f2(V2)). When sequential branching is specified, every event in P:{C1} occurs before every event in P:{C2}. Otherwise, these sets of events are not ordered.

The actions of the split event are specified by the + and - characters. If the first character in the operator is +, then V1 = V. Otherwise, the first character is -, and V1 = mt. The third character in the operator specifies the value of V2 similarly.

There are four phrases that specify single events.

Hashing is specified using #. When at P with input evidence V, # means

  V   +-------+   h(V, P)
----> | P:hsh | ---------->

Signing is specified using !. When at P with input evidence V, ! means

  V   +-------+   g(V, P)
----> | P:sig | ---------->

Copying is specified using _. When at P with input evidence V,_ means

  V   +-------+   V
----> | P:cpy | ----->

Nullifying is specified using {}. When at P with input evidence V, {} means

  V   +-------+   mt
----> | P:nul | ----->

XHTML Rendering

A tool creates an XHTML document from a Copland phrase that contains the phrase and a visualization of its semantics. The document contains the phrase that was analyzed, a diagram of the abstract syntax of the phrase that makes it clear how it is parsed, and a diagram showing its event semantics.

The diagram contains two types of nodes. An oval represents an event and it contain the event’s label. A box represents evidence.

A black arrow shows both a flow of data and an ordering of events. A red arrow indicates an additional ordering of events due to the use of a sequential branching operator. A blue arrow connects a request with its matching reply.

Events and evidence passing that occur at one place are collected together within a surrounding rectangle. The place associated with the rectangle is displayed in the upper right corner of the rectangle.

© 2020 The MITRE Corporation.

Approved for Public Release; Distribution Unlimited. Public Release Case Number 20-2549

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.

This technical data deliverable was developed using contract funds under Basic Contract No. W56KGU-18-D-0004.