Scalable Trust Semantics & Infrastructure — 2021 Q2
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.