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 interpreted languages,
including the Java Virtual Machine, Flash/ActionScript, Dalvik/Android, CIL and JavaScript.

The Model

Part of the Alloy model I have for the JVM security constraints is here. This fragment uses
the "fred()" method of which dissassembles into these JVM instructions.
A table of the relation values is available in OpenOffice or Excel format.
This model fragment checks three constraints: There is also a deliberately malformed version of the model that shows that if
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
and 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.

Related Papers

Lightweight Modeling of Java Virtual Machine Security Constraints

Modeling the Java Bytecode Verifier

Java Security Model and Bytecode Verification.

JVM Specification


Resume of Mark C. Reynolds

Imja Tse Himal