A systematic approach to static access control

ABSTRACT

The Java Security Architecture includes a dynamic mechanism for enforcing access control checks, the so-called stack inspection process. While the architecture has several appealing features, access control checks are all implemented via dynamic method calls. This is a highly nondeclarative form of specification that is hard to read, and that leads to additional run-time overhead. This article develops type systems that can statically guarantee the success of these checks. Our systems allow security properties of programs to be clearly expressed within the types themselves, which thus serve as static declarations of the security policy. We develop these systems using a systematic methodology: we show that the security-passing style translation, proposed by Wallach et al. [2000] as a dynamic implementation technique, also gives rise to static security-aware type systems, by composition with conventional type systems. To define the latter, we use the general HM(X) framework, and easily construct several constraint- and unification-based type systems.

REFERENCES

• 1: Manuel Fähndrich , Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, Proceedings of the 4th International Symposium on Static Analysis, p.114-126, September 08-10, 1997
• 2: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 3: Banerjee, A. and Naumann, D. A. 2001. A simple semantics and static analysis for Java security. Tech. Rep. 2001-1, Stevens Institute of Technology. June. URL: http://guinness.cs.stevens-tech.edu/~naumann/publications/tr2001.ps.
• 4: Bartoletti, M., Degano, P., and Ferrari, G. 2001. Static analysis for stack inspection. In International Workshop on Concurrency and Coordination. Electronic Notes in Theoretical Computer Science, vol. 54. Elsevier Science, Amsterdam, The Netherlands.
• 5: Frédéric Besson , Thomas de Grenier de Latour , Thomas Jensen, Secure calling contexts for stack inspection, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.76-87, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571166]
• 6: 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
• 7: Clements, J. and Felleisen, M. 2003. A tail-recursive semantics for stack inspections. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2618. Springer-Verlag, New York, 22--37. URL: http://www.ccs.neu.edu/scheme/pubs/esop2003-cf.ps.gz.
• 8: Ú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]
• 9: Andrzej Filinski, Representing layered monads, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.175-188, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292557]
• 10: 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
• 11: Gong, L. 1998. Java security architecture (JDK1.2). URL: http://java.sun.com/products/jdk/1.2/docs/guide/security/spec/security-spec.doc.html.
• 12: Gong, L. and Schemers, R. 1998. Implementing protection domains in the Java Development Kit 1.2. In Proceedings of the Internet Society Symposium on Network and Distributed System Security. 125--134. URL: http://java.sun.com/people/gong/papers/jdk12impl.ps.gz.
• 13: Guzmán, J. C. and Suárez, A. 1994. An extended type system for exceptions. In Proceedings of the ACM Workshop on ML and its Applications. Number 2265 in INRIA Research Reports. INRIA, 127--135.
• 14: Tomoyuki Higuchi , Atsushi Ohori, A static type system for JVM access control, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.227-237, August 25-29, 2003, Uppsala, Sweden
• 15: Jensen, T., Le Mètayer, D., and Thorn, T. 1999. Verifying security properties of control-flow graphs. In Proceedings of the IEEE Symposium on Security and Privacy (S&P). IEEE Computer Society Press, Los Alamitos, Calif., 89--105. URL: http://www.irisa.fr/lande/jensen/papers/SP99.ps.
• 16: Larry Koved , Marco Pistoia , Aaron Kershenbaum, Access rights analysis for Java, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 17: Charlie Lai , Li Gong , Larry Koved , Anthony Nadalin , Roland Schemers, User Authentication and Authorization in the Java(tm) Platform, Proceedings of the 15th Annual Computer Security Applications Conference, p.285, December 06-10, 1999
• 18: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 19: Gleb Naumovich, A conservative algorithm for computing the flow of permissions in Java programs, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 20: Martin Odersky , Martin Sulzmann , Martin Wehr, Type inference with constrained types, Theory and Practice of Object Systems, v.5 n.1, p.35-55, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4]
• 21: Xavier Leroy , François Pessaux, Type-based analysis of uncaught exceptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.340-377, March 2000 [doi>10.1145/349214.349230]
• 22: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 23: François Pottier, A versatile constraint-based type inference system, Nordic Journal of Computing, v.7 n.4, p.312-347, Winter 2000
• 24: François Pottier, A Constraint-Based Presentation and Generalization of Rows, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.331, June 22-25, 2003
• 25: François Pottier , Sylvain Conchon, Information flow inference for free, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.46-57, September 2000
• 26: 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
• 27: Rémy, D. 1992a. Extending ML type system with a sorted equational theory. Tech. Rep. 1766, INRIA, Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France. URL: ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/eq-theory-on-types.ps.gz.
• 28: Didier Rémy, Projective ML, Proceedings of the 1992 ACM conference on LISP and functional programming, p.66-75, June 22-24, 1992, San Francisco, California, United States
• 29: Didier Rémy, Type inference for records in natural extension of ML, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 30: 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]
• 31: Simonet, V. 2003. Type inference with structural subtyping: a faithful formalization of an efficient constraint solver. In Proceedings of the Asian Symposium on Programming Languages and Systems. URL: http://cristal.inria.fr/~simonet/publis/simonet-structural-subtyping.ps.gz.
• 32: Christian Edward Skalka , Scott Smith, Types for programming language-based security, 2003
• 33: Skalka, C. and Pottier, F. 2002. Syntactic type soundness for HM(X). In Proceedings of the Workshop on Types in Programming (TIP). Electronic Notes in Theoretical Computer Science, vol. 75. URL: http://pauillac.inria.fr/~fpottier/publis/skalka-fpottier-tip-02.ps.gz.
• 34: 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
• 35: M. Spivey, A functional theory of exceptions, Science of Computer Programming, v.14 n.1, p.25-42, Jun. 1990 [doi>10.1016/0167-6423(90)90056-J]
• 36: Zhendong Su , Alexander Aiken, Entailment with Conditional Equality Constraints, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.170-189, April 02-06, 2001
• 37: Martin Franz Sulzmann , Paul Hudak, A general framework for hindley/milner type systems with constraints, 2000
• 38: Sulzmann, M., Müller, M., and Zenger, C. 1999. Hindley/Milner style type systems in constraint form. Research Report ACRC--99--009, University of South Australia, School of Computer and Information Science. July. URL: http://www.ps.uni-sb.de/~mmueller/papers/hm-constraints.ps.gz.
• 39: Peter Thiemann, Enforcing Safety Properties Using Type Specialization, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.62-76, April 02-06, 2001
• 40: Philip Wadler , Peter Thiemann, The marriage of effects and monads, ACM Transactions on Computational Logic (TOCL), v.4 n.1, p.1-32, January 2003 [doi>10.1145/601775.601776]
• 41: Philip Wadler, How to replace failure by a list of successes, Proc. of a conference on Functional programming languages and computer architecture, p.113-128, January 1985, Nancy, France
• 42: David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
• 43: Dan Seth Wallach , Edward Felten, A new approach to mobile code security, 1999
• 44: 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]
• 45: Andrew K. Wright , Robert Cartwright, A practical soft type system for scheme, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.87-152, Jan. 1997 [doi>10.1145/239912.239917]
• 46: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Reliability, Security, Theory

Keywords:
Type systems, access control, stack inspection