KTH Demo: Proof Generation
This is the first (and only) step of producer-side tool. It verifies that the proof generated by the producer is valid.
Tool output:
Manipulated Code
This section shows what happens in the verification if the code (but not the annotations) in the final jar file is modified before loaded onto the phone.
Code Modifications
The code is modified in the following way: The target label of the conditional branch that possibly jumps to the termination code is changed. The new target label is the label of the instruction below the conditional branch. This change will cause the program to always skip termination and thus in some executions violate the policy.
The change is shown below.
Original code
...
class s3mstest.wormgame.ScoreSender extends java.lang.Thread {
...
public void run();
Code:
...
42: getstatic #61;
45: iconst_0
46: if_icmpne 56 // Jump to to termination code?
49: iconst_1
50: putstatic #61;
53: goto 74 // Skip termination
56: getstatic #64;
59: dup
60: ldc #66;
62: invokevirtual #55;
65: ldc #68;
67: invokevirtual #55;
70: iconst_m1
71: invokestatic #72; //exit
74: aload_3
75: invokestatic #78; //openDataOutputStream
...
}
Modified code
...
class s3mstest.wormgame.ScoreSender extends java.lang.Thread {
...
public void run();
Code:
...
42: getstatic #61;
45: iconst_0
46: if_icmpne 49 // MODIFICATION: don't jump
49: iconst_1
50: putstatic #61;
53: goto 74 // Skip termination
56: getstatic #64;
59: dup
60: ldc #66;
62: invokevirtual #55;
65: ldc #68;
67: invokevirtual #55;
70: iconst_m1
71: invokestatic #72; //exit
74: aload_3
75: invokestatic #78; //openDataOutputStream
...
}
The verification step
The result of the verification now looks like this:
