Abstract
Security of mobile code is a major issue in today’s global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something undesirable? In this paper I will discuss a particular approach to this problem called language-based security. In this approach, security information is derived from a program written in a high-level language during the compilation process and is included in the compiled object. This extra security information can take the form of a formal proof, a type annotation, or some other form of certificate or annotation. It can be downloaded along with the object code and automatically verified before running the code locally, giving some assurance against certain types of failure or unauthorized activity. The verifier must be trusted, but the compiler, code, and certificate need not be. Java bytecode verification is an example of this approach. I will give an overview of some recent work in this area, including a particular effort in which we are trying to make the production of certificates and the verification as efficient and invisible as possible.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and R. Stata. A type system for Java bytecode subroutines. In Proc. 25th Symp. Principles of Programming Languages, pages 149–160. ACM SIG-PLAN/SIGACT, January 1998.
B. Bershad, S. Savage, P. Pardyak, E. G. Sirer, D. Becker, M. Fiuczynski, C. Chambers, and S. Eggers. Extensibility, safety, and performance in the SPIN operating system. In Proc. 15th Symp. Operating System Principles, pages 267–284. ACM, December 1995.
K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th Symp. Principles of Programming Languages, pages 262–275. ACM SIGPLAN/SIGACT, January 1999.
Drew Dean, Ed Felten, and Dan Wallach. JAVA security: From HotJava to Netscape and beyond. In Proc. Symp. Security and Privacy. IEEE, May 1996.
Whitfield Diffie and Susan Landau. Privacy on the Line: The Politics of Wiretapping and Encryption. MIT Press, 1998.
Ulfar Erlingsson and Fred B. Schneider. SASI enforcement of security policies: A retrospective, April 1999. Preprint.
N. Glew and G. Morrisett. Type-safe linking and modular assembly language. In Proc. 26th Symp. Principles of Programming Languages, pages 250–261. ACM SIGPLAN/SIGACT, January 1999.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. Assoc. Comput. Mach., 40(1):143–184, January 1993.
Luke Hornof and Trevor Jim. Certifying compilation and run-time code generation. In Proc. Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 60–74. ACM, January 1999.
Bill Joy and Ken Kennedy, co-chairs. Information Technology Research: Investing in Our Future. President’s Information Technology Advisory Committee, February 1999. http://www.ccic.gov/.
Dexter Kozen. Efficient code certification. Technical Report 98-1661, Computer Science Department, Cornell University, January 1998.
Tim Lindholm and Frank Yellin. The JAVA virtual machine specification. Addison Wesley, 1996.
G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Proc. Workshop on Compiler Support for System Software, pages 25–35. ACM SIGPLAN, May 1999.
G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In Xavier Leroy and Atsushi Ohori, editors, Proc. Workshop on Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28–52. Springer-Verlag, March 1998.
G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In 1996 Workshop on Compiler Support for Systems Software, 1996.
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In 25th ACM SIGPLAN/SIGSIGACT Symposium on Principles of Programming Languages, pages 85–97, San Diego California, USA, January 1998.
Andrew C. Myers. JFlow: Practical static information flow control. In Proc. 26th Symp. Principles of Programming Languages. ACM, January 1999.
Andrew C. Myers and Barbara Liskov. A decentralized model for information flow control. In Proc. 16th Symp. Operating System Principles, pages 129–142. ACM, October 1997.
Andrew C. Myers and Barbara Liskov. Complete, safe information flow with decentralized labels. In Proc. Symp. Security and Privacy, pages 186–197. IEEE, May 1998.
National Coordination Office for Computing, Information, and Communications. Information Technology for the 21st Century: A Bold Investment in America’s Future, 24 January 1999. Draft. http://www.ccic.gov/.
George C. Necula. Proof-carrying code. In Proc. 24th Symp. Principles of Programming Languages, pages 106–119. ACM SIGPLAN/SIGACT, January 1997.
George C. Necula. Compiling with proofs. PhD thesis, Carnegie Mellon University, September 1998.
George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proc. 2nd Symp. Operating System Design and Implementation. ACM, October 1996.
George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Proc. Conf. Programming Language Design and Implementation, pages 333–344. ACM SIGPLAN, 1998.
George C. Necula and Peter Lee. Efficient representation and validation of proofs. In Proc. 13th Symp. Logic in Computer Science, pages 93–104. IEEE, June 1998.
George C. Necula and Peter Lee. Safe, untrusted agents using using proof-carrying code. In Giovanni Vigna, editor, Special Issue on Mobile Agent Security, volume 1419 of Lect. Notes in Computer Science, pages 61–91. Springer-Verlag, June 1998.
Robert O’Callahan. A simple, comprehensive type system for Java bytecode subroutines. In Proc. 26th Symp. Principles of Programming Languages, pages 70–78. ACM SIGPLAN/SIGACT, January 1999.
Fred B. Schneider. Towards fault-tolerant and secure agentry. In Proc. 11th Int. Workshop WDAG’ 97, volume 1320 of Lecture Notes in Computer Science, pages 1–14. ACM SIGPLAN, Springer-Verlag, September 1997.
Fred B. Schneider. Enforceable security policies. Technical Report TR98-1664, Computer Science Department, Cornell University, January 1998.
Fred B. Schneider, editor. Trust in Cyberspace. Committee on Information Systems Trustworthiness, Computer Science and Telecommunications Board, National Research Council. National Academy Press, 1999.
D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In Conf. Programming Language Design and Implementation. ACM SIGPLAN, 1996.
R. Wahbe, S. Lucco, T. E. Anderson, and S. L Graham. Efficient software-based fault isolation. In Proc. 14th Symp. Operating System Principles, pages 203–216. ACM, December 1993.
David Walker. A type system for expressive security policies. In Proc. FLOC’99 Workshop on Run-time Result Verification, July 1999. To appear.
Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Proc. Conf. Programming Language Design and Implementation, pages 249–257. ACM SIGPLAN, June 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kozen, D. (1999). Language-Based Security. In: Kutyłowski, M., Pacholski, L., Wierzbicki, T. (eds) Mathematical Foundations of Computer Science 1999. MFCS 1999. Lecture Notes in Computer Science, vol 1672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48340-3_26
Download citation
DOI: https://doi.org/10.1007/3-540-48340-3_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66408-6
Online ISBN: 978-3-540-48340-3
eBook Packages: Springer Book Archive