The Coq mailing list

["Ramsdell, John D." <ramsdell AT mitre.org>]

Paul Rowe will present the paper "Orchestrating Layered Attestation",
by myself, Paul, Perry Alexander, Sarah C. Helble, Peter Loscocco
J. Aaron Pendergrass, and Adam Petz at Principles of Security and
Trust 2019 next week.  The paper presents a language and two versions of
its semantics.  The language and the proofs of the relations between the
two semantics was proved in Coq and made available to the public.

I attended the DeepSpec Summer School in 2017.  It played an important
role in making this work possible.  Thanks to all involved.

John

PAPER ABSTRACT:
We present Copland, a language for specifying layered
attestations. Layered attestations provide a remote appraiser with
structured evidence of the integrity of a target system to support a
trust decision. The language is designed to bridge the gap between
formal analysis of attestation security guarantees and concrete
implementations. We therefore provide two semantic interpretations of
terms in our language. The first is a denotational semantics in terms
of partially ordered sets of events. This directly connects Copland to
prior work on layered attestation. The second is an operational
semantics detailing how the data and control flow are executed. This
gives explicit implementation guidance for attestation frameworks. We
show a formal connection between the two semantics ensuring that any
execution according to the operational semantics is consistent with
the denotational event semantics. This ensures that formal guarantees
resulting from analyzing the event semantics will hold for executions
respecting the operational semantics. All results have been formally
verified with the Coq proof assistant.

COQ PROOFS
https://ku-sldg.github.io/copland/resources/coplandcoq/index.html