Scalable Trust Semantics & Infrastructure — 2020 Q4

PI(s): Perry Alexander

RESEARCHER(s):

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

PUBLIC ACCOMPLISHMENT HIGHLIGHTS:

• Developed an indexed type for terms and accompanying subset type to ensure selected protocols satisfy privacy policy.
• Released an initial version of the attestation monad, attestation virtual machine, and Copland compiler as a formal model of attestation and appraisal.
• Submitted a paper describing our formal model of Copland compilation and execution based on formal model.
• Released new versions of the CakeML and Haskell attestation manager implementations.

PUBLICATIONS FROM THE QUARTER:

No new papers accepted for publication. One new paper submitted and one currently in review.