Abstract
In order to run untrusted code in the same process as trusted code, there must be a mechanism to allow dangerous calls to determine if their caller is authorized to exercise the privilege of using the dangerous routine. Java systems have adopted a technique called stack inspection to address this concern. But its original definition, in terms of searching stack frames, had an unclear relationship to the actual achievement of security, overconstrained the implementation of a Java system, limited many desirable optimizations such as method inlining and tail recursion, and generally interfered with interprocedural optimization. We present a new semantics for stack inspection based on a belief logic and its implementation using the calculus of security-passing style which addresses the concerns of traditional stack inspection. With security-passing style, we can efficiently represent the security context for any method activation, and we can build a new implementation strictly by rewriting the Java bytecodes before they are loaded by the system. No changes to the JVM or bytecode semantics are necessary. With a combination of static analysis and runtime optimizations, our prototype implementation showes reasonable performance (although traditional stack inspection is still faster), and is easier to consider for languages beyond Java. We call our system SAFKASI (the Security Architecture Formerly Known as Stack Inspection).
- ABADI, M., BURROWS, M., LAMPSON, B., AND PLOTKIN, G. 1993. A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst. 15, 4 (Sept.), 706-734.]] Google Scholar
- BACK, G AND HSIEH, W. 1999. Drawing the red line in Java. In Proceedings of the 7th IEEE Workshop on Hot Topics in Operating Systems (Rio Rico, AZ, Mar.). IEEE Computer Society Press, Los Alamitos, CA. http://www.cs.utah.edu/flux/papers/redline-hotos7.ps.]] Google Scholar
- BACK, G., TULLMANN, P., STOLLER, L., HSIEH,W.C.,AND LEPREAU, J. 2000. Techniques for the design of Java operating system. In Proceedings of the 2000 Usenix Annual Technical Conference (San Diego, CA, June).]] Google Scholar
- BERNADAT, P., LAMBRIGHT, D., AND TRAVOSTINO, F. 1998. Towards a resource-safe Java for service guarantees in uncooperative environments. In Proceedings of the IEEE Workshop on Programming Languages for Real-Time Industrial Applications (Madrid, Spain, Dec.).]]Google Scholar
- BROMLEY, H. 1986. Lisp Lore: A Guide to Programming the Lisp Machine. Kluwer Academic Publishers, Hingham, MA.]] Google Scholar
- BURROUGHS CORP. 1969. Burroughs B6500 Information processing systems reference manual.]]Google Scholar
- BURROWS, M., ABADI, M., AND NEEDHAM, R. 1990. A logic of authentication. ACM Trans. Comput. Syst. 8, 1 (Feb.), 18-36.]] Google Scholar
- COHEN, G., CHASE, J., AND KAMINSKY, D. 1998. Automatic program transformation with JOIE. In Proceedings of the 23rd on USENIX Annual Conference (New Orleans, Louisiana, June). USENIX Assoc., Berkeley, CA, 167-178.]] Google Scholar
- CZAJKOWSKI,G.AND VON EICKEN, T. 1998. JRes: A resource accounting interface for Java. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '98, Vancouver, B. C., Canada, Oct. 18-12), B. Freeman-Benson and C. Chambers, Chairs. ACM Press, New York, NY, 21-35.]] Google Scholar
- DEAN, J., GROVE, D., AND CHAMBERS, C. 1995. Optimization of object-oriented programs using static class hierarchy analysis. In Proceedings of the Ninth European Conference on Object-Oriented Programming (ECOOP '95, Aarhus, Denmark, Aug.). Springer-Verlag, New York, NY.]] Google Scholar
- DEFOUW, G., GROVE, D., AND CHAMBERS, C. 1998. Fast interprocedural class analysis. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98, San Diego, CA, Jan. 19-21), D. B. MacQueen and L. Cardelli, Chairs. ACM Press, New York, NY, 222-236.]] Google Scholar
- DIWAN, A., MOSS,J.E.B.,AND MCKINLEY, K. S. 1996. Simple and effective analysis of statically typed object-oriented programs. In Proceedings of the Eleventh Annual Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '96, San Jose, CA, Oct. 6-10), L. Anderson and J. Coplien, Chairs. ACM Press, New York, NY, 292-305.]] Google Scholar
- EVANS, D. AND TWYMAN, A. 1999. Flexible policy-directed code safety. In Proceedings of the 1999 IEEE Symposium on Security and Privacy (Oakland, California, May). 32-45.]]Google Scholar
- FERNANDEZ, M. 1995. Simple and effective link-time optimization of Modula-3 programs. In Proceedings of the ACM SIGPLAN '95 Conference on Program Language Design and Implementation. ACM Press, New York, NY, 103-115.]] Google Scholar
- FLATT, M., FINDLER, R. B., KRISHNAMURTHY, S., AND FELLEISEN, M. 1999. Programming languages as operating systems: (or revenge of the son of the Lisp machine). In Proceedings of the 1999 ACM International Conference on Functional Programming (ICFP '99, Paris, France, Sept). http://www.cs.rice.edu/CS/PLT/Publications/icfp99-ffkf.ps.gz.]] Google Scholar
- FRIEDMAN-HILL, E. J. 1997. Jess: The Java Expert System Shell. Sandia National Laboratories, Livermore, CA. http://herzberg1.ca.sandia.gov/jess/]]Google Scholar
- GOLDBERG, A. AND ROBSON, D. 1989. Smalltalk-80: The Language. Addison-Wesley, Reading, MA.]] Google Scholar
- GONG, L. 1999. Inside Java 2 Platform Security: Architecture, API Design, and Implementation. Addison-Wesley, Reading, MA.]] Google Scholar
- GONG, L. AND SCHEMERS, R. 1998. Implementing protection domains in the Java Development Kit 1.2. In Proceedings of the 1998 Internet Society Symposium on Network and Distributed System Security (San Diego, CA, Mar.).]]Google Scholar
- GOSLING, J., JOY, B., AND STEELE, G. 1996. The Java Language Specification. Addison-Wesley, Reading, MA.]] Google Scholar
- GRISWOLD, D. 1998. The Java HotSpot Virtual Machine Architecture. Sun Microsystems Laboratories. http://java.sun.com/products/hotspot/whitepaper.html]]Google Scholar
- HARDY, N. 1988. The confused deputy. ACM SIGOPS Oper. Syst. Rev. 22, 4 (Oct.), 36-38. http://www.cis.upenn.edu/ KeyKOS/ConfusedDeputy.html]] Google Scholar
- HAWBLITZEL, C., CHANG, C.-C., CZAJKOWSKI, G., HU, D., AND VON EICKEN, T. 1998. Implementing multiple protection domains in Java. In Proceedings of the Annual Technical Conference on USENIX (New Orleans, LA, June). USENIX Assoc., Berkeley, CA.]] Google Scholar
- HENNESSY, J. L. 1982. Symbolic debugging of optimized code. ACM Trans. Program. Lang. Syst. 4, 4 (Oct.), 323-344.]] Google Scholar
- HICKS, M., KAKKAR, P., MOORE, J. T., GUNTER, C. A., AND NETTLES, S. 1998. PLAN: A packet language for active networks. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming Languages (ICFP '98, Baltimore, MD, Sept. 27-29), M. Felleisen, P. Hudak, and C. Queinnec, Chairs. ACM Press, New York, NY, 86-93. http://www.cis.upenn.edu/ switchware/papers/plan.ps]] Google Scholar
- LAMPSON, B. 1974. Protection. In Proceedings of the 5th Princeton Symposium on Information Sciences and Systems (Princeton, NJ, Mar.). 437-443.]]Google Scholar
- LAMPSON, B., ABADI, M., BURROWS, M., AND WOBBER, E. 1992. Authentication in distributed systems: Theory and practice. ACM Trans. Comput. Syst. 10, 4 (Nov.), 265-310.]] Google Scholar
- LINDHOLM, T. AND YELLIN, F. 1997. The Java Virtual Machine Specification. Addison-Wesley, Reading, MA.]] Google Scholar
- MYERS, A. C. 1999. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL, San Antonio, TX, Jan.). 228-241.]] Google Scholar
- MICROSOFT CORPORATION. 1997. Microsoft Security Management Architecture White Paper. Microsoft Corp., Redmond, WA. http://www.microsoft.com/ie/security/ie4security.htm.]]Google Scholar
- NATURALBRIDGE, LLC. 1998. BulletTrain Java Compiler. http://www.naturalbridge.com.]]Google Scholar
- NECULA, G. C. AND LEE, P. 1996. Safe kernel extensions without run-time checking. In Proceedings of the 2nd USENIX Symposium on Operating Systems Design and Implementation (OSDI '96, Seattle, WA, Oct. 28-31), K. Petersen and W. Zwaenepoel, Chairs. ACM Press, New York, NY, 229-243.]] Google Scholar
- NECULA, G. C. AND LEE, P. 1997. Safe, untrusted agents using proof-carrying code. In Mobile Agent Security. Springer-Verlag, New York, NY.]] Google Scholar
- NETSCAPE CORP. 1997. Introduction to the capabilities classes. Netscape Corp. http://developer.netscape.com/library/documentation/signedobj/capabilities/index.html.]]Google Scholar
- REDELL, D., DALAL, Y., HORSLEY, T., LAUER, H., LYNCH, W., MCJONES, P., MURRAY, H., AND PURCELL, S. C. 1980. Pilot: An operating system for a personal computer. Commun. ACM 23, 2 (Apr.), 81-92.]] Google Scholar
- ROSKIND, J. 1996. Evolving the security model for Java from Navigator 2.x to Navigator 3.x. Netscape Corp. http://developer.netscape.com/library/technote/security/sectn1.html.]]Google Scholar
- SALTZER, J. H. AND SCHROEDER, M. D. 1975. The protection of information in computer systems. In Proceedings of the IEEE. IEEE Press, Piscataway, NJ, 1278-1308.]]Google Scholar
- SAULPAUGH, T., CLEMENTS, T., AND MIRHO, C. A. 1999. Inside the JavaOS Operating System. Addison-Wesley, Reading, MA.]]Google Scholar
- SIRER, E. G., GRIMM, R., GREGORY, A. J., AND BERSHAD, B. N. 1999. Design and implementation of a distributed virtual machine for networked computers. In Proceedings of the 17th ACM Symposium on Operating System Principles (Kiawah Island Resort, SC, Dec.). ACM Press, New York, NY, 202-216.]] Google Scholar
- SPOONHOWER, D., CZAJKOWSKI, G., HAWBLITZEL, C., CHANG, C.-C., HU, D., AND VON EICKEN,T. 1998. Design and evaluation of an extensible web & telephony server based on the J-Kernel. 98-1715 (Nov.). Department of Computer Science, Cornell University, Ithaca, NY. http://www2.cs.cornell.edu/slk/papers/tr98-1715.pdf]] Google Scholar
- STEELE, G. L. 1978. Rabbit: A compiler for scheme. AI-TR-474. MIT Press, Cambridge, MA.]] Google Scholar
- SWINEHART, D. C., ZELLWEGER, P. T., BEACH, R. J., AND HAGMANN, R. B. 1986. A structural view of the Cedar programming environment. ACM Trans. Program. Lang. Syst. 8, 4 (Oct.), 419-490.]] Google Scholar
- TOLMACH, A. P. AND APPEL, A. W. 1990. Debugging standard ML without reverse engineering. In Proceedings of the 1990 ACM Symposium on LISP and Functional Programming (Nice, France, June 27-29), G. Kahn, Chair. ACM Press, New York, NY, 1-12.]] Google Scholar
- VAN DOORN, L. 2000. A secure Java virtual machine. In Proceedings of the Ninth USENIX Security Symposium (Denver, CO, Aug.).]] Google Scholar
- WALLACH, D. S. AND FELTEN, E. W. 1998. Understanding Java stack introspection. In Proceedings of the 1998 IEEE Symposium on Security and Privacy (Oakland, CA, May). IEEE Computer Society Press, Los Alamitos, CA, 52-63.]]Google Scholar
- WALLACH, D. S., BALFANZ, D., DEAN, D., AND FELTEN, E. W. 1997. Extensible security architectures for Java. In Proceedings of the Sixteenth ACM Symposium on Operating System Principles (Saint-Malo, France, Oct.). 116-128.]] Google Scholar
- WILLE, C. 2000. Presenting C#. SAMS, Carmel, IN.]] Google Scholar
- WIRTH, N. AND GUTKNECHT, J. 1992. Project Oberon: the design of an operating system and compiler. ACM Press/Addison-Wesley Publ. Co., New York, NY.]] Google Scholar
- WOBBER, E., ABADI, M., BURROWS, M., AND LAMPSON, B. 1994. Authentication in the Taos operating system. ACM Trans. Comput. Syst. 12, 1 (Feb.), 3-32.]] Google Scholar
Index Terms
- SAFKASI: a security mechanism for language-based systems
Recommendations
An efficient security verification method for programs with stack inspection
CCS '01: Proceedings of the 8th ACM conference on Computer and Communications SecurityStack inspection is a key technology for runtime access control of programs in a network environment. In this paper, a verification problem to decide whether a given program with stack inspection satisfies a given security property is discussed. First, ...
A java toolkit for teaching distributed algorithms
ITiCSE '02: Proceedings of the 7th annual conference on Innovation and technology in computer science educationWe present a toolkit for developing and visualizing distributed algorithms in Java. This toolkit consists of a Java class library with a simple programming interface that allows to develop distributed algorithms in a message passing model. The resulting ...
Static check analysis for Java stack inspection
Most static analysis techniques for optimizing stack inspection approximate permission sets such as granted permissions and denied permissions. Because they compute permission sets following control flow, they usually take intra-procedural control flow ...
Comments