Using OpenJDK for static analysis

[Florian Weimer]

On 02/11/2014 01:11 AM, Pascal Kesseli wrote:
> 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.

jdk7u-dev isn't the right mailing list for this question.  The discuss 
list might be better (and I'm redirecting it there), but officially, I 
think such questions should be posted to the forums (which I don't 
frequent).

> 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?

There are exceptions, like methods that won't work properly when not 
intrinsified.

>   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?

There was a proposal to write to documentation: 
<http://mail.openjdk.java.net/pipermail/cvmi-dev/2012-December/000068.html> 
But I don't think this was ever turned into a real JEP, and I haven't 
seen the documentation.

-- 
Florian Weimer / Red Hat Product Security Team