Modeling TCG-Based Secure Systems with Colored Petri Nets

With the rapid progresses in trusted computing related research and application, many trusted computing based security mechanisms have been proposed to defend against threats in open, dynamic and distributed environments. These mechanisms are supposed to serve as the security foundations in the underlying systems. However, the correctness of these security mechanisms still require further examination and validation. We propose a Colored Petri Nets (CPN or CP-nets) based approach to model the trusted computing based secure system. In particular, with CPN, we model process management, data protection and late launch mechanisms in the systems. Further, as case studies we use these models to investigate the memory protection mechanism in TrustVisor and remote attestation based on dynamic root of trust, respectively; and the results demonstrate that our models are indeed capable of depicting real secure system based on trusted computing. With the advantages of CPN based modeling and analysis (e.g., graphical representation, well defined semantics and a large number of formal analysis methods), our models can well serve as the foundation for formal analysis on the security properties of trusted computing enhanced systems.