The model should check the following constraints when an array load instruction is encountered:

- the stack depth is at least 2,
- the stack must contain an array ref and an integer index.

For the purposes of this project it can be assumed that the array is 1-dimensional with a statically assigned length. Time permitting, the model should be extended such that it also type checks the array reference type against the load instruction being executed, e.g. if the instruction is caload, the reference is to a char array.

Test the model as follows. Write a simple Java method that performs an array load, compile it, and apply the Alloy analyzer to the resulting model of the JVM bytecodes for that method. Verify that all constraints are satisfied (no counterexamples). Then, construct two malicious methods that will violate each constraint. Apply the Alloy analyzer and verify that constraint violations occur. (The malicious methods may be constructed using a bytecode construction library such as BCEL, a JVM assembler such as Jasmin, or a binary editor.)

The model should check the following constraints when a return instruction is encountered:

- the stack depth is at least 1,
- the stack must contain an item whose type matches the instruction.

Thus, for the second constraint, it must be the case that areturn pops a reference, dreturn pops a double, and so forth.

Test the model as follows. Write a simple set of Java methods that return different data types, compile them, and apply the Alloy analyzer to the resulting model of the JVM bytecodes for those methods. Verify that all constraints are satisfied (no counterexamples). Then, construct two malicious methods that will violate each constraint. Apply the Alloy analyzer and verify that constraint violations occur. (The malicious methods may be constructed using a bytecode construction library such as BCEL, a JVM assembler such as Jasmin, or a binary editor.)

Finally, use the analyzer to investigate the following conjecture: the stack depth must be exactly 1 when a return instruction is encountered in a benign method.

It is not necessary to model all JVM arithmetic instructions. Choose a representative sample (add, sub, div, mul, neg, mod).

The model should check the following constraints when a return instruction is encountered:

- the stack depth must be at least 2 for binary instructions and at least 1 for unary instructions,
- the stack must contain item(s) whose type matches the instruction.

Thus, for the second constraint, it must be the case that ladd pops two longs, ddiv pops two doubles, and so forth.

Test the model as follows. Write a simple set of Java methods that perform various simple computations (without type promotion), compile them, and apply the Alloy analyzer to the resulting model of the JVM bytecodes for those methods. Verify that all constraints are satisfied (no counterexamples). Then, construct two malicious methods that will violate each constraint. Apply the Alloy analyzer and verify that constraint violations occur. (The malicious methods may be constructed using a bytecode construction library such as BCEL, a JVM assembler such as Jasmin, or a binary editor.)

Finally, use the analyzer to investigate the behavior of Java methods in which type promotion does occur as part of an arithmetic operation.

The model should check the following constraints for a method that contains either a monitorenter instruction or a monitorexit instruction:

- the stack depth must be at least 1 for either monitor instruction,
- the stack must contain an object reference.

Test the model as follows. Write a simple Java method that contains a single synchronized statement (see section 7.14 of the JVM spec for an example). Compile it, and apply the Alloy analyzer to the resulting model of the JVM bytecodes for that method. Verify that all constraints are satisfied (no counterexamples). Then, construct two malicious methods that will violate each constraint. Apply the Alloy analyzer and verify that constraint violations occur. (The malicious methods may be constructed using a bytecode construction library such as BCEL, a JVM assembler such as Jasmin, or a binary editor.)

Finally, use the analyzer to investigate the following conjecture: if a monitor has been entered in a method, then every execution path that leads to a return from the method contains exactly one occurence of the monitorexit instruction.

Created: 2011.01.02 Last modified: 2011.01.05