[Prev][Next][Index][Thread]
Paper available on Java bytecode verification
I would like to announce the availability of the following paper:
Constraint-Based Specification and
Dataflow Analysis for Java Bytecode Verification
Abstract
Java bytecode verification should prevent various runtime errors in
Java Virtual Machine (JVM) programs and play an important part in
ensuring Java-based internet security. The official JVM specification
is inadequate for security-critical applications. Recent research
work has proposed using formal typing systems to specify bytecode
verification. However, it is still unknown how to make an
implementation, whose correctness and completeness with respect to the
formal specification can be proved.
This paper proposes an approach to bridging the gap. We first give
formal typing rules enforcing formal constraints on types for memory
locations in simplified legal JVM programs. Then we present a dataflow
analysis algorithm (scheme) as a bytecode verifier, which
non-deterministically uses the formal rules to compute the smallest
types for memory locations that satisfy the constraints, or to report
a failure if the computation fails. By formally proving the
correctness, termination and completeness of the algorithm, we show a
way to reach a bytecode verifier, which is provably correct with
respect to a formal specification.
This paper is available under
http://www.kestrel.edu/~qian/abs-jvmdflow.html
Comments are welcome.
Zhenyu Qian