A Systematic Approach to Static Access Control
The Java JDK 1.2 Security Architecture includes a dynamic mechanism for enforcing access control checks, so-called stack inspection. This paper studies type systems which can statically guarantee the success of these checks. We develop these systems using a new, systematic methodology: we show that the security-passing style translation, proposed by Wallach and Felten 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. They offer significant improvements on a previous type system for JDK access control, both in terms of expressiveness and in terms of readability of inferred type specifications.
KeywordsAccess Control Type System Security Policy Operational Semantic Security Architecture
- Alexander S. Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Principles of Programming Languages, pages 163–173, January 1994. URL: http://http.cs.berkeley.edu/~aiken/ftp/popl94.ps.
- Li Gong. Java security architecture (JDK1.2). URL: http://java.sun.com/products/jdk/1.2/docs/guide/security/spec/ security-spec.doc.html, October 1998.
- Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35–55, 1999. URL: http://www.cs.mu.oz.au/~sulzmann/publications/tapos.ps.CrossRefGoogle Scholar
- François Pottier. A 3-part type inference engine. In Gert Smolka, editor, Proceedings of the 2000 European Symposium on Programming (ESOP’00), volume 1782 of Lecture Notes in Computer Science, pages 320–335. Springer Verlag, March 2000. URL: http://pauillac.inria.fr/ fpottier/publis/fpottier-esop-2000.ps.gz.Google Scholar
- François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP’00), pages 46–57, September 2000. URL: http://pauillac.inria.fr/ fpottier/publis/fpottier-conchon-icfp00.ps.gz.
- Didier Rémy. Extending ML type system with a sorted equational theory. Technical Report 1766, INRIA, Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France, 1992. URL: ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/eq-theory-on-types.ps.gz.Google Scholar
- Didier Rémy. Projective ML. In 1992 ACM Conference on Lisp and Functional Programming, pages 66–75, New-York, 1992. ACM Press. URL: ftp://ftp.inria.fr/INRIA/Projects/cristal/ Didier.Remy/lfp92.ps.gz.
- Christian Skalka and Scott Smith. Static enforcement of security with types. In Proceedings of the the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP’00), pages 34–45, Montr al, Canada, September 2000. URL: http://www.cs.jhu.edu/~ces/papers/secty_icfp2000.ps.gz.
- Martin Sulzmann, Martin Müller, and Christoph Zenger. Hindley/Milner style type systems in constraint form. Research Report ACRC-99-009, University of South Australia, School of Computer and Information Science, July 1999. URL: http://www.ps.uni-sb.de/~mmueller/papers/hm-constraints.ps.gz.
- Peter Thiemann. Enforcing security properties using type specialization. In David Sands, editor, Proceedings of the 2001 European Symposium on Programming (ESOP’01), Lecture Notes in Computer Science. Springer Verlag, April 2001.Google Scholar
- Philip Wadler and Peter Thiemann. The marriage of effects and monads. Submitted to ACM Transactions on Computational Logic. URL: http://cm.bell-labs.com/cm/cs/who/wadler/papers/ effectstocl/effectstocl.ps.gz.
- David Walker. A type system for expressive security policies. In Conference Record of POPL’00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 254–267, Boston, Massachusetts, January 2000. URL: http://www.cs.cornell.edu/home/walker/papers/sa-popl00_ps.gz.
- Dan S. Wallach. A New Approach to Mobile Code Security. PhD thesis, Princeton University, January 1999. URL: http://www.cs.princeton.edu/sip/pub/dwallach-dissertation.html.
- Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, November 1994. URL: http://www.cs.rice.edu/CS/PLT/Publications/ic94-wf.ps.gz.zbMATHCrossRefMathSciNetGoogle Scholar