Mark Reynolds' web page
Description
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 test.java 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:- Local variable constraint
- Stack depth invariance constraint
- Stack guard constraint
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 Class2Alloy.java
and AlloyString.java. The Bytecode Engineering Library (BCEL), a part of Jakarta, is also
required.
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
