A symbolic Java virtual machine for program analysis, verification and test generation.
JBSE is the Java Bytecode Symbolic Executor. Basically, it is a special-purpose Java Virtual Machine written in Java.
JBSE is not a replacement of Hotspot, and is not meant to be used to run Java code in production. Rather, JBSE is meant to be used to exhaustively analyze how a piece of Java software behaves when fed with a possibly infinite set of inputs, mainly to assess whether the software under analysis has bugs or not. This makes it similar in aim to tools like Checkstyle, PMD or Spotbugs, but the analogy ends here. While the above mentioned tools work by scanning the source code in search for a predefined set of code patterns, JBSE simulates the execution of the compiled classfiles (that’s why it is a Java Virtual Machine). JBSE expects that you specify the verification properties of interest for your project as a set of assumptions and assertions. Assumptions specify the conditions that must be satisfied for an execution to be relevant for the analysis. Assertions specify the conditions that must satisfied for an execution to be correct. JBSE attempts to determine whether some inputs exist that satisfy all the assumptions and make fail at least one assertion. In this regard JBSE is more similar in spirit, implementation and mode of use to tools like Symbolic PathFinder, Sireum/Kiasan and JNuke. It can be used both as a standalone textual tool and as a library.
Specifying good verification properties is not always easy, especially when inputs are made of complex object configurations as customarily happen with object-oriented and heap-manipulating programs. To make the task simpler JBSE offers a comprehensive array of techniques and languages for expressing assumptions and assertions. None of the tools we are currently aware of offers all of them. This allows JBSE to execute and analyze a wide spectrum of Java programs, including programs that manipulate arrays.
Another distinctive feature of JBSE is its speed. According to our microbenchmarks it is among the fastest symbolic executors for Java bytecode, capable of analyzing the Siemens suite tcas program in about 5 seconds. All the standard caveats about the (scarce) generality of micro benchmarks apply, but we have not yet encountered a case study where JBSE is meaningfully slower than other approaches.
Determining whether a control-flow path in the program can be covered by some inputs is an intrinsically hard problem, much harder than scanning the source code for bug patterns. JBSE works by calculating, for all the paths in the program it explores, the associated path conditions, where a path condition is a formula on the program input variables whose solutions, if they exist, are the inputs that cover the path. JBSE checks whether the path conditions have solutions by invoking an external solver. Currently JBSE can interact with the SMT solvers Z3 and CVC4. The correctness, completeness and speed of JBSE strongly depend on those of the solver it relies upon.
JBSE also has limitations on its own. JBSE aims to implement as faithfully as possible the Java Virtual Machine specification v.8, but we are not there yet. Currently JBSE has a quite comprehensive implementation of most part of the specification, including invokedynamic, lambdas, method handles and default methods. JBSE does not really implement multithreading and synchronization: You can dynamically create threads other than the initial one, but JBSE will not schedule them - in other words, JBSE is single-threaded. Also lacking are many native methods in the JRE standard library, mostly related to reflection and security. Some of these limitations stem from the sheer amount of work that is necessary to do for implementing the desired features, some stem from the fact that doing a symbolic analysis of a full-featured Java program is too hard computationally.
A user and developer manual is in progress at this ReadTheDocs link but it is far from being complete. In the meantime you can integrate the manual with the README.md file and the examples project for learning how to use JBSE. You can also have a look at the publications section on the homepage of Pietro Braione for an overview of the JBSE techniques and internals.
The contributions to JBSE extend over a very long period. The current maintainer of JBSE is Pietro Braione (@pietrobraione), with help from Giovanni Denaro, who also contributed the rewriting engine. Marco Gaboardi wrote the initial implementation of JBSE. Diego Piazza contributed to the development of the SMTLIB2 interface. Esther Turati worked on the JUnit test suite generator. Last but not least, Andrea Mattavelli restructured the project to be built with Maven, and Andrea Aquino contributed patches to existing code.
If you find JBSE useful and you want to cite it in your publication you can refer these papers:
P. Braione, G. Denaro, M. Pezzè. Symbolic execution of programs with heap inputs. In Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2015), pp 602-613. doi:10.1145/2786805.2786842.
P. Braione, G. Denaro, M. Pezzè. Enhancing Symbolic Execution with Built-In Term Rewriting and Constrained Lazy Initialization. In Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2013), pp 411-421. doi:10.1145/2491411.2491433.
Of course we invite you to star the project on Github. We also invite you to give a look at TARDIS and SUSHI, our automatic test generators for Java programs based on JBSE and EvoSuite.
JBSE is a research prototype offered as-is, and we disclaim any expressed or implied warranty on its correctness, quality, or even fitness for a particular purpose. In no event shall its authors and the organization they belong to be considered liable for any direct or consequent damage that may derive from its use, for any definition of liability. See the license for more information.
For any issue contact Pietro Braione at name.surname@unimib.it or open an issue here.