SAW + JVM

[weaversa]

I've tried and tried but cannot figure out what the non-deprecated version of the proof given below could be. I know that to map the input array alloc to a term I have to do something like this:

    let xs = eval_list x;
    for [0,1,2,3]
      (\i -> jvm_elem_is ref i (jvm_term (nth xs i)));

I think the problem I'm having is that the only example of the newish java+crucible verification interface is the ecdsa example, and it's huge. If it's not too much trouble, would someone be willing to modernize the sawscript below? I guess it's also possible that crucible proofs of java programs is just not ready yet?

public class Salsa20 {

    static int rotate(int u, int c) {
        return (u << c) | (u >>> (32 - c));
    }
    
    static int [] quarterround(int [] y) {
        int z[] = new int[4];
        z[1] = y[1] ^ rotate(y[0] + y[3], 7);
        z[2] = y[2] ^ rotate(z[1] + y[0], 9);
        z[3] = y[3] ^ rotate(z[2] + z[1], 13);
        z[0] = y[0] ^ rotate(z[3] + z[2], 18);
        return z;
    }
}

enable_deprecated;

let quarterround_java_setup = do {
  java_allow_alloc;
  y <- java_var "y" (java_array 4 java_int);
  java_return {{ quarterround y }};
  java_verify_tactic z3;
};

m <- java_load_class "Salsa20";
result <- java_verify m "quarterround" [] quarterround_java_setup;

[brianhuffman]

I'll have a go at this. The crucible_jvm stuff definitely needs some more TLC and polish. When I last worked on it, I only had enough time to get the ecdsa proof script working. I have plenty of ideas for improvements to it; it's just a matter of finding the time to work on it more. I'll have to double check with @atomb, but I think we have some time planned for crucible_jvm on our SAW roadmap during the next release cycle after this one (i.e. within a few months).

[brianhuffman]

Here's a working proof script:

enable_experimental;

m <- java_load_class "Salsa20";

let {{
quarterround : [4][32] -> [4][32]
quarterround [y0, y1, y2, y3] = [z0, z1, z2, z3]
  where
    z1 = y1 ^ ((y0 + y3) <<< 7)
    z2 = y2 ^ ((z1 + y0) <<< 9)
    z3 = y3 ^ ((z2 + z1) <<< 13)
    z0 = y0 ^ ((z3 + z2) <<< 18)
}};

result <-
  crucible_jvm_verify m "quarterround" [] false
  do {
    y <- jvm_alloc_array 4 java_int;
    y0 <- jvm_fresh_var "y0" java_int;
    y1 <- jvm_fresh_var "y1" java_int;
    y2 <- jvm_fresh_var "y2" java_int;
    y3 <- jvm_fresh_var "y3" java_int;
    jvm_elem_is y 0 (jvm_term y0);
    jvm_elem_is y 1 (jvm_term y1);
    jvm_elem_is y 2 (jvm_term y2);
    jvm_elem_is y 3 (jvm_term y3);

    jvm_execute_func [y];

    z <- jvm_alloc_array 4 java_int;
    let {{ [z0,z1,z2,z3] = quarterround [y0,y1,y2,y3] }};
    jvm_elem_is z 0 (jvm_term {{ z0 }});
    jvm_elem_is z 1 (jvm_term {{ z1 }});
    jvm_elem_is z 2 (jvm_term {{ z2 }});
    jvm_elem_is z 3 (jvm_term {{ z3 }});
    jvm_return z;
  }
  z3;

I know it's a bit rubbish because of the element-wise treatment of arrays. Issue #422 (points-to declarations for entire arrays) are at the top of my todo list when I get back to working on crucible_jvm stuff again.

[weaversa]

Thanks @brianhuffman !