Skip to main content
SpringerLink
Log in

Modeling TCG-Based Secure Systems with Colored Petri Nets

  • Conference paper
Trusted Systems (INTRUST 2010)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 6802))

Included in the following conference series:

Abstract

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.

This work is supported by the National Basic Research Program of China (973) under Grant No. 2009CB320703, the Science Fund for Creative Research Groups of China under Grant No. 60821003, National Key S & T Special Projects under Grant No. 2009ZX01039-001-001 and the National High-Tech Research and Development Plan of China under Grant No.2009AA01Z139, and National Natural Science Foundation of China under Grant No. 60873238. and No. 60903178.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Wobber, T.: A Logical Account of NGSCB. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 1–12. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Ahmed, T., Tripathi, A.R.: Static verification of security requirements in role based cscw systems. In: The Eighth ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 196–203 (2003)

    Google Scholar 

  3. AMD. AMD64 Virtualization Codenamed Pacifica Technology–Secure Virtual Machine Architecture Reference Manual. Technical Report Publication Number 33047, Revision 3.01, AMD (May 2005)

    Google Scholar 

  4. AMD. Amd64 architecture programmer’s manual, vol. 2: System programming (2007)

    Google Scholar 

  5. Berger, S., Caceres, R., Goldman, K.A., Perez, R., Sailer, R., van Doorn, L.: vTPM: Virtualizing the Trusted Platform Module. In: Proceedings of the 15th USENIX Security Symposium, pp. 305–320. USENIX (August 2006)

    Google Scholar 

  6. Bhargava, R., Serebrin, B., Spadini, F., Manne, S.: Accelerating two-dimensional page walks for virtualized systems. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2008), Seattle, WA, USA, pp. 26–35. ACM, New York (March 2008)

    Chapter  Google Scholar 

  7. Bruschi, D., Cavallaro, L., Lanzi, A., Monga, M.: Replay attack in TCG specification and solution. In: ACSAC, pp. 127–137. IEEE Computer Society, Los Alamitos (2005)

    Google Scholar 

  8. Chen, L., Landfermann, R., Löhr, H., Rohe, M., Sadeghi, A.-R., Stüble, C.: A protocol for property-based attestation. In: STC 2006, pp. 7–16. ACM Press, New York (2006)

    Google Scholar 

  9. Chen, S.-Y., Wen, Y., Zhao, H.: Formal analysis of secure bootstrap in trusted computing. In: Xiao, B., Yang, L.T., Ma, J., Muller-Schloer, C., Hua, Y. (eds.) ATC 2007. LNCS, vol. 4610, pp. 352–360. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. CPN group at the Department of Computer Science in University of Aarhus. Examples of Industrial Use of CP-nets (2010), http://www.daimi.au.dk/CPnets/intro/example_indu.html

  11. Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol Composition Logic (PCL). Electron. Notes Theor. Comput. Sci. 172, 311–358 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  12. Datta, A., Franklin, J., Garg, D., Kaynar, D.: A logic of secure systems and its application to trusted computing. In: Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, pp. 221–236. IEEE Computer Society, Washington, DC, USA (2009)

    Chapter  Google Scholar 

  13. Garfinkel, T., Pfaff, B., Chow, J., Rosenblum, M., Boneh, D.: Terra: A Virtual Machine-Based Platform for Trusted Computing. In: SOSP 2003, Bolton Landing, New York, USA, October 19-22 (2003)

    Google Scholar 

  14. Garg, D., Franklin, J., Kaynar, D., Datta, A.: Compositional system security with interface-confined adversaries. In: Mathematical Foundations of Programming Semantics (MFPS) Conference (April 6, 2010)

    Google Scholar 

  15. Gu, L., Cheng, Y., Ding, X., Deng, R.H., Guo, Y., Shao, W.: Remote attestation on function execution. In: Chen, L., Yung, M. (eds.) INTRUST 2009. LNCS, vol. 6163, pp. 60–72. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Gu, L., Ding, X., Deng, R.H., Xie, B., Mei, H.: Remote attestation on program execution. In: ACM workshop on Scalable Trusted Computing (STC), held in conjunction with the 15th ACM Conference on Computer and Communications Security (ACM CCS 2008) (2008)

    Google Scholar 

  17. Gu, L., Ding, X., Deng, R.H., Xie, B., Mei, H.: Remote platform attestation - the testimony for trust management. In: Yan, Z. (ed.) Trust Modeling and Management in Digital Environments: from Social Concept to System Development. IGI Global (2010), doi:10.4018/978-1-61520-682-7, ISBN-13: 978-1615206827

    Google Scholar 

  18. Gürgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security Evaluation of Scenarios Based on the TCG’s TPM Specification. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 438–453. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Intel Corporation. Intel Trusted Execution Technology — Preliminary Architecture Specification. Technical Report Document Number: 31516803, Intel Corporation (2006)

    Google Scholar 

  20. Intel Corporation. Intel Virtualization Technology for Directed I/O Architecture Specification. Technical Report Order Number: D51397-001, Intel Corporation (February 2006)

    Google Scholar 

  21. Jaeger, T., Sailer, R., Shankar, U.: PRIMA: policy-reduced integrity measurement architecture. In: SACMAT 2006, pp. 19–28. ACM Press, New York (2006)

    Google Scholar 

  22. Jensen, K.: Colored Petri Nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 254, pp. 248–299. Springer, Heidelberg (1987)

    Google Scholar 

  23. Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. EATCS Monographs on Theoretical Computer Science, vol. 1. Springer, Heidelberg (1992)

    Book  MATH  Google Scholar 

  24. Jensen, K.: An Introduction to the Theoretical Aspects of Coloured Petri Nets. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803. Springer, Heidelberg (1994)

    Google Scholar 

  25. Y. Jiang, C. Lin, H. Yin, and Z. Tan. Security analysis of mandatory access control model. In IEEE International Conference on Systems, Man and Cybernetics, volume vol. 6, page 5013–5018, 2004.

    Google Scholar 

  26. Jørgensen, J.B., Mortensen, K.H.: Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 249–268. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  27. Katt, B., Hafner, M., Zhang, X.: Building a stateful reference monitor with Coloured Petri Nets. In: CollaborateCom, pp. 1–10 (2009)

    Google Scholar 

  28. Katt, B., Zhang, X., Hafner, M.: Towards a Usage Control Policy Specification with Petri Nets. In: Meersman, R., Dillon, T., Herrero, P. (eds.) OTM 2009. LNCS, vol. 5871, pp. 905–912. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Kauer, B.: OSLO: improving the security of trusted computing. In: Proceedings of 16th USENIX Security Symposium, pp. 1–9. USENIX Association, Berkeley (2007)

    Google Scholar 

  30. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP 2009), Operating Systems Review (OSR), Big Sky, MT, pp. 207–220. ACM SIGOPS (October 2009)

    Google Scholar 

  31. Knorr, K.: Dynamic access control through Petri Net workflows. In: 16th Annual Computer Security Applications Conference (ACSAC), page 159 (2000)

    Google Scholar 

  32. Madsen, O.L., Moller-Pedersen, B., Nygaard, K.: Object Oriented Programming in the Beta Programming Language. Addison-Wesley Publishing Company, Reading (1993)

    Google Scholar 

  33. McCune, J.M., Li, Y., Qu, N., Zhou, Z., Datta, A., Gligor, V., Perrig, A.: TrustVisor: Efficient TCB Reduction and Attestation. In: IEEE Symposium on Security and Privacy (2010)

    Google Scholar 

  34. McCune, J.M., Parno, B.J., Perrig, A., Reiter, M.K., Isozaki, H.: Flicker: an execution infrastructure for TCB minimization. In: 3rd ACM SIGOPS/EuroSys European Conference on Computer Systems, pp. 315–328. ACM, New York (2008), 1352625

    Google Scholar 

  35. Microsoft Corporation. BitLocker Drive Encryption: Technical Overview. New (optionally) TPM-based secure boot and filesystem encryption from MS Vista (2006)

    Google Scholar 

  36. Poritz, J., Schunter, M., Van Herreweghen, E., Waidner, M.: Property attestation—scalable and privacy-friendly security assessment of peer computers. Technical Report RZ 3548, IBM Research (May 2004)

    Google Scholar 

  37. Rakkay, H., Boucheneb, H.: Security analysis of role based access control models using colored petri nets and CPNtools. In: Gavrilova, M.L., Tan, C.J.K., Moreno, E.D. (eds.) Transactions on Computational Science IV. LNCS, vol. 5430, pp. 149–176. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  38. Sadeghi, A.-R., Selhorst, M., Stüble, C., Wachsmann, C., Winandy, M.: TCG inside?: a note on TPM specification compliance, pp. 47–56 (2006), 1179487

    Google Scholar 

  39. Sadeghi, A.-R., Stüble, C.: Property-based attestation for computing platforms: caring about properties, not mechanisms. New Security Paradigms (2004)

    Google Scholar 

  40. Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and Implementation of a TCG-based Integrity Measurement Architecture. In: Proceedings of the 13th USENIX Security Symposium, San Diego, CA, USA, August 9-13 (2004)

    Google Scholar 

  41. Shi, E., Perrig, A.: Van Doorn, L.: BIND: A Fine-Grained Attestation Service for Secure Distributed Systems. In: 2005 IEEE Symposium on Security and Privacy, S&P 2005 (2005)

    Google Scholar 

  42. Shin, W.: An extension of role based access control for trusted operating systems and its coloured petri net model, PhD thesis. Gwangju Institute of Science and Technology, Korea (2005), http://itslab.csce.kyushu-u.ac.jp/ssr/SSR-1/thesis-main.pdf

  43. Trusted Computing Group. TPM main specification. Main Specification Version 1.2 rev. 85, Trusted Computing Group (February 2005)

    Google Scholar 

  44. Trusted Computing Group. TCG Specification Architecture Overview (Revision 1.4) (2007)

    Google Scholar 

  45. Varadharajan, V.: Hook-up property for information flow secure nets. In: Computer Security Foundations Workshop IV, pp. 154–175 (1991)

    Google Scholar 

  46. Zhan, J., Zhang, H., Zou, B., Li, X.: Research on automated testing of the trusted platform model. In: ICYCS, pp. 2335–2339. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

  47. Zhang, J., Ma, J., Moon, S.: Universally composable secure tnc model and eap-tnc protocol in if-t. Science China Information Sciences 53(3), 465–482 (2010)

    Article  MathSciNet  Google Scholar 

  48. Zhang, Z., Hong, F., Liao, J.: Modeling Chinese Wall Policy Using Colored Petri Nets. In: CIT 2006: Proceedings of the Sixth IEEE International Conference on Computer and Information Technology, p. 162. IEEE Computer Society, Washington, DC, USA (2006)

    Google Scholar 

  49. Zhang, Z., Hong, F., Liao, J.-G.: Verification of strict integrity policy via petri nets. In: The International Conference on Systems and Networks Communication (ICSNC), p. 23 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Key Laboratory of High Confidence Software Technologies (Ministry of Education), Institute of Software, School of EECS, Peking University, China

    Liang Gu, Yao Guo & Hong Mei

  2. Institute for Infocomm Research, Singapore

    Yanjiang Yang & Feng Bao

Authors
  1. Liang Gu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yao Guo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yanjiang Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Feng Bao
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Hong Mei
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Hewlett-Packard Labs, Long Down Avenue, Stoke Gifford, BS34 8QZ, Bristol, UK

    Liqun Chen

  2. Google Inc. and Department of Computer Science, Columbia University, USA

    Moti Yung

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gu, L., Guo, Y., Yang, Y., Bao, F., Mei, H. (2011). Modeling TCG-Based Secure Systems with Colored Petri Nets. In: Chen, L., Yung, M. (eds) Trusted Systems. INTRUST 2010. Lecture Notes in Computer Science, vol 6802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25283-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-25283-9_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-25282-2

  • Online ISBN: 978-3-642-25283-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation