• DocumentCode
    1923710
  • 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
  • fYear
    2011
  • fDate
    18-20 April 2011
  • Firstpage
    55
  • Lastpage
    58
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Communications and Mobile Computing (CMC), 2011 Third International Conference on
  • Conference_Location
    Qingdao
  • Print_ISBN
    978-1-61284-312-4
  • Type

    conf

  • DOI
    10.1109/CMC.2011.108
  • Filename
    5931124
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1923710