article · Scholarship at UWindsor (University of Windsor) · 2001
Formalizing Java bytecode verifier using Z.
Cited by 0Open access
Abstract
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. Paper copy at Leddy Library: Theses & Major Papers - Basement, West Bldg. / Call Number: Thesis2001 .G86. Source: Masters Abstracts International, Volume: 40-06, page: 1545. Adviser: Liwu Li. Thesis (M.Sc.)--University of Windsor (Canada), 2001.
Cite this paper
Guo, R. (2001). Formalizing Java bytecode verifier using Z. Scholarship at UWindsor (University of Windsor).
Guo, Rui. “Formalizing Java bytecode verifier using Z.” Scholarship at UWindsor (University of Windsor), 2001.
Guo, Rui. 2001. “Formalizing Java bytecode verifier using Z.” Scholarship at UWindsor (University of Windsor).
Guo, R. (2001) ‘Formalizing Java bytecode verifier using Z’, Scholarship at UWindsor (University of Windsor).
@article{guo2001formalizing,
title = {{Formalizing Java bytecode verifier using Z.}},
author = {Guo, Rui},
journal = {Scholarship at UWindsor (University of Windsor)},
year = {2001}
}Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.