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.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
- Modeling TCG-Based Secure Systems with Colored Petri Nets
- Springer Berlin Heidelberg
Neuer Inhalt/© ITandMEDIA, Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung/© astrosystem | stock.adobe.com