Result: The Functions of Java Bytecode

Java bytecode provides a portable representation for programs that allows executable content to be embedded in web pages, transferred across a network, and executed on a remote user's machine. Features like these provide many new opportunities for developers, but special precautions must be taken to protect users from badly-behaved programs, which might otherwise destroy valuable data or compromise their privacy. To avoid such problems, bytecode programs from untrusted sources must be verified before they are used. If a program passes, then it should be well-behaved, and should not be able to subvert the other security mechanisms of the Java platform. However, if a program fails, then it will be rejected. Clearly, to be sure that it is effective, we need a precise way to understand bytecode verification. This paper describes the main features of a formal specification for Java bytecode that allows us to reason about the correctness of Java implementations, and to guarantee safety prope.