Copland

Semantics, languages and tools for layered attestation

Home
Publications
Documentation
Software
Blog

Blog

Copland Collection Updated

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.


CHASE Tutorial Updated

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.


Maat Released

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.


CHASE Tutorial Added

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.


MEMOCODE Paper Accepted

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.


Copland Collection Released

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.


NFM Paper Accepted

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.


Tutorial Update

31 Dec 2020

The Copland Tutorial has been udpated to include analysis tool outputs.


Copland Tutorial Added

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.


Haskell AM Initial Release

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.


JSON Exchange Format Update

17 Jun 2019

JSON exchange format has been updated to version 0.1.


JSON Exchange Format

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.


HoTSoS 2019 Presentation

30 May 2019

Check out Adam’s HoTSoS 2019 presentation of our paper A Copland Attestation Manager.