Automated Trust Analysis of Copland Specifications for Layered Attestation

Paul D. Rowe, John D. Ramsdell, and Ian D. Kretz

The MITRE Corporation

This page provides access to the input files used in “Automated Trust Analysis of Copland Specifications for Layered Attestation” as published in Principles and Practice of Declarative Programming (PPDP’21).

The analysis requires you to install the Copland Collection tool suite which can be downloaded from here. The README in the download contains instructions for compiling the code.

To download a tarball of all input files, including a Makefile to run them, click here. Once you have downloaded the inputs and installed the Copland Collection, simply type make on the command line to run the analyses. You can vary the assumptions by editing the *_supps.gli files.

If you simply wish to browse the contents of the input files or the resulting outputs, links are provided below to view them online in Markdown.

Theory of minimal, adversary-ordered saturated queries:

• Fixed theory

Example 1:

• Copland phrase
• Assumptions
• Query
• Output

Example 2:

• Copland phrase
• Assumptions
• Query
• Output

Example 17:

• Copland phrase
• Assumptions
• Query
• Output