| Java security is a problem that is raised sharply with its ubiquity through Internet. Sun provides two kinds of specifications of Java bytecode verifier, which is used to ensure the soundness of a program. One is a prose specification and the other is a reference to implementation. Neither of these two way is a good approach to solve the security problems.; This thesis proposes a new way to formalize Java bytecode verifier by using Z language. The formal method is usually a perfect choice to some novel, difficult and critical projects. As a model-based formal specification language, Z is a good language to model a well-structured system. Besides the well-structured way it can offer, Z can also support verification of the implementation based on its specification. This approach offers a formal basis for any operation that is crucial to security. This helps to avoid causing security holes. By giving formal description to each bytecode instruction, the verifier could check the typing correctness within a method at each step of runtime. On the other hand, a more flexible and clearer module is constructed, which is applied to the type checking system, not only for Java but also for other similar mechanism. This thesis focuses on two essential problems: subroutine and object initialization.; Since this thesis gives a core model to deal with the Java bytecode verifier, it is easy to be extended to include all the instructions of Java bytecode. |
