Semantics, languages and tools for layered attestation


Trust Analysis of Copland Phrases

Clare C. Parran, Ian D. Kretz, John D. Ramsdell, and Paul D. Rowe</br> 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 repo.


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 distrusful 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. But 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).

Background Assumptions

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.

Analysis Via Model Finding

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.

Using Chase

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:

where <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 and will download copies from this repo to use.

Running Chase

  1. Ensure the Copland Collection is installed by following the install instructions in the main
  2. Choose a Copland phrase to analyze and create a <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)
  3. Download thy.gli and the Makefile from this repository
  4. Create a <basename>.gln file (see the ex directories for examples)
    • Define the assumption that some particular component was corrupt when it was measured
    • Define assumptions about system dependencies using the “depends” predicate
    • Specify if you want to see deep corruptions
    • Specify if you want to see recent corruptions
    • Finally, include all the other necessary files (<basename>.gli, <basename>_dist.gli and thy.gli)
  5. make

The 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.

Example Run

$ 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

Example Walkthrough

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]