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

Submitted by Warren Alexander on Fri, 07/09/2021 - 5:07pm

PI(s): Perry Alexander

RESEARCHER(s):

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

PUBLIC ACCOMPLISHMENT HIGHLIGHTS:

  • Published a collection of patterns for flexible deployment of layered attestation.

  • Continued verification of an end-to-end layered attestation and appraisal using our verified semantics for attestation managers.

  • Modeling and implementation of a general appraisal algorithm

  • Maintained the publicly available Copland repository including CakeML, Coq and Haskell attestation manager implementations.

PUBLICATIONS FROM THE QUARTER:

  • Helble, S., I. Kretz, P. Loscocco, J. Ramsdell, P. Rowe, and P. Alexander, "Flexible Mechanisms for Remote Attestation," in press ACM Transactions on Privacy and Security.

  • Fritz, A. and P. Alexander, "A Dependently Typed Attestation Protocol Language," accepted poster presentation at _Hot Topics in Science of Security (HoTSoS'21), online, April 13-15, 2021.

  • 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: