Mark Reynolds' web page


Description

I'm working on applying the Alloy modeling language to the security constraints
imposed by the Java Virtual Machine. My initial project proposal is available.

My midterm presentation is available in PowerPoint or OpenOffice format>

My final presentation is available in PowerPoint or OpenOffice format.

The project final report is here.

Journal

I have an ongoing journal of the work.

The Model

The Alloy model I have for the JVM security constraints is here. It is currently based on
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.
The model 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: Eclipse is not happy with BCEL's jar file. May I recommend Jcreator instead? It's small
and the LE version is free.

Related Papers

Java Security Model and Bytecode Verification.
JVM Specification

Imja Tse Himal