Mark Reynolds' web page
There are four Projects for the
Spring 2011 CS511 course that will use Alloy.
I gave a presentation on Jan 25, 2011 that
describes how Alloy is used to model software systems.
It contains a simple
Filesystem model that was derived from the Alloy tutorial.
On Jan 31, 2011 I gave a follow-up presentation on the Java Virtual Machine.
My thesis work is based on applying Alloy to model the security properties of
including the Java Virtual Machine,
Part of the Alloy model I have for the JVM security constraints is here. This fragment uses
the "fred()" method of test.java which
dissassembles into these JVM instructions.
of the relation values is available in OpenOffice or
This model fragment checks three constraints:
There is also a deliberately malformed version of the model that shows that if
- Local variable constraint
- Stack depth invariance constraint
- Stack guard constraint
the local variable constraint is violated, the model produces a counterexample.
Violation of the stack guard constraint is shown here.
The Alloy model contains initialization statements that are produced by a classfile-to-Alloy
translator. The Java source for this translator is contained in two files Class2Alloy.java
and AlloyString.java. The Bytecode Engineering Library (BCEL), a part of Jakarta, is also
Note: Older versions of Eclipse are not happy with BCEL's jar
file. I recommend you upgrade
to a recent release of Eclipse, or use
another Java IDE such as JCreator.
Lightweight Modeling of Java Virtual Machine Security Constraints
Modeling the Java Bytecode Verifier
Security Model and Bytecode Verification.