/WhyBack

Primary LanguageJupyter NotebookGNU General Public License v3.0GPL-3.0

WhyBack is a deductive verifier for JVM languages that works at the level of JVM bytecode. It provides an annotation library to specify programs at the source code level in a way that "survives" compilation to bytecode. Then, WhyBack encodes bytecode programs into Why3, which performs the actual verification.

By working on bytecode while supporting specification at the source code level, WhyBack can accommodate a lot of Java features in a uniform way. In fact, it can verify programs written in recent Java versions, and even supports some features of other JVM languages such as Kotlin and Scala.

WhyBack is built on top of ByteBack, which encodes programs in the Boogie IVL for use with the Boogie verifier. This version of ByteBack is also referred to as "BoogieBack".

Installation instructions for WhyBack are the same as the ones for BoogieBack, and they are included below.

Installing ByteBack

Manual setup

Building

Build ByteBack using Gradle:

./gradlew install

This command builds:

Dependencies

As mentioned above, ByteBack encodes bytecode programs into Boogie. To verify ByteBack's Boogie output, you also need to install:

For example, Z3 can be installed through pypi using the ./requirements.txt file, while Boogie can be installed by using the .NET SDK 6:

dotnet tool install -g boogie

Testing your manual setup

ByteBack includes system tests and verification experiments. A separate file describes how to run them.

Using ByteBack

An example of usage

Let's see how to use byteback-cli to verify the Java program Main.java in ./example.

Main.java contains a single method positive_sum with pre- and postcondition:

@Predicate
public boolean positive_arguments(int a, int b) {
    return gte(a, 0) & gte(b, 0);
}

@Predicate
public boolean positive_return(int a, int b, int returns) {
    return gte(returns, 0);
}

@Require("positive_arguments")   // a >= 0 && b >= 0
@Ensure("positive_return")       // returns >= 0
public int positive_sum(int a, int b) {
    return a + b;
}

To verify this simple program, go to directory ./example and follow these steps:

  1. Compile Main.java, including the BBlib .jar in the classpath:
javac Main.java -cp ../byteback-annotations/build/libs/byteback-annotations.jar

This generates bytecode for class Main.

  1. Run ByteBack using byteback-cli on the generated bytecode:
# The PATH to byteback-cli is already set in the Docker image
export PATH="$PATH:../byteback-cli/build/install/byteback-cli/bin/"

byteback-cli \
	-cp ../byteback-annotations/build/libs/byteback-annotations.jar \
	-cp . \
	-c Main \
	-o Main.bpl

This generates a Boogie program Main.bpl, which encodes the Java program's semantics and its specification in Boogie.

  1. Finally, verify the generated Boogie program using the Boogie verifier:
boogie Main.bpl

This should return with a successful verification:

Boogie program verifier finished with 2 verified, 0 errors

Command line options

byteback-cli is the command line tool that runs ByteBack. It inputs Java bytecode and outputs Boogie programs. byteback-cli supports the following options:

byteback-cli \
	  -cp CLASS_PATH \
	  -c TARGET_CLASS \
	[ -o BOOGIE_OUTPUT ] \
	[ -p PRELUDE ]\
	[ --npe ] \
	[ --iobe ]

  • -cp CLASS_PATH declares the classpath where ByteBack will look for bytecode to be analyzed. You can repeat this option to specify multiple classpaths.

  • -c TARGET_CLASS give the fully qualified name of an entry class for ByteBack's analysis. You can repeat this option to declare multiple entry classes. ByteBack will recursively process all application classes that are referenced from any entry class (excluding standard library classes).

  • -o BOOGIE_OUTPUT declares the name of the output Boogie file generated by ByteBack. If this option is omitted, ByteBack prints the Boogie program to standard output.

  • -p PRELUDE specifies the Boogie prelude files to be used. If this option is omitted, ByteBack uses its standard prelude.

  • --npe enables support for verifying behavior of implicit NullPointer exceptions.

  • --iobe enables support for verifying behavior of implicit IndexOutOfBounds exceptions.

ByteBack annotations

BBLib, the ByteBack annotations library, includes annotations and static methods for specifying functional properties at the level of Java source code, or any other language that compiles to JVM bytecode.

See the annotated programs in ./byteback-test for examples of using BBLib.

Citing ByteBack

To cite ByteBack refer to the paper:

Marco Paganoni and Carlo A. Furia. Verifying Functional Correctness Properties At the Level of Java Bytecode. In Proceedings of the 25th International Symposium on Formal Methods (FM). Lecture Notes in Computer Science, 14000:343–363, Springer, March 2023.

@InProceedings{PF-FM23-ByteBack,
  author = {Marco Paganoni and Carlo A. Furia},
  title = {Verifying Functional Correctness Properties At the Level of {J}ava Bytecode},
  booktitle = {Proceedings of the 25th International Symposium on Formal Methods (FM)},
  year = {2023},
  series = {Lecture Notes in Computer Science},
  pages = {343--363},
  volume = {14000},
  publisher = {Springer}
}

Another publication describing the research behind ByteBack:

Marco Paganoni and Carlo A. Furia. Reasoning About Exceptional Behavior At the Level of Java Bytecode. In Proceedings of the 18th International Conference on integrated Formal Methods (iFM). Lecture Notes in Computer Science, 14300:113–133, Springer, November 2023.

@InProceedings{PF-iFM23-ByteBack,
  author = {Marco Paganoni and Carlo A. Furia},
  title = {Reasoning About Exceptional Behavior At the Level of {J}ava Bytecode},
  booktitle = {Proceedings of the 18th International Conference on integrated Formal Methods (iFM)},
  year = {2023},
  series = {Lecture Notes in Computer Science},
  pages = {113--133},
  volume = {14300},
  publisher = {Springer},
}