Title :
Formal Analysis of Trusted Computing: One Case Study
Author :
Zhou, HongWei ; Yuan, JinHui
Author_Institution :
Key Lab. of Data Eng. & Knowledge Eng., Minist. of Educ., Beijing, China
Abstract :
LS2 is the logic to reason about the property of trusted computing. However, it lacks the capability of modeling the isolation provided by virtualization which is often involved in previous trusted computing system. With the support of changed LS2, we model three types of isolation. Moreover, we formally analyze the integrity measurement property of TrustVisor proposed recently which provides the isolated execution environment for security-sensitive code.
Keywords :
program diagnostics; security of data; TrustVisor; formal analysis; integrity measurement property; isolated execution environment; security-sensitive code; trusted computing system; virtualization; Access control; Analytical models; Computational modeling; TV; Time measurement; Virtual machining; TPM; isolation; trusted computing; virtualization;
Conference_Titel :
Communications and Mobile Computing (CMC), 2011 Third International Conference on
Conference_Location :
Qingdao
Print_ISBN :
978-1-61284-312-4
DOI :
10.1109/CMC.2011.108
