A type system for the Java bytecode language and verifier

作     者：Freund, SN Mitchell, JC 

作者机构：Williams Coll Williamstown MA 01267 USA Stanford Univ Stanford CA 94305 USA 

出 版 物：《JOURNAL OF AUTOMATED REASONING》 (自动推理杂志)

年 卷 期：2003年第30卷第3-4期

页      面：271-321页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Java Virtual Machine bytecode verification type systems 

摘      要：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.