The safety of the Java Virtual Machine is founded on bytecode verification. Although verification complexity appears to roughly correlate with program size in. the average case, its worst-case behavior is quadratic. This can be exploited for denial-of-service attacks using relatively short programs (applets or agents) specifically crafted to keep the receiving virtual machine's verifier busy for an inordinate amount of time. Instead of the existing, quadratic-complexity verification algorithm, which needs to decide the validity of any given bytecode program, we present a linear-complexity alternative that merely ensures that no unsafe program is ever passed on to the virtual machine. Hence, in certain cases, our algorithm will modify an unsafe bytecode program to make it safe, a process that we call 'proofing". Proofing does not change the semantics of programs that would have passed the original bytecode verifier. For programs that would have failed verification, our algorithm will, in linear time, either reject them, or transform them into programs (of unspecified semantics) that are guaranteed to be safe. Our method also solves a long-standing problem, in which for certain perfectly legal Java source programs the bytecodes produced by Java compilers are erroneously rejected by existing verifiers.

Java Bytecode Verification was so far mostly approached from a correctness perspective. Security vulnerabilities have been found repeatedly and were corrected shortly thereafter. However, correctness is not the only potential point of failure in the verifier idea. In this paper we construct Java code, which is correct, but requires an excessive amount of time to prove safety. In contrast to previous flaws in the bytecode verifier, the enabling property for this exploit lies in the verification algorithm itself and not in the implementation and is thus not easily fixable. We explain how this architectural weakness could be exploited for denial-of-service attacks on JVM-based services and devices.

Java bytecode is commonly verified prior to execution. The standard verifier is designed as a black-box component that either accepts or rejects its input. Internally, it uses an iterative data-flow analysis to trace definitions of values to their uses to ensure type safety. The results of the data-flow analysis are discarded once that verification has completed. In many JVMs, this leads to a duplication of work, since definition-use chains will be computed all over again during just-in-time compilation. We introduce a novel bytecode verification algorithm that verifies bytecode via Static Single Assignemnt (SSA) form construction. The resulting SSA representation can immediately be used for optimization and code generation. Our prototype implementation takes less time to transform bytecode into SSA form and verify it than it takes Sun's verifier to merely confirm the validity of Java bytecode, with the added benefit that SSA is available "for free" to later compilation stages.

One of Java's most fundamental core concepts is dynamic class loading. While being very practical in the general purpose domain, the runtime cost of dynamic class loading poses a significant challenge for the deployment of Java applications in embedded systems. In this paper we describe a mechanism called static class loading which allows to perform the resource-intensive class loading process at compile-time while preserving the full class-loading semantics as defined in the Java specification. This eliminates the need for a byte-code interpreter and allows to translate all Java code to native code ahead-of-time, saving valuable resources on the target platform.