Trusted Platform Module (TPM) Verification
Project Award Date: 04-16-2012
If the Trusted Platform Module (TPM) is to form the trusted root of secure computing systems, validation, verification, and certification are essential. Without these assurances, there is no trust in the system. With millions of TPMs fielded, it becomes critical to remove ambiguities and inconsistencies in the current TPM specification.
ITTC researchers will provide a formal TPM specification, verification of the specification, and a verified TPM implementation. A verified TPM - the ultimate research goal - will dramatically simplify certification.
Model the TPM state and command execution - Using monadic techniques develop a model of the TPM internal state and a framework for command execution.
Model and Verify the attestation subset - Using the TPM state model, specify and verify the TPM command subset for PCR management and quote generation. Extend existing verification of PCR extension results.
Model and Verify the key management subset - Using the TPM state model, specify and verify the TPM command subset for generating and managing keys.
Verify common TPM command sequences - Using the new monadic model to expand previously performed verification of various TPM processes including boot
Primary Sponsor(s): Battelle Memorial Institute