Stack inspection: Theory and variants

ABSTRACT

Stack inspection is a security mechanism implemented in runtimes such as the JVM and the CLR to accommodate components with diverse levels of trust. Although stack inspection enables the fine-grained expression of access control policies, it has rather a complex and subtle semantics. We present a formal semantics and an equational theory to explain how stack inspection affects program behavior and code optimisations. We discuss the security properties enforced by stack inspection, and also consider variants with stronger, simpler properties.

REFERENCES

• 1: Abadi, M. and Fournet, C. 2003. Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Symposium (NDSS'03). Internet Society, 107--121.
• 2: Martín Abadi , Butler Lampson , Jean-Jacques Lévy, Analysis and caching of dependencies, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.83-91, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 3: Samson Abramsky , C.-H. Luke Ong, Full abstraction in the lazy lambda calculus, Information and Computation, v.105 n.2, p.159-267, Aug. 1993 [doi>10.1006/inco.1993.1044]
• 4: Banerjee, A. and Naumann, D. 2001. A simple semantics and static analysis for Java security. CS Report 2001--1, Stevens Institute of Technology.
• 5: Anindya Banerjee , David A. Naumann, Representation independence, confinement and access control [extended abstract], Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-177, January 16-18, 2002, Portland, Oregon
• 6: Bartoletti, M., Degano, P., and Ferrari, G. 2001. Static analysis for stack inspection. In ConCoord: International Workshop on Concurrency and Coordination. ENTCS, vol. 54. Elsevier North-Holland, Amsterdam, The Netherlands.
• 7: Nick Benton , Andrew Kennedy , George Russell, Compiling standard ML to Java bytecodes, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.129-140, September 26-29, 1998, Baltimore, Maryland, United States
• 8: Frédéric Besson , Thomas Jensen , Daniel Le Métayer , Tommy Thorn, Model checking security properties of control flow graphs, Journal of Computer Security, v.9 n.3, p.217-250, January 2001
• 9: Don Box , Ted Pattison, Essential .NET: The Common Language Runtime, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 10: Ulfar Erlingsson , Fred B. Schneider, IRM Enforcement of Java Stack Inspection, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.246, May 14-17, 2000
• 11: Fournet, C. and Gordon, A. D. 2001. Stack inspection: Theory and variants. Tech. Rep. MSR--TR--2001--103, Microsoft Research. http://research.microsoft.com/scripts/pubs/view.asp?TR_ID=MSR-TR-2001-103.
• 12: Cédric Fournet , Andrew D. Gordon, Stack inspection: theory and variants, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.307-318, January 16-18, 2002, Portland, Oregon
• 13: Li Gong, Inside Java 2 platform security architecture, API design, and implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 14: Andrew D. Gordon , Andrew M. Pitts, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 15: Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000 [doi>10.1145/371880.371887]
• 16: Norman Hardy , Norm Hardy, The Confused Deputy: (or why capabilities might have been invented), ACM SIGOPS Operating Systems Review, v.22 n.4, p.36-38, Oct. 1988
• 17: Douglas J. Howe, Proving congruence of bisimulation in functional programming languages, Information and Computation, v.124 n.2, p.103-112, Feb. 1, 1996 [doi>10.1006/inco.1996.0008]
• 18: Jensen, T., Metayer, D. L., and Thorn, T. 1999. Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, Calif., 89--103.
• 19: Guenter Karjoth, An Operational Semantics of Java 2 Access Control, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.224, July 03-05, 2000
• 20: .NET framework security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 21: François Rouaix , Xavier Leroy, Security properties of typed applets, Secure Internet programming: security issues for mobile and distributed objects, Springer-Verlag, London, 2001
• 22: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 23: Microsoft. 2001. NET Framework Developer's Guide: Security Optimizations. http://msdn.microsoft.com/library/en-us/cpguide/html/cpconsecurityoptimizations.asp.
• 24: Milner, R. 1977. Fully abstract models of typed lambda-calculi. Theoret. Comput. Sci. 4, 1--23.
• 25: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 26: Morris, J. H. 1968. Lambda-calculus models of programming languages. Ph.D. dissertation. MIT Cambridge, Mass.
• 27: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 28: Ørbæek, P. and Palsberg, J. 1997. Trust in the λ-calculus. J. Funct. Prog. 3, 2, 75--85.
• 29: Plotkin, G. D. 1975. Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1, 125--159.
• 30: François Pottier , Christian Skalka , Scott F. Smith, A Systematic Approach to Static Access Control, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.30-45, April 02-06, 2001
• 31: Schinz, M. and Odersky, M. 2001. Tail call elimination on the Java Virtual Machine. In Proceedings of the SIGPLAN Workshop on Multi-Language Infrastructure and Interoperability (BABEL'01). ENTCS, vol. 59(1). Elsevier North Holland, Amsterdam, The Netherlands, 155--168.
• 32: Christian Skalka , Scott Smith, Static enforcement of security with types, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.34-45, September 2000
• 33: Dan S. Wallach , Andrew W. Appel , Edward W. Felten, SAFKASI: a security mechanism for language-based systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.341-378, Oct. 2000 [doi>10.1145/363516.363520]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
      F.3.2 Semantics of Programming Languages
      F.3.3 Studies of Program Constructs

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Languages, Security, Theory

Keywords:
Access control, contextual equivalence, equational reasoning, operational semantics, stack inspection