Using OpenJDK for static analysis

[Pascal Kesseli]

Hi everyone,

We are developing a bounded model checker for C/C++ called CBMC here at the
University of Oxford. We're currently evaluating different options to
implement a Java frontend for the program, allowing us to statically verify
Java code as well.

There's obviously a whole series of problems to be tackled before this is
possible, one of which is the following: In order to provide a reasonable
scope, the verifier needs to know the semantics of native JRE library code.
One way of allowing us to do so is for our program to model JNI and use
OpenJDK's C/C++ implementations to determine the semantics of such a method
call in Java.

This approach begs the following questions:
 1.) Are all native runtime library operations in OpenJDK implemented in
proper JNI or are there exceptions and caveats to this approach?
 2.) Are the implementations of these functions reasonably detached from
each other and the rest of the VM, such that they can be analysed in
isolation?

Thanks for a quick heads-up on this and best,
Pascal