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
