University of Kansas


Visible to the public Verifying the Trusted Platform Module


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.


Visible to the public Security as a System-Level Constraint