Proofing : an efficient and safe alternative to mobile-code verification

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