Visible to the public Scalable Trust Semantics & Infrastructure — 2021 Q1Conflict Detection Enabled

Submitted by Warren Alexander on Sun, 04/18/2021 - 4:45pm

PI(s): Perry Alexander

RESEARCHER(s):

HARD PROBLEM(S) ADDRESSED: Policy-Governed Secure Collaboration, Scalability and Composability

PUBLIC ACCOMPLISHMENT HIGHLIGHTS:

  • Published the first verified semantics for an attestation manager.
  • Began verification of an end-to-end layered attestation using our verified semantics for attestation managers.
  • Continued development of a model for attestation protocol negotiation using dependent types for policy enforcement.
  • Released updates to the CakeML and Haskell attestation manager implementations.

PUBLICATIONS FROM THE QUARTER:

  • Petz, A. and P. Alexader, "An Infrastructure for Faithful Execution of Remote Attestation Protocols," NASA Formal Methods Symposium (NFM'21), May 24-28, Norfolk, VA.
Groups: