Advertisement

Access Control Based on Code Identity for Open Distributed Systems

  • Andrew Cirillo
  • James Riely
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)

Abstract

In computing systems, trust is an expectation on the dynamic behavior of an agent; static analysis is a collection of techniques for establishing static bounds on the dynamic behavior of an agent. We study the relationship between code identity, static analysis and trust in open distributed systems. Our primary result is a robust safety theorem expressed in terms of a distributed higher-order pi-calculus with code identity and a primitive for remote attestation; types in the language make use of a rich specification language for access control policies.

Keywords

Trusted Computing Remote Attestation Access Control Authorization Logic Compound Principals Higher-Order Pi Calculus Typing 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Necula, G.C.: Proof-carrying code. In: POPL 1997 (1997)Google Scholar
  2. 2.
    Trusted Computing Group: TCG TPM Specification Version 1.2 (March 2006), http://www.trustedcomputinggroup.org
  3. 3.
    Trusted Computing Group: TCG Software Stack (TSS) Specification Version 1.2 (January 2006), http://www.trustedcomputinggroup.org
  4. 4.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1) (1999)Google Scholar
  5. 5.
    Abadi, M., Fournet, C., Gonthier, G.: Authentication primitives and their compilation. In: POPL, pp. 302–315. ACM Press, New York, NY, USA (2000)CrossRefGoogle Scholar
  6. 6.
    Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: CCS 2004: Proceedings of the 11th ACM conference on Computer and communications security, pp. 132–145. ACM Press, New York, NY, USA (2004)CrossRefGoogle Scholar
  7. 7.
    Sadeghi, A.R., Stüble, C.: Property-based attestation for computing platforms: Caring about properties, not mechanisms. In: New Security Paradigms Workshop (2004)Google Scholar
  8. 8.
    Schoen, S.: Trusted Computing: Promise and Risk. Electronic Frontier Foundation (October 2003), http://www.eff.org/Infrastructure/trusted_computing/20031001_tc.pdf
  9. 9.
    Sandhu, R., Zhang, X.: Peer-to-peer access control architecture using trusted computing technology. In: SACMAT 2005: Proceedings of the tenth ACM symposium on Access control models and technologies, pp. 147–158. ACM Press, New York, NY, USA (2005)CrossRefGoogle Scholar
  10. 10.
    Jaeger, T., Sailer, R., Shankar, U.: Prima: policy-reduced integrity measurement architecture. In: SACMAT 2006: Proceedings of the eleventh ACM symposium on Access control models and technologies, pp. 19–28. ACM Press, New York, NY, USA (2006)CrossRefGoogle Scholar
  11. 11.
    Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh (1993)Google Scholar
  12. 12.
    Thomsen, B.: Plain chocs: A second generation calculus for higher order processes. Acta Informatica 30(1), 1–59 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Milner, R.: Functions as processes. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 167–180. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  14. 14.
    Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst. 15(4), 706–734 (1993)CrossRefGoogle Scholar
  15. 15.
    Abadi, M., Birrell, A., Wobber, T.: Access control in a world of software diversity. In: Tenth Workshop on Hot Topics in Operating Systems (HotOS X) (June 2005)Google Scholar
  16. 16.
    Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: ESOP, pp. 141–156 (2005)Google Scholar
  17. 17.
    Fournet, C., Gordon, A., Maffeis, S.: A type discipline for authorization in distributed systems. CSF 00, 31–48 (2007)Google Scholar
  18. 18.
    Cirillo, A., Jagadeesan, R., Pitcher, C., Riely, J.: Do As I SaY! Programmatic Access Control with Explicit Identities. CSF 0, 16–30 (2007)Google Scholar
  19. 19.
    Sangiorgi, D.: Asynchronous process calculi: the first-order and higher-order paradigms (tutorial). Theoretical Computer Science 253, 311–350 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Yoshida, N.: Minimality and separation results on asynchronous mobile processes. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, p. 131. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  21. 21.
    Merro, M.: Locality in the pi-calculus and applications to distributed objects. PhD thesis, Ecole des Mines de Paris (October 2000)Google Scholar
  22. 22.
    Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Inf. Comput. 173(1), 82–120 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Pitcher, C., Riely, J.: Dynamic policy discovery with remote attestation. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  24. 24.
    Gordon, A.D., Jeffrey, A.S.A.: Types and effects for asymmetric cryptographic protocols. J. Computer Security 12(3/4) (2004)Google Scholar
  25. 25.
    Haack, C., Jeffrey, A.S.A.: Pattern-matching spi-calculus. In: Proc. IFIP WG 1.7 Workshop on Formal Aspects in Security and Trust (2004)Google Scholar
  26. 26.
    Yoshida, N., Hennessy, M.: Assigning types to processes. LICS 00, 334 (2000)MathSciNetGoogle Scholar
  27. 27.
    Abadi, M.: Trusted computing, trusted third parties, and verified communications. In: SEC 2004: 19th IFIP International Information Security Conference (2004)Google Scholar
  28. 28.
    Peinado, M., Chen, Y., England, P., Manferdelli, J.: NGSCB: A Trusted Open System. Information Security and Privacy 3108/2004, 86–97 (2004)CrossRefGoogle Scholar
  29. 29.
    Pearson, S.: Trusted Computing Platforms: TCPA Technology in Context. Prentice-Hall, Englewood Cliffs (2002)Google Scholar
  30. 30.
    Abadi, M., Wobber, T.: A logical account of NGSCB. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol. 3236, Springer, Heidelberg (2004)Google Scholar
  31. 31.
    Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and implementation of a TCG-based integrity measurement architecture. In: 13th USENIX Security Symposium (2004)Google Scholar
  32. 32.
    Haldar, V., Chandra, D., Franz, M.: Semantic remote attestation: A virtual machine directed approach to trusted computing. In: USENIX VM (2004)Google Scholar
  33. 33.
    Haldar, V., Franz, M.: Symmetric behavior-based trust: A new paradigm for internet computing. In: New Security Paradigms Workshop (2004)Google Scholar
  34. 34.
    Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theoretical Computer Science 298(3) (2003)Google Scholar
  35. 35.
    Gordon, A.D., Jeffrey, A.S.A.: Authenticity by typing for security protocols. J. Computer Security 11(4) (2003)Google Scholar
  36. 36.
    Fournet, C., Gordon, A., Maffeis, S.: A type discipline for authorization policies. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, Springer, Heidelberg (2005)Google Scholar
  37. 37.
    Wobber, T., Yumerefendi, A., Abadi, M., Birrell, A., Simon, D.R.: Authorizing applications in Singularity. In: EuroSys 2007: Proceedings of the ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, Lisbon, Portugal, pp. 355–368. ACM, New York, NY, USA (2007)Google Scholar
  38. 38.
    Wallach, D.S., Appel, A.W., Felten, E.W.: SAFKASI: a security mechanism for language-based systems. ACM Trans. Softw. Eng. Methodol. 9(4) (2000)Google Scholar
  39. 39.
    Abadi, M., Fournet, C.: Access control based on execution history. In: Proceedings of the 10th Annual Network and Distributed System Security Symposium (2003)Google Scholar
  40. 40.
    Cardelli, L.: Program fragments, linking, and modularization. In: POPL 1997 (1997)Google Scholar
  41. 41.
    Bugliesi, M., Focardi, R., Maffei, M.: Compositional analysis of authentication protocols. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, Springer, Heidelberg (2004)Google Scholar
  42. 42.
    Bugliesi, M., Focardi, R., Maffei, M.: Analysis of typed analyses of authentication protocols. In: CSFW (2005)Google Scholar
  43. 43.
    Anderson, R., Kuhn, M.: Tamper resistance - a cautionary note. In: Second USENIX Workshop on Electronic Commerce Proceedings (1996)Google Scholar
  44. 44.
    Huang, A.: Hacking the Xbox. Xenatera Press (2003)Google Scholar
  45. 45.
    Arbaugh, W.A., Farber, D.J., Smith, J.M.: A secure and reliable bootstrap architecture. In: IEEE Symposium on Security and Privacy (1997)Google Scholar
  46. 46.
    Smith, S., Weingart, S.: Building a high-performance, programmable secure coprocessor. Computer Networks, Special Issue on Computer Network Security 31 (1999)Google Scholar
  47. 47.
    Irvine, C., Levin, T.: A cautionary note regarding the data integrity capacity of certain secure systems. In: Integrity, Internal Control and Security in Information Systems (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Andrew Cirillo
    • 1
  • James Riely
    • 1
  1. 1.CTIDePaul University 

Personalised recommendations