Trust Engineering via Protocol Design: Understanding Attestations from Trusted Execution Environments
Attestation protocols use digital signatures and other cryptographic
values to convey evidence of hardware state, program code, and
associated keys. They require hardware support such as Trusted
Execution Environments. Conclusions about attestations thus depend
jointly on protocols, hardware services, and program behavior.
We present a mechanized approach to modeling these properties,
combining protocol analysis with axioms, that formalize hardware and
software properties. Here, we model aspects of Intel’s SGX mechanism.
Above the underlying manufacturer-provided protocols, we describe how
to build a modular user-level that uses its attestations to make trust
Joshua Guttman received the A.B. degree from Princeton University, Princeton, NJ, in 1975 and the Ph.D. degree from the University of Chicago, IL, in 1984. He is Senior Principal Scientist at The MITRE Corporation, Bedford, MA. Having worked in mechanised reasoning and compiler verification, he now focuses on applying rigorous methods to cryptographic protocols, network security, and operating system security.