Semantics, languages and tools for layered 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.
A symbol is a lowercase letter optionally followed by letters, digits, and underscores. The syntax of a Copland phrase is
COPLAND ::= * PLACE : PHRASE | PHRASE
PLACE ::= SYMBOL | DIGITS
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.
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.
The syntax of evidence type EVIDENCE is
EVIDENCE ::= mt
| m(msp(SYMBOL, PLACE, SYMBOL), PLACE, EVIDENCE)
| g(EVIDENCE, PLACE) | H(EVIDENCE, PLACE)
| 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.
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
LABEL ::= PLACE:msp(SYMBOL, PLACE, SYMBOL)
| 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 | ----->
+-------+
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.