Java bytecode specification and verification

ABSTRACT

We propose a framework for establishing the correctness of untrusted Java bytecode components w.r.t. to complex functional and/or security policies. To this end, we define a bytecode specification language (BCSL) and a weakest precondition calculus for sequential Java bytecode. BCSL and the calculus are expressive enough for verifying non-trivial properties of programs, and cover most of sequential Java bytecode, including exceptions, subroutines, references, object creation and method calls. Our approach does not require that bytecode components are provided with their source code. Nevertheless, we provide a means to compile JML annotations into BCSL annotations by defining a compiler from the Java Modeling Language (JML) to BCSL. Our compiler can be used in combination with most Java compilers to produce extended class files from JML-annotated Java source programs. All components, including the verification condition generator and the compiler are implemented and integrated in the Java Applet Correctness Kit (JACK).

References

1. A. V. Aho, R. Sethi, and J. D. Ullman. Compilers-Principles, Techniques and Tools. Addison-Wesley: Reading, 1986.]]
2. B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2 revised edition, 1997.]]
3. R. Bornat. Proving pointer programs in Hoare Logic. In MPC, pages 102--126, 2000.]]
4. L. Burdy, A. Requet, and J.-L. Lanet. Java applet correctness: A developer-oriented approach. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME 2003: Formal Methods: ISFME, volume 2805 of LNCS, pages 422--439. Springer, 2003.]]
5. A. Courbot, M. Pavlova, G. Grimaud, and J.-J. Vandewalle. A low-footprint java-to-native compilation scheme using formal methods. submitted to Cardis06.]]
6. K. K. Dhara and G. T. Leavens. Forcing behavioral subtyping through specification inheritance. In 18th International Conference on Software Engineering, Berlin, Germany, pages 258--267, 1996.]]
7. G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, and J. Kiniry. JML Reference Manual. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org.]]
8. B. Jacobs, J. Kiniry, and M. Warnier. Java program verification challenges. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, editors, Formal Methods for Components and Objects, volume 2852, Incs, pages 202--219. Springer, Berlin, 2003.]]
9. X. Leroy. Java bytecode verification: an overview. In G. Berry, H. Comon, and A. Finkel, editors, Computer Aided Verification, CAV 2001, volume 2102 of Incs, pages 265--285. Springer-Verlag, 2001.]]
10. T. Lindholm and F. Yellin. Java Virtual Machine Specification. Addison-Wesley Longman Publishing Co., Inc., 1999.]]
11. G. C. Necula and P. Lee. The design and implementation of a certifying compiler. In ACM SIGPLAN'98 Conference on Programming Language Design and Implementation (PLDI), pages 333--344, 17--19 June 1998. Montreal, Canada.]]
12. M. Pavlova. Java bytecode logic and specification. Preliminary version. Available from http://www.inria.fr/everest/Mariela.Pavlova.]]
13. M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. In CARDIS 2004. Springer-Verlag, 2004.]]

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language types

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program specifications

      • Program verification