Semantics, languages and tools for layered attestation
29 Feb 2024
New paper out from our colleagues at MITRE: Evidence Tampering and Chain of Custody in Layered Attestations complete with Coq sources. The paper examines evidence custody chains in remote attestation with the goal of identifying all tampering opportunities. The ultimate goal being trust in the evidence used for appraisal.
22 Dec 2023
The Copland Collection, a set of tools for writing and analyzing Copland specification, has been updated by MITRE. download the newest version of th Copland Collection here.
22 Dec 2023
A new version of the CHASE model finder tutorial is available on the Documentation page. Usage examples covering analysis of Copland phrases are updated in the tutorial.
31 Dec 2022
The Maat attestation manager is now publicly available. Maat is a highly customizable, centralized software integrity measurement and attestation (M&A) service.
28 Dec 2022
A new tutorial on writing and using the CHASE model finder is available on the Documentation page. Usage examples covering analysis of Copland phrases are included in the tutorial.
Flexible Mechanisms Paper Published
04 Sep 2021
“Flexible Mechanisms for Remote Attestation” by Sarah Helble, Ian Kretz, Peter Loscocco, John Ramsdell, Paul Rowe, and Perry Alexander has been puplished in ACM Transactions On Security and Privacy, 24(4). The paper defines a collection of common attestation shapes used in layered attestation. The paper can be accessed here.
Automated Trust Analysis Paper Accepted
31 Aug 2021
“Automated Trust Analysis of Copland Specifications for Layered Attestation” by Paul Rowe, John Ramsdell, and Ian Kretz has been accepted for publication at Principles and Practice of Declarative Programming (PPDP’21), September 6-8 in Tallinn, Estonia. The paper describes a method for analyzing trust properties of Copland phrases, allowing analysts and designers to evaluate the strength of a Copland phrase in the presence of an active adversary. You can access a prepub manuscript from the publications page. The full details of inputs used for examples in the paper can be browsed here.
30 Aug 2021
“Design and Formal Verification of a Copland-based Attestation Protocol” by Adam Petz, Grant Jurgensen, and Perry Alexander has been accepted for publication at the MEMOCODE ‘21 conference, Nov 20-22, to be held virtually. This paper introduces a workflow for both analyzing and executing Copland-based attestation protocols in the context of a security architecture. It concludes by instantiating that workflow with a concrete architecture and layered attestation protocol designed for a DARPA CASE demonstration platform that hosts a legacy UAV flight control application. Download a pdf of the paper from the publications page.
NFM ‘21 (Virtual) Conference Presentation
28 May 2021
Adam Petz recently presented his joint work with Dr. Perry Alexander entitled “An Infrastructure for Faithful
Execution of Remote Attestation Protocols” at the (virtual) NASA
Formal Methods (NFM’21) conference. A video recording of the
talk/slides and live Q&A following the talk can be viewed on Youtube
here.
Download a pdf of the paper from the publications page.
20 May 2021
Our MITRE colleagues have released The Copland Collection, a collection of tools for processing and analyzing Copland protocol specifications. The Copland Collection includes application of the CHASE model finder to explore interleaving of corruption and measurements to better understand protocol effectiveness. Download the Copland Collection here.
24 Feb 2021
“An Infrastructure for Faithful Execution of Remote Attestation Protocols” by Adam Petz and Perry Alexander has been accepted for publication at NASA Formal Methods Symposium (NFM’21), May 24-28, in Norfolk, VA. This paper presents a verified model of our attestation manager implementation that compiles Copland terms into an attestation intermediate form. Download a prepub manuscript from the publications page.
Haskell Attestation Manager Release
12 Jan 2021
Our Haskell Attestation Manager is available. The Haskell Attestation Manger is a direct implementation of a Copland interpreter using monad transformers. The Haskell AM is used primarily for prototyping, but can be used for delivered systems.
CakeML Attestation Manager Release
12 Jan 2021
Our reference CakeML Attestation Manager is available. The CakeML Attestation Manger is a relatively small implementation of a Copland interpreter written using the CakeML language. The implementation is actively maintained and used as our primary delivery platform.
31 Dec 2020
The Copland Tutorial has been udpated to include analysis tool outputs.
22 Dec 2020
A new tutorial on writing basic Copland phrases is available on the Documentation page. The tutorial describes various attestation styles including mutual attestation, certificate-style attestation, and delegated appraisal. Example phrases are included throughout.
24 Jun 2019
The first release of our Haskell Attestation Manager is now available on the software page. Clone the release repo and follow the instructions in README.md to build the release.
17 Jun 2019
JSON exchange format has been updated to version 0.1.
30 May 2019
A description of the JSON format used to exchange protocols an evidence in KU’s tools has been added to the software page.
30 May 2019
Check out Adam’s HoTSoS 2019 presentation of our paper A Copland Attestation Manager.