Scalable Trust Semantics & Infrastructure--2018Q2

PI(s), Co-PI(s), Researchers: Perry Alexander

HARD PROBLEM(S) ADDRESSED

Scalability and composability, Policy governed collaboration

PUBLICATIONS
P. Alexander, "Trust and Proof," invited presentation at the _2018 KCNSC Trust Consortium_, Department of Energy's Kansas City National Security Campus, Grandview, MO, June 5-6, 2018.

S. Helble, Pendergrass, A., Loscocco, P., Alexander, P., Petz, A., Rowe, P., Ramsdell, J., "Principles of Layered Attestation," invited presentation at the _High Confidence Software and Systems Conference_, Annapolis, MD, May 7-9, 2018.

D. Hardin, Alexander, P., Slind, K. "VeriCores: Cyber-Instrumenting Devices Built from Verified Components," invited presentation at the _High Confidence Software and Systems Conference_, Annapolis, MD, May 7-9, 2018.

KEY HIGHLIGHTS
* Continued working with MITRE, JHUAPL and NSA R21 on the development of a formal semantics for attestation protocols. The formal semantics forms the basis of defining what a protocol does and how it interacts with its environment.

* Continued working on a Galois Connection based definition of measurement soundness. The model provides a precise definition of the abstraction that measurement performs. Formalized in Coq, the model allows us to look at whether a measurement gathers what we think it does.

* Continued working on a trace-based definition of measurement sufficiency. The model situates measurement among the various system events that occur on a target system. Formalized in Coq, the model allows us to evaluate a measurement's context in order to discover whether it is valid with respect to system events.

COMMUNITY ENGAGEMENTS

* We gave or supported three invited presentations. Two presentations were made at the High Confidence Software & Systems Conference that presented joint work with Rockwell Collins on reusable verification components and joint work with MITRE, JHUAPL, and R21 on layered attestation semantics

EDUCATIONAL ADVANCES: