Verifying the Trusted Platform Module
Presented as part of the 2013 HCSS conference.
ABSTRACT
As the hardware root-of-trust for trusted computing systems, the Trusted Platform Module (TPM) is critical in establishing system trust. The TPM 1.2 and associated Trusted Software Stack (TSS) are described by 700 pages of precise, textual documentation and have not been formally modeled or verified. As the hardware root of trust for trusted computing, formal treatment of the TPM is warranted. To address assurance issues in the TPM, we are developing and verifying a model of the TPM 1.2 using PVS.
The TPM is a cryptographic co-processor defined by the Trusted Computing Group to support trusted computing. It provides three subsystems for: (i) high-integrity measurement storage; (ii) quote generation and delivery; and (iii) sealing data and keys to TPM state. Platform Configuration Registers (PCRs) store and extend hashes in a manner that prevents unauthorized reset or modification. The quote generation system delivers quotes to appraisers using remote attestation to preserve anonymity of appraisal targets and ensure measurement integrity. Finally, sealing session keys to PCR states using TPM resident keys binds a secret to a TPM and a TPM state.
Our objective in modeling the TPM is specifying abstract instruction requirements, establishing correctness of protocols and instruction sequences, and establishing correctness of detailed instruction definitions with respect to abstract requirements. We use an axiomatic approach to specify each instruction as a state transformation. A state monad sequences instruction execution allowing examination of protocols. Our ultimate goal is defining a bisimulation between the abstract and concrete models to demonstrate congruence between models.
The proposed presentation will focus on the abstract requirements model, individual instruction definition and verification, and attestation protocol verification. We will focus on modeling methodology, the use of PVS, and verification results thus far. We will discuss how individual TPM instructions are defined, how TPM state is represented, how the state monad is used for instruction sequencing, and how we use our model for verification of an attestation protocol that uses a Privacy CA to preserve anonymity of appraisal targets.
BIO:
Dr. Perry Alexander is a Professor of Electrical Engineering and Computer Science at the University of Kansas. His research interests include formal modeling, language semantics, systems-level design and component retrieval. He is a Senior Member of IEEE and is past president of the Engineering of Computer-Based Systems Technical Committee. He is the principal architect of the Rosetta systems-level design language. He has published over 90 refereed papers, has won 15 teaching awards, and presented numerous invited talks. The professional achievement he is most proud of is his students.