Compositional Proofs

The examples shown so far treat programs as monolithic entities. A Java method or C function, along with all of its callees, is translated into a single mathematical model. SAWScript also has support for more compositional proofs, as well as proofs about functions that use heap data structures.

Compositional Imperative Proofs

As a simple example of compositional reasoning on imperative programs, consider the following Java code.

class Add {
    public static int add(int x, int y) {
        return x + y;
    }

    public static int dbl(int x) {
        return add(x, x);
    }
}

Here, the add function computes the sum of its arguments. The dbl function then calls add to double its argument. While it would be easy to prove that dbl doubles its argument by following the call to add, it’s also possible in SAWScript to prove something about add first, and then use the results of that proof in the proof of dbl, as in the following SAWScript code (java_add.saw on GitHub).

let add_spec = do {
    x <- jvm_fresh_var "x" java_int;
    y <- jvm_fresh_var "y" java_int;
    jvm_execute_func [jvm_term x, jvm_term y];
    jvm_return (jvm_term {{ x + y }});
};

let dbl_spec = do {
    x <- jvm_fresh_var "x" java_int;
    jvm_execute_func [jvm_term x];
    jvm_return (jvm_term {{ x + x }});
};

cls <- java_load_class "Add";
ms <- jvm_verify cls "add" [] false add_spec abc;
ms' <- jvm_verify cls "dbl" [ms] false dbl_spec abc;
print "Done.";

This can be run as follows:

$ saw -b <path to directory where Java lives> java_add.saw

In this example, the definitions of add_spec and dbl_spec provide extra information about how to configure the symbolic simulator when analyzing Java code. In this case, the setup blocks provide explicit descriptions of the implicit configuration used by jvm_extract (used in the earlier Java FFS example and in the next section). The jvm_fresh_var commands instruct the simulator to create fresh symbolic inputs to correspond to the Java variables x and y. Then, the jvm_return commands indicate the expected return value of the each method, in terms of existing models (which can be written inline). Because Java methods can operate on references, as well, which do not exist in Cryptol, Cryptol expressions must be translated to JVM values with jvm_term.

To make use of these setup blocks, the jvm_verify command analyzes the method corresponding to the class and method name provided, using the setup block passed in as a parameter. It then returns an object that describes the proof it has just performed. This object can be passed into later instances of jvm_verify to indicate that calls to the analyzed method do not need to be followed, and the previous proof about that method can be used instead of re-analyzing it.