Secure calling contexts for stack inspection

ABSTRACT

Stack inspection is a mechanism for programming secure applications by which a method can obtain information from the call stack about the code that (directly or indirectly) invoked it. This mechanism plays a fundamental role in the security architecture of Java and the .NET Common Language Runtime. A central problem with stack inspection is to determine to what extent the <i>local</i> checks inserted into the code are sufficient to guarantee that a <i>global</i> security property is enforced. In this paper, we present a technique for inferring a <i>secure calling context</i> for a method. By a secure calling context we mean a pre-condition on the call stack sufficient for guaranteeing that execution of the method will not violate a given global property. This is particularly useful for annotating library code in order to avoid having to re-analyse libraries for every new application. The technique is a constraint based static program analysis implemented via fixed point iteration over an abstract domain of linear temporal logic properties.

REFERENCES

• 1: David F. Bacon , Peter F. Sweeney, Fast static analysis of C++ virtual function calls, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.324-341, October 06-10, 1996, San Jose, California, United States
• 2: Gilles Barthe , Dilian Gurov , Marieke Huisman, Compositional Verification of Secure Applet Interactions, Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering, p.15-32, April 08-12, 2002
• 3: M. Bartoletti, P. Degano, and G. Ferrari. Static analysis for stack inspection. In Proc. of Int. workshop on Concurrency and Coordination (ConCoord 2001), Electronic Notes in Theoretical Computer Science vol. 54. Elsevier, 2001.
• 4: 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
• 5: Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325703]
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: Patrick Cousot , Radhia Cousot, Automatic synthesis of optimal invariant assertions: Mathematical foundations, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.1-12, August 15-17, 1977
• 8: Patrick Cousot , Radhia Cousot, Formal language, grammar and set-constraint-based program analysis by abstract interpretation, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.170-181, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224199]
• 9: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 10: Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada [doi>10.1145/335169.335201]
• 11: 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
• 12: L. Gong. Going beyond the sandbox: An overview of the new security architecture in the Java development kit 1.2. In Proc. of USENIX Symposium on Internet Technologies and Systems, Dec. 1997.
• 13: David Grove , Greg DeFouw , Jeffrey Dean , Craig Chambers, Call graph construction in object-oriented languages, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.108-124, October 05-09, 1997, Atlanta, Georgia, United States
• 14: T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security properties. In Proc. of the 20th IEEE Symp. on Security and Privacy, pages 89--103. New York: IEEE Computer Society, 1999.
• 15: Microsoft Corp. Secure Coding Guidelines for the .NET Framework. Microsoft Corp., 2002.
• 16: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 17: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 18: Hemant D. Pande , Barbara G. Ryder, Data-Flow-Based Virtual Function Resolution, Proceedings of the Third International Symposium on Static Analysis, p.238-254, September 24-26, 1996
• 19: 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
• 20: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 21: 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
• 22: M. Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of Lecture Notes in Computer Science, pages 238--266. Springer-Verlag Inc., New York, NY, USA, 1996.
• 23: Dan Seth Wallach , Edward Felten, A new approach to mobile code security, 1999
• 24: D. S. Wallach and E. W. Felten. Understanding Java stack inspection. In 1998 IEEE Symposium on Security and Privacy, May 1998.

INDEX TERMS

Keywords:
constraints, language based security, linear temporal logic, stack inspection, static program analysis