Visible to the public Scalable Trust Semantics & Infrastructure Update. 2018 Q3Conflict Detection Enabled

Submitted by RCJBob on Fri, 10/12/2018 - 11:43am

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

HARD PROBLEM(S) ADDRESSED

Scalability, Composability

Policy Governed Collaboration

PUBLICATIONS

N/A

KEY HIGHLIGHTS

* Continued working with MITRE, JHUAPL and NSA R21 on the development of a formal semantics for attestation protocols. We have completed the first full version of a denotational and operational semantics for protocol execution. This will be submitted for publication in November.

* Added a static type system and lambda and nonce functionality to the APDT semantics. New functionality will support a broader collection of attestation tasks and simplify writing individual protocols.

* Continued developing an APDT evaluator in Haskell and CakeML that implements the APDT formal semantics. We will begin verifying the interpreter against the formal semantics next quarter.

* Continued working on a Galois Connection based definition of measurement soundness. The model currently addresses imperfect hashing as a measurement technique. Future work will extend to behavioral measurements.

* Continued working on a trace-based definition of measurement sufficiency. With the APDT semantics completed, we now have a trace-based semantics for APDT execution. We will use that trace semantics to verify properties of executing protocols focusing initially on measurement ordering and adversary actions.

Groups: