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