AW: Using OpenJDK for static analysis

[Pascal Kesseli]

Hi Florian,

Thanks for the heads up. I'll be sure to take a look at the forum as well.
Technically speaking, we won't actually execute any Java code at all, so as
long as there is a JNI implementation with the correct semantics somewhere
in the code for every native method, we can use that for our analysis.

Whether or not that method is actually called at runtime or optimised away
through intrinsic methods should not make a difference with regard to the
semantics of the program, right?

Thanks,
Pascal


-----Ursprüngliche Nachricht-----
Von: Florian Weimer [mailto:fweimer at redhat.com] 
Gesendet: 11 February 2014 12:59
An: Pascal Kesseli
Cc: jdk7u-dev at openjdk.java.net; discuss at openjdk.java.net
Betreff: Re: Using OpenJDK for static analysis

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