Scalable Trust Semantics & Infrastructure--2018 Q4

PI(s), Co-PI(s), Researchers: Perry Alexander

HARD PROBLEM(S) ADDRESSED

Scalability and Composability

Policy-governed Collaboration

PUBLICATIONS

KEY HIGHLIGHTS

* Continued working with MITRE, JHUAPL and NSA R21 on a language for attestation protocols, now called Copland. The initial formal semantics is complete and verified in Coq. We submitted a paper to POST'19 and created a website for distribution.

* Added the nonce implementation to the Copland interpreter. Continued development of the static type system and lambda expression. Began formal specification of an attestation monad to capture stateful semantics of attestation and appraisal.

* Completed an initial Copland evaluator in Haskell running in Linux. The interpreter implements the full language and adds attestation management capabilities. The interpreter will be publicly available early in Q1 2019

* Continued development of a CakeML interpreter that implements the Copland formal semantics. Basic terms including measurements can be evaluated. Began a CakeML embedding in Coq to support verifying the interpreter against formal semantics.

* Continued working on a trace-based definition of measurement sufficiency. The Copland trace-based semantics allows discussion of protocol soundness and sufficiency. Began working to capture well-defined remote attestation properties in our formal system to support formal analysis.

* Began discussions of decentralization and aggregation of trust using blockchain as an mechanism for accomplishing decentralization. The intent is to eliminate certificate authorities and appraise entire attestation infrastructures.

COMMUNITY ENGAGEMENTS

EDUCATIONAL ADVANCES: