University of Kansas

file

Visible to the public Verifying the Trusted Platform Module

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.