A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. This tool is a static analyzer for enforcing programming guidelines to Java programs. It takes a Java bytecode program and a programming guideline as inputs, infers the trace information of the program and then verifies if it is accepted by the guideline. If the inferred result is not acceptable, the tool tries to search for an execution path of the program that violates the guideline.
This tool is based on our PPDP'21 paper:
S. Erbatur and U. Schöpp and C. Xu. Type-based enforcement of infinitary trace properties for Java. PPDP 2021, ACM, Article 18, 1–14.
The previous version was developed by Zălinescu et al., based on their APLAS'17 paper.
The new features of the current version include:
- It enhaces the analysis precision by capturing different effects depending on regions.
- Effect annotations are given by the abstract interpretation based on Büchi automata due to Hofmann and Chen.
- It can analyze also nonterminating programs by capturing the information of their infinite traces.
- It supports exception handling, i.e., it can analyze programs with exceptions.
- It tries to report a counterexample when it judges that the program may not adhere to the guideline.
- Java 8
The tool can be built using Gradle. A configuration file "build.gradle" is provided in the repository. For example, in an IDE (e.g. IntelliJ IDEA), one can setup a project for the tool by opening the build.gradle file as a project.
The tool was tested and evaluated with the Securibench Micro benchmark as well as a bunch of additional examples.
The benchmark provides 122 test cases in 12 categories. Each benchmark program implements a small self-contained servlet. Our tool are applied to verify if they adhere to the guideline that only untainted commands can be executed.
The testcases folder contains 19 programs with typical nonterminating behaviors and 10 programs with exception handling for testing the infinitary and exceptional effect analysis. For these programs, a simple policy is employed to test if the tool computes the correct effects.
There are totally 157 test cases (see the Evaluation.java file) and 145 of them run as expected. The tool does not support features such as reflection and concurrency, resulting in 8 failed tests. The remaining 4 failures are due to the limitation of the approach (for example, the analysis is not fully path-sensitivity).
The experiment can be run from the commond-line by typing:
./gradlew build
- Eugen Zălinescu
- Ulrich Schöpp
- Chuangjie Xu
- Jakob Knauer