Kimera Bytecode Verification


We have built a clean-room implementation of a robust and secure verifier as part of our security architecture. We have empirically demonstrated that our implementation is safer than the current state of the art commercial verifiers.

There are numerous advantages to our approach to separate verification in the Kimera firewall. Namely,

The small size and clean structure of our verifier enables us to have a clear mapping between the Java virtual machine (JVM) specification and the Java safety axioms implemented in our verifier. Whereas typical commercial implementations of integrated Java virtual machines may distribute security checks thoughout the verification, compilation, interpretation and runtime stages, our verifier performs complete bytecode verification in a single component. Further, the implementation is annotated with safety axioms that we have distilled from the Java virtual machine specification. Hence, it is possible to easily check the verifier for correctness. We believe that our verifier embodies the most complete set of safety axioms about Java bytecode.

The implementation of our verifier facilitates code coverage testing. It is trivial to figure out the set of axioms that have not been tested by a given test suite, which can be used to guide the development and construction of test cases. The fine grain nature of the axioms further simplifies this task.

The actual implementation of our verifier closely follows the Java virtual machine specification. Four passes are performed during verification. The first pass verifies that the class file is consistent and that its structures are sound. The second pass determines the instruction boundaries of the bytecode and verifies that all branches are safe. The third and most complicated pass involves data flow analysis and verifies that the operands in the Java virtual machine are used in accordance with their types. The first three passes together ensure that the submitted class file does not perform any unsafe operations in isolation. The final and fourth pass ensures that the combination of the submitted class with the rest of the Java virtual machine does not break any global typesafety or interface restrictions.

Kimera verification service is accessible from the web. You can run the verifier on a class you would like to examine by providing a URL to the class (the default is a simple hello world applet that passes verification, you can also try badapplet.class for a non-typesafe applet that fails verification). The verifier that you are about to run does not perform phase four link checks. The submitted class files are logged.


Emin Gün Sirer

Project Kimera
Department of Computer Science and Engineering
© 1997, University of Washington