Scalable Trust Semantics & Infrastructure — 2021 Q1

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.