Roberto Barbuti
ABSTRACT
The Java Virtual Machine embodies a verifier which performs a set of checks on bytecode programs before their execution. The verifier performs a data-flow analysis applied to a type-level abstract interpretation of the code. The current implementations of the bytecode verifier present a significant problem: there are legal Java programs which are correctly compiled into a bytecode that is rejected by the verifier. Also the more powerful verification techniques proposed in several papers suffer from the same problem. In this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the efficiency of current implementations. The enhanced version is based on a domain of types which is more expressive than the one used in standard verification.
- Barbuti, R., Bernardeschi, C., De Francesco, N. and Tesei, L. Enhancing the Java Bytecode Verifier by Abstract Interpretation. Internal Report Dipartimento di Informatica, Università di Pisa, 2002.]]Google Scholar
- Cousot, P. and Cousot, R. Abstract Interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proc. of POPL'77. ACM Press, 238-258, 1977]] Google ScholarDigital Library
- Cousot, P. and Cousot, R. Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics,82(1):43-57, 1979.]]Google ScholarCross Ref
- Freund, S. N. and Mitchell, J. C. A Formal Framework for the Java Bytecode Language and Verifier. ACM Conference on Object-Oriented Programming Systems, Languages & Applications, 1999.]] Google ScholarDigital Library
- Hagiya, M. and Tozawa, A. On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines. Static Analysis Symposium '98, LNCS 1503, Springer, 1998.]]Google ScholarCross Ref
- Leroy, X. Java bytecode verification: an overview. In Proceedings of CAV'01, Springer LNCS 2102, 2001.]] Google ScholarDigital Library
- Lindholm, T. and Yellin, F. The Java Virtual Machine Specification. The Java Series, Addison-Wesley, 1999.]] Google ScholarDigital Library
- Nipkow, T. Verified Bytecode Verifiers. FOSSACS 2001, LNCS 2030, Springer, 2001.]] Google ScholarDigital Library
- O'Callahan, R. A Simple, Comprehensive Type System for Java Bytecode Subroutines. ACM Symposium on Principles of Programming Languages, 1999.]] Google ScholarDigital Library
- Qian, Z. Standard fixpoint iteration for Java bytecode verification. ACM Transactions on Programming Languages and Systems22(4):638-672, 2000.]] Google ScholarDigital Library
- Stärk, R. F. and Schmid, J. The problem of bytecode verification in current implementations of the JVM. Technical Report, Department of Computer Science, ETH Zürich, 2000.]]Google Scholar
- Stata, R. and Abadi, M. A type system for Java bytecode subroutines. ACM Transactions on Programming Languages and Systems,21(1):90-137, 1999.]] Google ScholarDigital Library
Recommendations
A Type System for the Java Bytecode Language and Verifier
The Java Virtual Machine executes bytecode programs that may have been sent from other, possibly untrusted, locations on the network. Since the transmitted code may be written by a malicious party or corrupted during network transmission, the Java ...
Modeling the Java Bytecode Verifier
The Java programming language has been widely described as secure by design. Nevertheless, a number of serious security vulnerabilities have been discovered in Java, particularly in the Bytecode Verifier, a critical component used to verify class ...
A type system for object initialization in the Java bytecode language
In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then executed by the Java Virtual Machine. Since bytecode may be written by hand, or ...
Comments