Automatic JVM Safety Verification Using wunderhorn

wunderhorn is a tool that takes a program P and a safety property Q and attempts to determine if P satisfies Q. A program can be any program represented as Java source or a JVM bytecode classfile. A safety property is an assertion. If each run of a program P that reaches an assertion Q satisfies the condition of Q, then P satisfies Q.

Verifying freedom from language-level errors

wunderhorn automatically attempts to verify that a given program cannot throw one of several exceptions that is typically a result of an error, such as:

• Accessing an array out of bounds

• Attempting to divide by 0

For example, consider the following implementation of a function that, given integers m and n, computes the Least Common Multiple (LCM) of m and n:

public class LCM {
  static int gcd(int a, int b) {
    int t;
    while (b != 0) {
      t = a % b;
      a = b;
      b = t;
    }
    return a;
  }

  static int lcm(int a, int b) {
    return a / gcd(a, b) * b;
  }

  public static void main(String[] args) {
    int x = Wunderhorn.arby_int();
    int y = Wunderhorn.arby_int();
    lcm(x, y);
  }
}

This implementation is not safe: if it is given input m = n = 0, it will attempt to divide a number by 0, and throw an exception.

When wunderhorn is given the above implementation, it reports that that program is not safe:

$ wunderhorn LCM.java
Division by 0 possible at LCM.lcm line 13.

Verifying satisfaction of custom static assertions

wunderhorn allows users to express application-specific properties as assertions that that are verified statically. Consider the following implementation of the Fibonacci function, annotated with an assertion that specifies that the function fib should always return a non-negative value:

public class Fib {
  public static int fib(int n) {
    if (n <= 0) return 0;
    if (n == 1) return 1;
    return fib(n-1) + fib(n-2);
  }

  public static void main(String[] args) {
    int x = Wunderhorn.arby_int();
    Wunderhorn.ensure(fib(x) >= 0);
  }
}

wunderhorn reports that Fib satisfies its assertion:

$ wunderhorn Fib.java
Safe!

Building wunderhorn

To build wunderhorn, download a copy and make it:

$ git clone https://github.com/gt-wunderhorn/gt-wunderhorn
$ cd gt-wunderhorn
$ sudo make configure
$ make
$ sudo make install
Safe!

Using wunderhorn

To use wunderhorn, run it on a Java source or JVM bytecode class that contains a main method, and is optionally annotated with assertions. Here is a shell session for running wunderhorn on one of its included examples, Fib.java given above:

$ cd example
$ wunderhorn Fib.java
Safe!

Implementation

wunderhorn is implemented in OCaml OCaml. It uses several existing frameworks for performing program-analysis tasks. In particular, it uses:

• Sawja, which translats a given JVM bytecode class to a stackless low-level intermediate representation.

• Z3, which attempts to solve a given CHC system that formulates verifying program safety. In particular, it uses the Duality solver implemented within Z3.

Developers