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: 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

Imja Tse Himal