ABSTRACT

Copland is a domain specific language designed for describing, analyzing and executing attestation protocols. Its formal semantics defines evaluation, sequencing, and dispatch of measurements resulting in evidence describing a system’s state. That evidence is in turn appraised to determine if and how an external system will interact with it. The contribution of this work is a description of the first Copland interpreter and the attestation manager built around it. Following an overview of the syntax and formal semantics is a collection of motivating examples. Next is a description of a Haskellbased Copland interpreter and the attestation manager constructed around it. Examples are provided to show the interpreter’s interface format. A description of the Copland landscape and future goals closes the presentation.

Adam Petz is a PhD student in Computer Science at the University of Kansas under the guidance of his advisor, Dr. Perry Alexander.  Adam's broad research interests include formal methods, programming language semantics, functional programming, trusted computing, and computer security.  Adam has contributed to a number of successful externally-funded research projects while at the University of Kansas, and is currently working under the Cyber Assured Systems Engineering(CASE) DARPA effort.  Adam completed his Master's in Computer Science at the University of Kansas in 2016, and completed two B.S. degrees in Computer Science and Mathematics at Emporia State University in 2014.