Proof linking: an architecture for modular verification of dynamically-linked mobile code

ABSTRACT

Security flaws are routinely discovered in commercial implementations of mobile code systems such as the Java Virtual Machine (JVM). Typical architectures for such systems exhibit complex interdependencies between the loader, the verifier, and the linker, making them difficult to craft, validate, and maintain. This reveals a software engineering challenge that is common to all mobile code systems in which a static verification phase is introduced before dynamic linking. In such systems, one has to articulate how loading, verification, and linking interact with each other, and how the three processes should be organized to address various security issues.We propose a standard architecture for crafting mobile code verifiers, based on the concept of proof linking. This architecture modularizes the verification process and isolates the dependencies among the loader, verifier, and linker. We also formalize the process of proof linking and establish properties to which correct implementations must conform. As an example, we instantiate our architecture for the problem of Java bytecode verification and assess the correctness of this instantiation. Finally, we briefly discuss alternative mobile code verification architectures enabled by our modularization.

REFERENCES

• 1: 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]
• 2: 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]
• 3: D. Clark and D. Wilson. A comparison of commercial and military computer security policies. In Proceedings of the IEEE Symposium on Security and Privacy, pages 184-194, 1987.
• 4: Drew Dean, The security of static typing with dynamic linking, Proceedings of the 4th ACM conference on Computer and communications security, p.18-27, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266428]
• 5: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 6: Premkumar T. Devanbu , Philip W-L Fong , Stuart G. Stubblebine, Techniques for trusted software engineering, Proceedings of the 20th international conference on Software engineering, p.126-135, April 19-25, 1998, Kyoto, Japan
• 7: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 8: The Secure Internet Programming Group. History of the group, 1997. Availablat at http://nvu.cs.princeton.edu/sip/History.html.
• 9: Stanley Letovsky and Elliot Soloway. Delocalized Plans and Program Comprehension. IEEE Software, pages 41-49, May 1986.
• 10: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 11: Daryl McCullough. Specification for Multi-Level Security and a Hook-Up Property. In Proceedings for the IEEE Symposium on Security and Privacy, pages 161- 166, 1987.
• 12: Daryl McCullough. Noninterference and the Composability of Security Properties. In Proceedings of the IEEE Symposium on Security and Privacy, pages 1' 77- 186, 1988.
• 13: Gary McGraw , Edward W. Felten, Java security: hostile applets, holes&antidotes, John Wiley & Sons, Inc., New York, NY, 1997
• 14: 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]
• 15: Spencer Rugaber, Kurt Stirewalt, and Linda W. WilIs. The Interleaving Problem in Program Understanding. In 2nd Working Conference on Reverse Engineering, pages 166-175, Toronto, Ontario, Canada, July 1995.
• 16: SRI International Computer Science Laboratory. The PVS verification system. Available athttp://wuu.csl.sri.com/pvs.html.
• 17: The Kiiera Team. Security Flaws in Java Implementations, 1997. Available athttp://kimera.cs.washington.edu/flaus/.
• 18: Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
• 19: B. W. Weide and J. E. HoIIingsworth. Scalability of Reuse Technology to Large Systems Requires Local Certifiability. In Proceedings of the 5th Annual Workshop on Software Reuse, 1992.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Code inspections and walk-throughs

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS

General Terms:
Design, Languages, Performance, Security, Theory, Verification