Font Size: a A A

Formalizing Type Safety Of The Java Virtual Machine

Posted on:2006-10-30Degree:DoctorType:Dissertation
Country:ChinaCandidate:T J ZuoFull Text:PDF
GTID:1118360182960106Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
This thesis deals with machine-checking the security of the Java Virtual Machine (JVM). We present a fully formal, machine-checked specification of the bytecode verification and dynamic class loading, which are important parts in Java's security architecture. Precisely, we define a subset of Java virtual machine language (JVML), present a type system and an operational semantics for the subset, and prove the soundness of the type system with respect to the operational semantics. Therefore, our type system guarantees that a well-typed program cannot cause type errors. All definitions and proofs have been done fully formally with the interactive theorem prover HOL 4, representing one of its major applications. This approach guarantees not only rigorous definitions, but also gives maximal confidence in the results obtained. We also discuss an implementation and an extension of HOL 4.In the formalization of bytecode verification, we present formal models, in three stages, for object initialization, subroutine, and lock primitives, which are difficult static analysis problems. In the first stage, we define a small subset of JVML, called JVMLO. We proves that the constraints, imposed by the JVM specification on alias analysis, are too strong. Thus, there exist lots of unnecessary type check in Sun's bytecode verifier. The type system of JVMLO ensures that every object is initialized before it is used.In the second stage, we extend JVMLO to JVML1, which includes bytecode instructions of subroutine. We introduce a subroutine record in the type system, which is used to record called subroutines and modified local variables. We define a partial order on subroutine records, which means subroutines cannot be called recursively in bytecode programs. This choice conforms to the Java virtual machine specification. In fact, we argue that the special feature, which subroutines may be called recursively, is desirable or not. Our type system deviates from Sun's specification in a few aspects. For example, we formalize a simpler, equally effective restriction for alias analysis. Our rules can accept more correct bytecode programs than Sun's rules. Sun's rules forbid aload x instruction when x is uninitialized, while our rules has no such restriction. Sun's rules allow only one ret instruction per subroutine, while our rules allow an arbitrary number. Although weaker than Sun's rules, our rules do not compromise soundness. The soundness theorem of the type system guarantees that (1) subroutines can return correctly based on the call stack;(2) alias analysis is correct in the presence of subroutines.In the third stage, we define JVML2 by introducing lock primitives into JVML1. The type system of JVML2 is an extension to Sun's verifier because the present implementation does not check the correct usage of lock primitives. By introducing new types and a list to record locked object types, we construct a sound type system of JVML2, which is an extension of the type system of JVML1. A well-typed JVML2 program can guarantee structured locking property, which means (1) the numbers of locks and unlocks performed on an object must be equal, whether the method invocation completes normally or abruptly;(2) at no point during a method invocation, the number of unlocks may exceed the number of locks performed on an object.Class loaders play important roles in Java's dynamic class loading, which not only improves programming flexibility but also provide separate namespaces for different software components. However, early versions (1.0 and 1.1) of the JDK contained a flaw, called Saraswat's type spoofing, in class loader implementation. Since JDK 1.2, a loading constraint scheme is introduced to fix the problem. We not only include the scheme in our fonnalization but also show that there exist other forms of type spoofing in JDK 1.2 and 1.3. We thus propose a subtyping constraint scheme to fix the new problem. The main idea of the scheme is introducing a set, which is used to keep merged types during bytecode verification, into the type system. We then define subtyping constraints based on the set. To prove the soundness of the type system, we propose a new approach to assign types to values. We also formalize the JVM classfile structure and define operation on it. Thus, our formal specification is more closed to Sun's specification. Through rigorous fonnalization and soundness proof, we also analyze the subtle relations between bytecode verification and class loading.In general, the thesis (1) provides a full, rigorous and sound formal specification for the JVM;(2) provides a unified and formal framework for the investigation of other features of the JVM;(3) provides a rational and sound reconstruction of Sun's verifier;(4) gives a better understanding of the JVM through formal analysis;(5) proves the feasibility of formalizing real programming languages in HOL system.
Keywords/Search Tags:type security, bytecode verification, dynamic class loading, type system, operational semantics, theorem proving, the HOL system
PDF Full Text Request
Related items