Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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.
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.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pottier, F., Skalka, C., Smith, S. (2001). A Systematic Approach to Static Access Control. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_3
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive