Semantics, languages and tools for layered attestation
Clare C. Parran, Ian D. Kretz, John D. Ramsdell, and Paul D. Rowe
The MITRE Corporation
The purpose of this tutorial is to guide the reader through the use of our trust analysis tools for Copland phrases. Readers not already familiar with the syntax and semantics of Copland should first visit our Copland tutorial.
While this tutorial does not require the reader to replicate the results using the Copland Collection tool suite, it can be beneficial to follow along on your own. The Copland Collection software suite can be downloaded here. Once the package is downloaded, the README contains instructions for compilation and installation. The other tutorial files can be obtained from this website.
The purpose of remote attestation is for an appraiser to gain trust in a remote system through integrity measurements of its subcomponents. However, we face an interesting dilemma. If the appraiser is distrustful of the target to begin with, why should the appraiser be any more trustful of the target to faithfully gather the required integrity evidence? The answer typically lies in relying on layered architectures that allow subcomponents with strong security protections to measure other subcomponents with weaker protections. We can use Copland to orchestrate the activities (integrity measurements, evidence bundling, etc.) of a layered attestation. For any given Copland phrase, we would like to know if it leverages the layered architecture in a way that produces trustworthy evidence. In other words, we would like to know all the ways an adversary might interfere with the execution of a Copland phrase to result in evidence that will pass appraisal, even though a given target component was corrupt at the time it was measured.
To that end, we have developed an automated analysis methodology to enumerate all the different ways an adversary can successfully interfere with a Copland phrase. This tutorial introduces the methodology by walking the reader through various examples. Our aim is to provide enough details and variations to empower the reader to perform their own analyses on Copland phrases of their own design. Readers interested in the scientific basis for the correctness and completeness of our approach are encouraged to read the Automated Trust Analysis of Copland Specifications for Layered Attestations paper published in Principles and Practice of Declarative Programming (PPDP 2021).
The trust analysis we perform is based on a simple, but powerful, model of how an adversary can interfere with the execution of a Copland phrase. We envision an adversary with the ability to corrupt any component of the target system to cause it to deviate from its regular behavior. The adversary can also repair any corrupted component, returning it to its regular state. These two actions toggle the corruption state of a component. In turn, the corruption state of components affects the evidence that is generated by a measurement. A regular measurer will (with one exception noted below) generate evidence that accurately reflects the corruption state of its target. A corrupt measurer will always generate evidence that indicates its target is regular, regardless of the corruption state of the target. In the former case, if the target is corrupt, then we say that the measurement detects the corruption. In the latter case, if the target is corrupt, we say the target avoids detection.
The one exception to the above rule is when the measurer relies on some other component in its context to function properly. For example, antivirus software typically relies on the operating system kernel to provide it an accurate picture of the file system. A corrupt kernel can lie to a regular antivirus and convince it that some target file is regular when it is actually corrupt. Thus, when a corrupt component avoids detection, we know that either the measurer or some other component it relies on was corrupt at the time of the measurement. The effect the corruption state has on evidence is summarized in the following table.
| Measurer | Context | Target | Evidence Appraisal |
|---|---|---|---|
| corrupt | * | * | passes |
| * | corrupt | * | passes |
| regular | regular | regular | passes |
| regular | regular | corrupt | fails |
Another consideration we have been exploring is the ability of the adversary to tamper with a measurer’s evidence. An adversary that has unlimited access to the system could manipulate evidence that reveals a component’s corruption. For example, if the kernel takes a measurement of the antivirus software and it produces evidence that reveals the antivirus is corrupt, the adversary may want to doctor the evidence in a way that will not reveal the corruption state of the antivirus software. This is what we refer to as a tampering adversary. The details of how an adversary can perform tampering as it pertains to specific Copland phrases is an ongoing effort and will be included in this guide in future updates. The ongoing efforts are in an attempt to determine all the ways the adversary could potentially doctor evidence and to determine what tampering strategies an adversary is likely to exploit based on level of effort. These findings will be included in the Chase logic in future updates as well.
While this adversary is quite powerful, it does have some key limitations. We do not consider how a corrupt component might redirect the control flow of a Copland execution. While studying the trustworthiness of Copland phrases in the face of such abilities is interesting, our work has so far focused on the set of adversary abilities described above. In the future, we hope to enhance the analysis method to account for a broader range of adversary abilities. In our analysis, we are only interested in learning the ways in which an appraiser can be fooled into accepting an attestation when it should reject the results. That is, we would like to know how an adversary can corrupt or repair components, such that the resulting evidence will pass appraisal.
Our approach to analyzing adversary behavior is to create a theory in first order logic that describes possible executions of a Copland phrase, and then use a model finder to enumerate all of the executions.
The subset of first order logic we use is called geometric logic. A formula is in geometric form if it is a sentence consisting of a single implication, the antecedent is a conjunction of atomic formulas, and the consequent is a disjunction. Each disjunct is a conjunction of atomic formulas in which variables not appearing in the antecedent are existentially quantified.
The model finder we use is Chase. To see how to write Chase input, please visit the Input Syntax section in its online documentation.
Chase is a non-interactive model finder. One can specify runtime parameters on the command line, and also at the beginning of a source file. For example
[ bound = 500, limit = 5000, input_order ]
limits the size of structures considered by Chase, the number of inference steps, and requires that formulas in the input be always considered in the order they were presented.
There are various programs and files in the Copland
Collection repository used for
analysis. There is a program that extracts the semantics of a Copland
phrase as Chase input (coplandval2chase). There are several
programs that construct a web page with diagrams from Chase output and are
orchestrated by the coplandvalmeaschase script. Various Chase theory files
are concatenated to form the input for Chase.
In order to run Chase, the following files will be needed:
<basename>.cop<basename>.glnthy.gliMakefilewhere <basename> is any name, the cop file contains the Copland phrase, the thy.gli defines basic assumptions and axioms for the Chase logic and the gln file is discussed in more detail throughout the tutorial. Most likely, you will not need to alter the content in thy.gli and the Makefile.
<basename>.cop file (for additional guidance
on creating Copland phrases please refer to the Copland tutorial linked above or
view examples in the examples directory of the Copland Collection)thy.gli and the Makefile provided with this tutorial<basename>.gln file (see the ex directories for examples)
makeThe following files will be produced: <basename>.xhtml (showing the abstract syntax tree
and event semantics) and <basename>_chase.xhtml (showing the abstract
syntax tree, execution semantics and the models produced by Chase analysis). Our focus in this tutorial
will be on Chase models shown in the <basename>_chase.xhtml file. The models
shown in the output, describe the ways in which an adversary can corrupt and repair
components in order to avoid detection. These models are discussed in
more detail in the example walkthrough.
$ ls
Makefile ex1.cop ex1.gln thy.gli
$ make
copland2xhtml ex1.cop > ex1.xhtml
copland2distinct -o ex1_dist.gli ex1.cop
coplandvalmeaschase ex1.cop > ex1_chase.xhtml
rm ex1_dist.gli
$ : View ex1_chase.xhtml in browser
We will consider a simple attestation scenario and use it to illustrate the utility of Copland using Chase. In the examples, a client must provide evidence to their bank that their web browser is free of malicious extensions before a transaction can proceed. A simple version of this attestation may take place among the bank, a browser monitor (bmon) running in the client’s userspace (us) and a host-based antivirus suite (av) running in the client’s kernelspace (ks). The target of the attestation is the client’s browser extensions (exts). The bank can choose to have the client use either or both of av and bmon to generate evidence. As we will see, the bank’s choices greatly influence the trustworthiness of the evidence it receives.
The Chase adversary behaves as described above and is capable of corrupting or repairing components with the goal of producing measurement evidence that will pass appraisal. It is important to note that the Chase adversary cannot stop measurements from taking place, but may delay measurements to their own advantage. We also consider corruptions/repairs that take place in a narrow timeframe to be more difficult for the adversary to perform. Similarly, corruptions/repairs of deeper components (ones subject to greater ambient protections) are also considered more difficult for the adversary. The examples will provide a greater explanation of these concepts.
With the above background in mind, this tutorial will now walk through a few examples of Copland phrases and their corresponding Chase output. The example Copland phrases we use in this tutorial are extracted from the Automated Trust Analysis for Layered Attestations paper (linked above).
Please refer to the following examples:
(We recommend moving through the examples in the order presented below, starting
with ex1 and ending with ex3b.)
[ex1] [ex1b] [ex2] [ex2b] [ex2c] [ex3] [ex3b]
Approved for Public Release; Distribution Unlimited. Public Release Case Number 22-1025.
This technical data was developed using contract funds under Basic Contract No.~W56KGU-18-D-0004. 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.
©2022 The MITRE Corporation. ALL RIGHTS RESERVED.