article · 2003

A Type System for the Java Bytecode Language and Verifier

Stephen N. Freund, John C. Mitchell

Cited by 0Abstract and details only

Abstract

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 Virtual Machine contains a bytecode verifier to check the code for type errors before it is run. As illustrated by reported attacks on Java run-time systems, the verifier is essential for system security. However, no formal specification of the bytecode verifier exists in the Java Virtual Machine Specification published by Sun. In this paper, we develop such a specification in the form of a type system for a subset of the bytecode language. The subset includes classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. We also present a type checking algorithm and prototype bytecode verifier implementation, and we conclude by discussing other applications of this work. For example, we show how to extend our formal system to check other program properties, such as the correct use of object locks.

Cite this paper

APA 7

Freund, S. N., & Mitchell, J. C. (2003). A Type System for the Java Bytecode Language and Verifier.

MLA 9

Freund, Stephen N., and John C. Mitchell. “A Type System for the Java Bytecode Language and Verifier.” 2003.

Chicago

Freund, Stephen N., and John C. Mitchell. 2003. “A Type System for the Java Bytecode Language and Verifier.”

Harvard

Freund, S.N. and Mitchell, J.C. (2003) ‘A Type System for the Java Bytecode Language and Verifier’.

BibTeX

@article{freund2003type,
  title = {{A Type System for the Java Bytecode Language and Verifier}},
  author = {Freund, Stephen N. and Mitchell, John C.},
  year = {2003}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.