Verified TPM

The goal of the Verified TPM is specifying and verifying the TPM 1.2 formally in PVS. We specify the TPM as a state transformation system with each instruction modifying the TPM state. We then use a state monad to sequence instruction execution, threading state through a sequence of instructions.

Recent Activities

• FM'14 Paper Submitted - 17 Nov 2013
• NFM'13 Presentation - 20 May 2013
• Mvd Presentation - 20 Sep 2012

Team

Faculty

• Perry Alexander

Students

• Jessica Ims

Research Staff

Subcontractors

The System-Level Design Group is a part of The Information and Telecommunication Technology Center at The University of Kansas.

Verified TPM is supported by