JBMC: Bounded Model Checking for Java Bytecode
- 3.9k Downloads
JBMC is a bounded model checking tool for verifying Java bytecode. It is built on top of the CPROVER framework. JBMC processes Java bytecode together with a model of the standard Java libraries. It checks a set of desired properties, such as assertions and absence of uncaught exceptions, under given bounds on loops, recursion and data structures. Internally, it uses the same bounded model checking engine as its sibling tool CBMC and discharges the generated verification conditions with the help of MiniSAT 2.2.1.
JBMC is a bounded model checker based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), which allows the verification of Java programs . JBMC inherits memory model, symbolic execution engine and SAT/SMT backends of its sibling tool CBMC . In particular, JBMC consists of a frontend for parsing Java bytecode and a Java operational model (JOM), which is an exact but verification-friendly model of the standard Java libraries. Thus, JBMC supports Java bytecode and can verify programs that make use of classes, inheritance, polymorphism, arrays, bit-level operations and floating-point arithmetic using CBMC’s verification engine.
JBMC can reason about array bound violations, unintended arithmetic overflows, and other kinds of functional and runtime errors. However, as with other bounded model checkers, JBMC is in general incomplete, i.e., can only be used to find property violations up to a given bound k but not to prove properties, unless we know an upper bound on the depth of the state space by checking whether all loops have been fully unrolled; this is accomplished by inserting a so-called unwinding assertion at the end of each loop and recursion to check for termination.
JBMC natively supports MiniSAT as its main solver to discharge verification conditions (VCs) and check for their satisfiability, but can also be used with other incremental SAT solvers such as Glucose. For SV-COMP 2019, however, JBMC does not use incremental bounded model checking to verify Java programs with (multiple) loops, i.e., it does not check the VCs in iteration \(k + 1\) by building upon the work done for iteration k .
The GOTO Symex component performs a symbolic execution of the program, which thus handles dynamic memory allocation, encoding of virtual method dispatch, unrolling of the loops and unfolding of recursive method calls. In particular, JBMC uses two functions that compute the constraints C (i.e., assumptions and variable assignments) and properties P (i.e., built-in and user-defined assertions); it automatically generates safety conditions that check for null dereference, array bounds errors, type cast errors and other kinds of functional and runtime errors. Both functions accumulate the control-flow predicates at each program point and use these predicates to guard both the constraints and the properties, so that they properly reflect the Java bytecode’s semantics. JBMC’s VC generator then derives the VCs from these; the resulting bit-vector formula (i.e., \(C \wedge \lnot P\)) is then passed on to the configured SAT solver to check for satisfiability. If this formula is satisfiable, then JBMC produces a counterexample; otherwise, if the formula is unsatisfiable, then a successful verification result is reported.
JBMC uses an abstract representation of the standard Java libraries, called the Java operational model (JOM), which consists of simplified models of the most common classes from java.lang and a few from java.util; these models remove verification-irrelevant performance optimizations (e.g., in the implementation of container classes), exploit declarative specifications (using assume statement) and functions that are built into the CPROVER framework (e.g., for array and string manipulation).
JBMC also implements a solver for strings to determine the satisfiability of a set of constraints involving strings . Specifically, our string solver implements a decision procedure for string operations that are typically used by Java programs, such as concatenation, search, extract and conversions to other data types. This decision procedure uses incremental SAT solving to lazily instantiate quantifiers.
JBMC also provides API classes that allow users to define non-deterministic verification harnesses and stub functions as used in the SV-COMP benchmarks. The API1 contains such methods for primitive data-types (e.g. nondetDouble()) and strings (e.g. nondetString()). The API also provides an Open image in new window method, which advises JBMC to ignore paths that do not satisfy a user-specified condition. JBMC is able to check for array bounds, division by zero, unintended arithmetic overflows, runtime errors in Java (e.g. illegal memory access) and user-specified assertions.
Current development efforts include improving support for regular expressions, multi-threaded programs and enabling output of VCs using the SMT-LIB format to be checked by SMT solvers such as Z3, CVC4, Boolector, MathSAT and Yices.
4 Strengths and Weaknesses
JBMC does not produce any incorrect result for any of the Java verification tasks available in SV-COMP 2019 ; it correctly claims 139 benchmarks correct and finds existing errors in 192. However, JBMC crashes (and returns unknown) in 37 benchmarks due to time or memory exhaustion, or due to missing models of the Java standard library. JBMC can handle most Java basic features (e.g., inheritance, polymorphism and exceptions) and strings manipulations (but regexes are not fully supported yet). However, JBMC’s concurrency support is still limited and there is no support for Java 8 lambdas, reflection and Java Native Interface (JNI). As its sibling CBMC, JBMC can only prove bounded programs unless an upper bound is known on the depth of the state space, which is not generally the case. Lastly, our JOM does not cover the entire Java standard library.
5 Tool Setup
where assert.prp indicates the specification to be verified for StringValueOf08. Note that this program invokes in line 4 a non-deterministic method (Verifier.nondetString();) to produce an arbitrary string value; this method is provided by SV-COMP in org.sosy_lab.sv_benchmarks.Verifier. The JOM (core-models.jar) is also part of the submission archive. If a verification task uses a Java library method that is not part of the JOM then the wrapper script returns unknown. The Benchexec tool info module is called jbmc.py and the benchmark definition file jbmc.xml. The competition submission of JBMC uses MiniSAT 2.2.1 as SAT backend. JBMC competes in the Java category.
6 Software Project
JBMC is maintained by Peter Schrammel together with numerous contributors4 from the community. It is publicly available under a BSD-style license. The source code is available at http://www.github.com/diffblue/cbmc in the jbmc directory. Instructions for building JBMC from source are given in the file COMPILING.md.
Executable available at https://gitlab.com/sosy-lab/sv-comp/archives/tags/svcomp19.
Can be built from https://github.com/diffblue/cprover-sv-comp/tree/svcomp19.
- 1.Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 133–155. Springer, Cham (2019)Google Scholar
- 3.Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., Trtik, M.: JBMC: a bounded model checking tool for verifying Java bytecode. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 183–190. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_10CrossRefGoogle Scholar
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.