Formal developing of security bootstrap on TPM

Security bootstrap is pretty important to the platform security, and trusted bootstrap is significant in the research of trusted computing. However, works on trusted bootstrap are relatively less. In this paper, we present a trusted bootstrap framework and related measurements from both hardware and software aspects based on trusted computing. We modify trust chain defined by TCG slightly by introducing a new component called PMBR, to implement a more flexible security bootstrap. Our approach can automatically recover programs being attacked. Furthermore, the “attack codes” inserted by attackers and their corresponding physical addresses can be precisely extracted and located respectively. On the other, we use B method as the formal tool to develop PMBR, which can generate the execution code automatically.