Pluggable verification modules: an extensible protection mechanism for the JVM

ABSTRACT

Through the design and implementation of a JVM that supports Pluggable Verification Modules (PVMs), the idea of an extensible protection mechanism is entertained. Link-time bytecode verification becomes a pluggable service that can be readily replaced, reconfigured and augmented. Application-specific verification services can be safely introduced into the dynamic linking process of the JVM. This feature is enabled by the adoption of a previously proposed modular verification architecture, Proof Linking [23, 24], which decouples bytecode verification from the dynamic linking process, rendering the verifier a replaceable module. The PVM mechanism has been implemented in an open source JVM, the Aegis VM [21]. To evaluate the software engineering and security engineering benefits of this extensible protection mechanism, an augmented type system JAC (Java Access Control) [37] has been successfully implemented as a PVM.

REFERENCES

• 1: Jonathan Aldrich , Craig Chambers , David Notkin, ArchJava: connecting software architecture to implementation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581365]
• 2: Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 3: Wolfram Amme , Niall Dalton , Jeffery von Ronne , Michael Franz, SafeTSA: a type safe and referentially secure mobile-code representation based on static single assignment form, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.137-147, June 2001, Snowbird, Utah, United States
• 4: John Aycock , R. Nigel Horspool, Simple Generation of Static Single-Assignment Form, Proceedings of the 9th International Conference on Compiler Construction, p.110-124, March 25-April 02, 2000
• 5: B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
• 6: Joshua Bloch. JSR 175: A metadata facility for the Java programming language. http://www.jcp.org/en/jsr/detail?id=175
• 7: John Boyland, Alias burying: unique variables without destructive reads, Software—Practice & Experience, v.31 n.6, p.533-553, May 2001 [doi>10.1002/spe.370 ]
• 8: John Boyland , James Noble , William Retert, Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only, Proceedings of the 15th European Conference on Object-Oriented Programming, p.2-27, June 18-22, 2001
• 9: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 10: Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
• 11: Antonio Carzaniga , Gian Pietro Picco , Giovanni Vigna, Designing distributed applications with mobile code paradigms, Proceedings of the 19th international conference on Software engineering, p.22-32, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253236]
• 12: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 13: Alessandro Coglio and Allen Goldberg. Type safety in the JVM: Some problems in JDK 1.2.2 and proposed solutions. In Proceedings of the 2nd ECOOP Workshop on Formal Techniques for Java Programs Sophia Antipolis and Cannes, France, June 2000.
• 14: Susan Eisenbach, Formal underpinnings of Java, Addendum to the 1998 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), January 1998, Vancouver, British Columbia, Canada [doi>10.1145/346852.346968]
• 15: John Corwin , David F. Bacon , David Grove , Chet Murthy, MJ: a rational module system for Java and its applications, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 16: Patrick Doyle , Tarek S. Abdelrahman, A Modular and Extensible JVM Infrastructure, Proceedings of the 2nd Java™ Virtual Machine Research and Technology Symposium, p.65-78, August 01-02, 2002
• 17: Dominic Duggan, Type-Safe linking with recursive DLLs and shared libraries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.6, p.711-804, November 2002 [doi>10.1145/586088.586093]
• 18: ECMA. Common language infrastructure (CLI). Standard 335, ECMA, December 2002.
• 19: D. R. Engler , M. F. Kaashoek , J. O'Toole, Jr., Exokernel: an operating system architecture for application-level resource management, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.251-266, December 03-06, 1995, Copper Mountain, Colorado, United States
• 20: J. Ferber, Computational reflection in class based object-oriented languages, Conference proceedings on Object-oriented programming systems, languages and applications, p.317-326, October 02-06, 1989, New Orleans, Louisiana, United States
• 21: Philip W. L. Fong. The Aegis VM Project. http://aegisvm.sourceforge.net
• 22: Philip W. L. Fong, Proof linking: a modular verification architecture for mobile code systems, Simon Fraser University, Burnaby, BC, Canada, 2004
• 23: Philip W. L. Fong , Robert D. Cameron, Proof linking: modular verification of mobile programs in the presence of lazy, dynamic linking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.379-409, Oct. 2000 [doi>10.1145/363516.363523]
• 24: Philip W. L. Fong and Robert D. Cameron. Proof linking: Distributed verification of Java classfiles in the presence of multiple classloaders. In Proceedings of the USENIX Java Virtual Machine Research and Technology Symposium (JVM'01), pages 53--66, Monterey, California, USA, April 2001.
• 25: Philip W. L. Fong and Cheng Zhang. Capabilities as alias control: Secure cooperation in dynamically extensible systems. Technical Report CS-2004-3, Department of Computer Science, University of Regina, Regina, Saskatchewan, Canada S4S 0A2, 2004. ISBN:0-7731-0479-8.
• 26: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 27: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 28: Neal Glew , Greg Morrisett, Type-safe linking and modular assembly language, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292563]
• 29: Allen Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security, p.49-58, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288104]
• 30: Norman Hardy , Norm Hardy, The Confused Deputy: (or why capabilities might have been invented), ACM SIGOPS Operating Systems Review, v.22 n.4, p.36-38, Oct. 1988
• 31: Timothy L. Harris. Extensible virtual machines. Technical Report 525, University of Cambridge Computer Laboratory, Cambridge, UK, December 2001.
• 32: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 33: Sarfraz Khurshid , Darko Marinov , Daniel Jackson, An analyzable annotation language, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 34: Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Christina Videira Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. In Proceedings of the 11th European Conference on Object-Oriented Programming (ECOOP'97), volume 1241 of Lecture Notes in Computer Science Finland, June 1997. Springer-Verlag.
• 35: Gregor Kiczales , Erik Hilsdale , Jim Hugunin , Mik Kersten , Jeffrey Palm , William G. Griswold, An Overview of AspectJ, Proceedings of the 15th European Conference on Object-Oriented Programming, p.327-353, June 18-22, 2001
• 36: Gregor Kiczales , Jim Des Rivieres, The Art of the Metaobject Protocol, MIT Press, Cambridge, MA, 1991
• 37: Günter Kniesel , Dirk Theisen, JAC—access right based encapsulation for Java, Software—Practice & Experience, v.31 n.6, p.555-576, May 2001 [doi>10.1002/spe.372 ]
• 38: Sheng Liang , Gilad Bracha, Dynamic class loading in the Java virtual machine, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.36-44, October 18-22, 1998, Vancouver, British Columbia, Canada
• 39: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 40: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 41: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 42: Andrew C. Myers and Barbara Liskov. Complete, safe information flow with decentralized labels. In Proceedings of the 1998 IEEE Symposium on Security and Privacy (S&P'98), Oakland, California, USA, May 1998.
• 43: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 44: George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
• 45: Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292549]
• 46: K. Palacz , J. Baker , C. Flack , C. Grothoff , H. Yamauchi , J. Vitek, Engineering a customizable intermediate representation, Proceedings of the 2003 workshop on Interpreters, virtual machines and emulators, p.67-76, June 12-12, 2003, San Diego, California [doi>10.1145/858570.858578]
• 47: Zhenyu Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.638-672, July 2000 [doi>10.1145/363911.363915]
• 48: Zhenyu Qian , Allen Goldberg , Alessandro Coglio, A formal specification of Java class loading, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.325-336, October 2000, Minneapolis, Minnesota, United States
• 49: Jonathan A. Rees, A Security Kernel Based on the Lambda-Calculus, Massachusetts Institute of Technology, Cambridge, MA, 1996
• 50: Michael D. Schroeder. Cooperation of Mutually Suspicious Subsystems in a Computer Utility Ph.D. thesis, Massachusetts Institute of Technology, September 1972.
• 51: Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. Detecting format-string vulnerabilities with type qualifiers. In Proceedings of the 10th USENIX Security Symposium Washington, D.C., USA, August 2001.
• 52: Raymie Stata , Martin Abadi, A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.90-137, Jan. 1999 [doi>10.1145/314602.314606]
• 53: Tommy Thorn, Programming languages for mobile code, ACM Computing Surveys (CSUR), v.29 n.3, p.213-239, Sept. 1997 [doi>10.1145/262009.262010]
• 54: Raja Vallée-Rai , Phong Co , Etienne Gagnon , Laurie Hendren , Patrick Lam , Vijay Sundaresan, Soot - a Java bytecode optimization framework, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.13, November 08-11, 1999, Mississauga, Ontario, Canada
• 55: Jan Vitek , Boris Bokowski, Confined types in Java, Software—Practice & Experience, v.31 n.6, p.507-532, May 2001 [doi>10.1002/spe.369 ]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General
          Subjects: Protection mechanisms

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Domain-specific architectures
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages; Macro and assembly languages
      D.3.4 Processors
          Subjects: Run-time environments
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

Keywords:
Aegis VM, Java virtual machine, bytecode verification, extensible protection mechanism, extensible systems, mobile code security, pluggable verification modules, proof linking