FRAMES  NO FRAMES

Projects Using Alloy

Project 1: Alloy model of JVM array load instructions

Develop an Alloy model that will successfully analyze a binary representation of a Java method for conformance with the specification regarding array load instructions (baload, caload, ...). The model should capture the static and dynamic properties of an arbitrary method. Static properties include immutable properties of the instructions in the method, e.g. baload is a 1-byte instruction that pops 2 items off the stack, and then pushes 1 item onto the stack. Dynamic properties include the execution state as the method is executed. In particular, the model should capture the depth of the stack and the types of all elements on the stack.

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

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.)

Project 2: Alloy model of JVM return instructions

Develop an Alloy model that will successfully analyze a binary representation of a Java method for conformance with the specification regarding return instructions (areturn, dreturn, ...). The model should capture the static and dynamic properties of an arbitrary method. Static properties include immutable properties of the instructions in the method, e.g. areturn is a 1-byte instruction that pops 1 item off the stack. Dynamic properties include the execution state as the method is executed. In particular, the model should capture the depth of the stack and the types of all elements on the stack.

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

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.

Project 3: Alloy model of JVM arithmetic instructions

Develop an Alloy model that will successfully analyze a binary representation of a Java method for conformance with the specification regarding arithmetic instructions (ddiv, ladd, ...). The model should capture the static and dynamic properties of an arbitrary method. Static properties include immutable properties of the instructions in the method, e.g. ladd is a 1-byte instruction that pops 2 items off the stack and pushes one. Dynamic properties include the execution state as the method is executed. In particular, the model should capture the depth of the stack and the types of all elements on the stack.

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:

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.

Project 4: Alloy model of JVM monitors

Develop an Alloy model that will successfully analyze a binary representation of a Java method for conformance with the specification regarding Java methods that use synchronized statements. The model should capture the static and dynamic properties of an arbitrary method. Static properties include immutable properties of the instructions in the method, e.g. monitorenter is a 1-byte instruction that pops 1 item off the stack. Dynamic properties include the execution state as the method is executed. In particular, the model should capture the depth of the stack, the types of all elements on the stack, and the current state of the monitor.

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

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