The Jalapa Tutorial v 0.5 Logo

Jalapa is an extension to the security model of Java, that allows for specifying, analysing and enforcing history-based usage policies.

Policies are defined by usage automata, that recognize the forbidden execution histories. Usage automata are an extension of finite stata automata, with some additional features that make them practical for expressing usage policies.

Programmers can either enforce e policy globally, or can sandbox an untrusted piece of code with a policy, which is enforced at run-time through its local scope.

This tutorial will guide you to securing Java programs with Jalapa.


First, you need to install Jalapa on your machine. Assume you are using a Unix/Linux system (installation is also possible under Windows and Mac OS/X, but the instructions on how to do that, as well as the command lines in this tutorial, might be quite different). Download the Jalapa sources from the Sourgeforge svn repository:

svn co jalapa 

This will create a directory named jalapa with the following structure:

Makefile              // the makefile for the GNU make utility
bcel                  // the Apache BCEL library
Jalapa                // the Eclipse plugin (development version)
jisel                 // the Jalapa Runtime Environment
LocUsT                // the usage policies model-checker
StaticAnalysis        // the static analyser (develpment version)
web                   // this tutorial
examples              // the test examples used in this tutorial

To compile the runtime environment, and produce the jar archive:

cd jalapa
make jisel

A simple usage policy

Assume you are given the following untrusted Java code, that reads the first line from a given input file, and writes it to a given output file (see


public class WriteFile {

    public static void main(String args[]) {
	    try {			
            BufferedReader rf = new BufferedReader(new FileReader(args[0]));
            BufferedWriter wf = new BufferedWriter(new FileWriter(args[1]));

            String s = rf.readLine();
            wf.write(s, 0, s.length());

        } catch (IOException e) {

A clear attack would be that of reading a private file, and writing it to a public location on the disk. Note that the Java stack inspection mechanism offers no protection against this kind of attacks (unless that of brutally prohibiting any file write), because after the method read has returned, there is no trace of it left on the call stack.

The Jalapa security model supersedes Java stack inspection by allowing for the specification and enforcement of history-based policies. A policy is defined through a usage automaton, that formally specifies which sequences of method calls (a.k.a. traces), are not permitted. Back to our example, we want to prohibit any sequence of method calls where a file write is performed after a file read. This policy is specified by the usage automaton chinese-wall below:

name: chinese-wall
read := (
write := ( s, int off, int len)
states: q0 q1 fail
start: q0
final: fail
q0 -- read --> q1
q1 -- write --> fail

A usage automaton closely resembles a finite state automaton, composed of six fields that we are going to explain. The field tagged name just defines the name of the policy. The tag aliases introduces some convenient shorthands for the methods mentioned in the policy. An alias can be seen as the abstraction of (the signature of) a security-relevant method into an event, that triggers a transition on the usage automaton in hand.

In the usage automaton chinese-wall above, the event read is fired whenever the method readLine() of the class BufferedReader is invoked. Similarly, the event write is fired when the method with signature BufferedWriter.write(String,int,int) is invoked. In our policy, the parameters s of type String, off of type int, and len of type int are immaterial, so our aliases will neglect them.

The remaining fields describe the logics of the automaton: the tag states is for the set of states, start is for the initial state, and final is for the final state, that we assume to denote a policy violation. The tag trans preludes to the transition relation of the automaton. In our example, a transition from q0 to q1 occurs upon reading any file. A transition from q1 to fail occurs upon writing any file. Since the state fail is declared to be offending, this actually implements the desired Chinese Wall policy. For instance, consider the following trace:

...                                // constructors of the superclasses of FileReader
(rf:FileReader).<init>(args[0])    // constructor of the class FileReader
(rf:BufferedReader).<init>()       // constructor of the class BufferedReader
...                                // constructors of the superclasses of FileWriter
(wf:FileWriter).<init>(args[1])    // constructor of the class FileWriter
(wf:BufferedWriter).<init>()       // constructor of the class BufferedWriter
(rf:BufferedReader).readLine()     // method readLine() of the class BufferedReader
(wf:BufferedWriter).write(s)       // method write(String) of the class BufferedWriter

This trace violates the Chinese Wall policy, because it is mapped to the sequence of events read write, which leads the usage automaton to the fail state. Notice that the other method calls correspond to self-loops (not explicitly written) in the usage automaton.

So far, we have seen how to specify our Chinese Wall policy. To enforce it on our Java program, we will run WriteFile inside a sandbox. This will be set up by Jisel, our Java Instrumentator for the Security Enforcement of Local policies. This tool instruments the Java bytecode, by inserting the pieces of code needed to implement the security mechanism. More in detail, Jisel performs the following operations:

  1. it detects the set M of all the methods involved in policies.
  2. then, it inspects the bytecode, starting from the methods used in the aliases, and then computing a sort of transitive closure through a visit of the inheritance graph.
  3. it creates a wrapper for each of these security-relevant methods. A wrapper WC for the class C declares exactly the same methods of C, implements all the interfaces of C, and extends the superclass of C. Indeed, WC can replace C in any context, in that it admits the same operations of C. The wrapper class WC has a single field, which will be assigned upon instantiation of C.
  4. A method m of WC can be either monitored or not. If the corresponding method m of C does not belong to M, then WC.m simply calls C.m. Otherwise, WC.m calls the PolicyPool.check method that controls whether C.m can actually be executed without violating the active policies. A further step substitutes (the references to) the newly created classes for (the references to) the classes in the original program.
  5. Finally, the instrumented code is deployed and linked to the Jisel run-time support, i.e. a library that contains the resources necessary to the monitoring process. Note that the instrumentation phase produces a stand-alone application, requiring no custom JVM and no external components other than the library.

Assume you have written the policy chinese-wall above in a file named e.g. mypolicies.upy in the same directory jalapa/examples/cw where WriteFile.class is located (actually, the file name mypolicies is irrelevant: Jisel searches the provided directory for all the files with the extension .upy). To run the Jisel rewriter, we must supply the following command line:

cd jalapa/examples/cw
cd ..
java -Dpolicies=chinese-wall -cp ..:../bcel/bcel-5.2.jar jisel.Jisel cw -o cw-sec -m WriteFile

The system property policies specifies the set of policies (separated by commas) to be considered by Jisel. The class path must comprise the jar with the BCEL classes (IMPORTANT: do not swap the system property with the class path). With the option -o one can choose the destination path of the instrumented classes, in our case the directory cw-sec. The option -m provides Jisel with the entry point of the program, in our case the class WriteFile.

To run the instrumented program, one must supply the set of policies to be enforced, besides the inputs of the original program, if any. The command line for our example is as follows:

cd cw-sec
echo secret > in
java -cp .:../../jisel.jar WriteFile in out

With the system property we inform the runtime environment that the policy chinese-wall has to be globally enforced throughout the execution of WriteFile. As expected, running the sandboxed code will yield a security exception:

Exception in thread "main" jisel.policy.SecurityPolicyException: 
Event ( arg0,int arg1,int arg2) Not allowed!
	at WriteFile.main(

Usage policies with parameters

The usage automaton chinese-wall of the previous example is much alike a finite state automaton, the only difference being that the final state fail represents an offending condition, instead of acceptance. In the following sections we shall present several enhancements of usage automata, which make them strictly more expressive than finite state automata. Along with the newly introduced features, we shall show some realistic policies exploiting them.

We consider first the implementation of a list datatype which allows for iterating over the elements of the list. In this scenario, a relevant safety policy is that preventing list modifications when the list is being iterated (indeed, Java collections implement this behaviour through local checks).

We first show an unsafe implementation of the class ListIter (see and, and then we shall show a usage automaton which can be used to enforce the above-mentioned policy.

public class ListIter {

    private Object[] v;
    private int last;
    private int iter;

    public ListIter() {
	v = new Object[3];
	last = 0;
	iter = -1;

    public void add(Object o) {
		if (last == v.length) {
			Object[] v2 = new Object[v.length * 2];
			for (int i=0; i<last; i++) v2[i] = v[i];
			v = v2;
		v[last++] = o;
    public void remove(Object o) {
		int i,j;
		for (i=0; i<last; i++) if (v[i] ==o) break;
		if (i<last) for (j=i+1; j<last; j++) v[j-1] = v[j];
		last = last-1;

    public void startIterator() {
		iter = 0;

    public Object next() throws Exception {
		if (iter>=last) throw new Exception("Iteration out of bounds");
		return v[iter++];

    public boolean hasNext() {
		return (iter<last);
    public String toString() {
		String s = "[";
		for (int i=0; i<last; i++) s += v[i] + ((i==last-1)? "" : ";");
		return s + "]";
public class ListIterTest {
    public static void main(String[] args) throws Exception {
	ListIter l0 = new ListIter(), l1 = new ListIter();
	String v0[] = {"a", "b", "c"}, v1[] = {"d", "e", "f"};
	for (int i=0; i<v0.length; i++) { l0.add(v0[i]); }
	for (int i=0; i<v1.length; i++) { l1.add(v1[i]); }

	while (l0.hasNext()) {
	    Object o0 =;
	    boolean found = false;
	    while (l1.hasNext()) {
		Object o1 =;
		if (o0==o1) found=true;
	    if (!found) { l1.add(o0); l0.remove(o0); }
	System.out.println("l0 = " + l0);
	System.out.println("l1 = " + l1);

The method main defines two lists l0 and l1, and joins them into l1, while removing the duplicates. Note that the resulting list l1 is [d;e;f;a;c], instead of the expected [d;e;f;a;b;c]. To prevent from this erroneous behaviour, we now define the usage automaton safe-iterator, that will be used to abort a computation when the method next() is invoked on a given list l after l has been modified.

name: safe-iterator
start(l) := (l:ListIter).startIterator()
next(l) := (l:ListIter).next()
modify(l)  := (l:ListIter).add(java.lang.Object o)
modify(l) := (l:ListIter).remove(java.lang.Object o)
states: q0 q1 fail
start: q0
final: fail
q0 -- modify(l) --> q1
q1 -- next(l) --> fail
q1 -- start(l) --> q0

Differently from the previous example, now the aliases have a parameter l, that stands for the target list upon which the methods start, next, add, and remove are invoked. For instance, consider the alias:

start(l) := (l:ListIter).startIterator()

This means that the event start(l) will be fired whenever the method startIterator() is invoked on an object l of type ListIter. The alias next(l) is similar. The methods add and remove are aliased by the event modify(l), which will be fired whenever add or remove are invoked on an object l of class ListIter. In this policy the formal parameter o of class Object is irrelevant, so our events will neglect it.

The usage automaton has three states: q0, q1, and fail. In the state q0 both modifications of the list and iterations are possible. However, a modification (i.e. an add or a remove) done in the state q0 will lead to q1, where it is no longer possible to iterate on l, until a start(l) resets the situation.

As in the previous case, we use Jisel to instrument the above code, and we run it while globally enforcing the policy safe-iterator.

cd jalapa/examples/safeiter
cd ..
java -Dpolicies=safe-iterator -cp ..:../bcel/bcel-5.2.jar jisel.Jisel safeiter -o safeiter-sec -m ListIterTest
cd safeiter-sec
java -cp .:../../jisel.jar ListIterTest

This will produce the expected exception, thrown after the element "a" is removed from l0 and the method next is subsequently invoked on the same list.

Exception in thread "main" jisel.policy.SecurityPolicyException: Event (_:ListIter).next() Not allowed!
	at ListIterTest.main(

The offending trace is summarized below:

start(l0)         // l0.startIteration()
next(l0)          //
start(l1)         // l1.startIteration()
next(l1)          //
next(l1)          //
next(l1)          //
modify(l1)        // l1.add("a")
modify(l0)        // l0.remove("a")
next(l0)          //

Formally, the enforcement mechanism recognizes the above execution trace as offending, by transforming the usage automaton into a set of finite state automata, and by using them as sequence recognizers. The transformation is called instantiation, because the formal parameter l is replaced by tha actual values l0 and l1. For instance, the finite state automaton for the instantition of l into l0 is as follows:

Finite state automaton for safe-iterator(l0)

Note that self-loops are generated for those transitions not explicitly mentioned in the usage automaton, and for those transitions not relevant for the current instantiation. This finite state automaton recognizes the execution trace above as offending. In general, since finite state automata can be non-deterministic, we define a trace to be offending when there exists some path leading to an offending state - a form of diabolic non-determinism. We say a trace T respects a usage policy P when none of the possible instantiations of P on the actual parameters in T will recognize T as offending. Full technical details can be found in this paper.

Dealing with multiple parameters

Pushing further the number of parameters increases the expressiveness of usage policies. The expressivity gain obtained by adding parameters is strict, e.g. the set of policies that may speak of two parameters is strictly more expressive of the set of policies with a single parameter. However, it is reasonable to think that real-world usage policies will hardly need more than five or six parameters.

As an example, consider a simple BankAccount class, which allows the customers of a bank to manage their accounts (see and The featured API has methods for depositing and withdrawing money, and for transferring money between two accounts. Furthermore, a customer can authorize/deny a third party to grab money from his account, e.g. an energy company which charges for the monthly fee.

import java.util.*;

public class BankAccount {
    private String customer;
    private int balance;
    private List authorized;

    public BankAccount(String customer, int balance) {
	this.customer = customer;
	this.balance = balance;
	authorized = new ArrayList();

    public int getBalance() {
	return balance;

    public void deposit(int amount) {
	balance += amount;

    public void withdraw(int amount) throws Exception {
	if (amount > balance) throw new Exception("Overdraft");
	balance -= amount; 

    public void transfer(int amount, BankAccount dst) throws Exception {
	System.out.print("Transferring " + amount + " from " + customer + " to " + dst + "... ");
	if (!authorized.contains(dst)) {
	    throw new Exception("Unauthorized transfer");

    public void allowTransfer(BankAccount a) {
    public void denyTransfer(BankAccount a) {

    public String toString() {
	return customer;
public class BankAccountTest {
    public static void main(String[] args) throws Exception {
	    BankAccount alice = new BankAccount("alice", 100);
	    BankAccount bob = new BankAccount("bob", 200);
	    BankAccount acme = new BankAccount("acme", 1000);
	    alice.transfer(50, acme);
	    bob.transfer(60, acme);
	    alice.transfer(70, acme);
	    alice.transfer(80, acme);

Note that the above implementation is buggy, because it uses lists instead of sets to manage authorizations. Indeed, running the main method allows the Acme company to grab 80 bucks from Alice's account, even though Alice has denied Acme to do that. To recover from this situation, we enforce the following policy, defined by the usage automaton authorized-transfer below. The policy prevents a company from transferring money from a customer account, unless explicitly allowed (and no subsequently denied) to do that.

name: authorized-transfer
allow(a0,a1) := (a0:BankAccount).allowTransfer(BankAccount a1)
deny(a0,a1) := (a0:BankAccount).denyTransfer(BankAccount a1)
transfer(a0,a1) := (a0:BankAccount).transfer(int b, BankAccount a1)
states: q0 q1 fail
start: q0
final: fail
q0 -- allow(a0,a1) --> q1
q1 -- deny(a0,a1) --> q0
q0 -- transfer(a0,a1) --> fail

We first discuss on the aliases introduced by the policy. They have two parameters: a0 which stands for the "source" bank account, and a1 for the "destination" account. For instance, consider:

transfer(a0,a1) := (a0:BankAccount).transfer(int b, BankAccount a1)

Here, a0 is the target object, of class BankAccount, upon which the method transfer is invoked. The parameter a1 in the alias is the formal parameter of class BankAccount in the method transfer. The aliases allow and deny are similar.

The usage automaton authorized-transfer(a0,a1) has three states. In the state q0, money transfers from account a0 to a1 are not permitted, while in the state q1 they are. Attempting a money transfer while in state q0 leads to the offending state fail.

cd jalapa/examples/bank
cd ..
java -Dpolicies=authorized-transfer -cp ..:../bcel/bcel-5.2.jar jisel.Jisel bank -o bank-sec -m BankAccountTest
cd bank-sec
java -cp .:../../jisel.jar BankAccountTest

Executing the method main of the class BankAccountTest produces the following output:

Transferring 50 from alice to acme... done
Transferring 60 from bob to acme... done
Transferring 70 from alice to acme... done
Exception in thread "main" jisel.policy.SecurityPolicyException: 
Event (_:BankAccount).transfer(int arg0,BankAccount arg1) Not allowed!
	at jisel.BankAccount_Jisel.transfer(
	at BankAccountTest.main(

The expected security exception is due to the following trace:

allow(alice,acme)           // alice.allowTransfer(acme)
allow(bob,acme)             // bob.allowTransfer(acme)
transfer(alice,acme)        // alice.transfer(50, acme)
transfer(bob,acme)          // bob.transfer(60, acme)
allow(alice,acme)           // alice.allowTransfer(acme)
transfer(alice,acme)        // alice.transfer(70, acme)
deny(alice,acme)            // alice.denyTransfer(acme)
transfer(alice,acme)        // alice.transfer(80, acme)

Eight possible instantiations of the policy authorized-transfer have to be considered by the enforcement mechanism, i.e. all the sequences of two elements from the set {alice, bob, acme}. The instantiation that leads to the offending state is authorized-transfer(alice,acme), which corresponds to the following finite state automaton (for simplicity, self-loops are omitted):

Finite state automaton for authorized-transfer(alice,acme)

As expected, this automaton correctly recognizes as offending the execution trace reported above.


Many real-world policies require the ability of speaking about "all possible objects", or stating that "a certain object x has to be different from some other object y". An instance of the first case is a policy requiring that a given method cannot be applied twice, regardless of the target object; an instance of the second case is any policy saying that after some method m has been invoked on o, then m cannot be applied on any other object different from o.

As a more involved example, we consider a class ClassifiedFile, that maintains a given secret until two (distinct) security officers authorize its disclosure. Again, we consider a buggy implementation where lists are misused instead of sets (see and The method disclose() reveals the secret contained in the classified file, if the needed authorizations have been granted (but mind the bug). The method authorize allows an officer to grant an authorization to the target file. The method suspend can be invoked by any officer, to prevent the file from receiving authorizations (in more refined scenarios, one can imagine a Chief Security Officer doing this to make a file "top secret"). Conversely, the method resume gets the authorizations possible again.

import java.util.*;

public class ClassifiedFile {

	private static final Set securityOfficers = new HashSet();
	private String id;
	private String secret;
	private boolean canAuth;
	private List<String> authorizations;

	public ClassifiedFile(String id, String secret) { = id;
		this.secret = secret;
		this.canAuth = true;
		authorizations = new ArrayList<String>();

	public static void addOfficer(String officer) {

	public String disclose() throws Exception {
		if (authorizations.size() < 2) throw new Exception("Access denied");
		System.out.println("Disclosure of file " + id + " authorized by " + authorizations);
		return secret;

	public void authorize(String officer) {
		if (securityOfficers.contains(officer) && canAuth)

	public void suspend(String officer) {
		if (securityOfficers.contains(officer)) canAuth = false;

	public void resume(String officer) {
		if (securityOfficers.contains(officer)) canAuth = true;
public class ClassifiedFileTest {
	public static void main(String[] args) throws Exception {

		ClassifiedFile emc = new ClassifiedFile("emc", "e = m c^2");

		ClassifiedFile pnp = new ClassifiedFile("pnp", "P = NP");		

Consider first the policy stating that a suspended file cannot receive authorizations. This is modelled by the following usage automaton:

name: suspend-auth
auth(f,o) := (f:ClassifiedFile).authorize(java.lang.String o)
suspend(f,o) := (f:ClassifiedFile).suspend(java.lang.String o)
resume(f,o) := (f:ClassifiedFile).resume(java.lang.String o)
states: q0 q1 fail
start: q0
final: fail
q0 -- suspend(f,*) --> q1
q1 -- resume(f,*) --> q0
q1 -- auth(f,*) --> fail

Notice the wildcard * used in transitions: as expected, * may stand for each possible officer. That is, a transition from q0 to q1 is possible whenever the method suspend is invoked on the file f, regardless of the officer who issued that. The other transitions are similar. Clearly, attempting an authorization of f while in q1 leads to the offending state.

Consider now the policy requiring that two distinct authorizations are needed to discose a classified file. Because of the buggy implementation, running the method main will reveal the secret content of the classified file pnp, although only one officer has authorized its disclosure. Enforcing the following usage policy ensures that this kind of anomalous behaviour cannot occur.

name: double-agreement
auth(f,o) := (f:ClassifiedFile).authorize(java.lang.String o)
disclose(f) := (f:ClassifiedFile).disclose()
states: q0 q1 ok fail
start: q0
final: fail
q0 -- auth(f,o) --> q1
q0 -- auth(f,-) --> ok
q1 -- auth(f,-) --> ok
q0 -- disclose(f) --> fail
q1 -- disclose(f) --> fail

The usage automaton double-agreement(f,o) has two parameters (a classified file f and a security officer o) and four states. The state q0 models the fact that f has been granted zero authorizations. In the state q1 one authorization has been received, by the officer o. A transition from q1 to ok is possible when an authorization is granted by an officer different from o. Indeed, the meaning of the wildcard - is: "any object different from any other object mentioned in the policy". Trying to disclose f when in states q0 or q1 leads to the offending state. The disclosure of f is only possible in the state ok, where both the needed distinct authorizations have been granted.

Let's see how the enforcement mechanism deals with conditions in our example. Running the method main of the class ClassifiedFile produces the following trace:

auth(emc,alice)       // emc.authorize("alice")
auth(emc,bob)         // emc.authorize("bob")
disclose(emc)         // emc.disclose()
auth(pnp,alice)       // pnp.authorize("alice")
auth(pnp,alice)       // pnp.authorize("alice")
disclose(pnp)         // pnp.disclose()

There are six possible instantiations of the usage automaton double-agreement we need to consider, i.e. all the possible choices of an officer, times all the possible choices of a classified file. As an example, we consider double-agreement(pnp,alice), which will recognize the above trace as offending when the last event is fired. The finite state automaton resulting from this instantiation is depicted below, where self-loops have been omitted for simplicity:

Finite state automaton for double-agreement(alice,pnp)

Notice the second transition in the usage automaton double-agreement, which leads to the ok state when the first authorization is received by an officer different from o. This is needed to identify the object o upon which the usage automaton is instantiated with the first officer which grants an authorization. This transition were omitted, some valid traces would be recognized as offending, e.g. auth(emc,alice) auth(emc,bob) disclose(emc) on the instantiation double-agreement(emc,bob).

Local policies

Suppose you have a simple Web browser whose functionality can be extended with plugins, and with methods for handling connections and cookies. Since plugins can be downloaded from the network, possibly from untrusted sites, we want to control their behaviour, and block their execution at the moment they attempt some malicious action. In particular, we focus here on two confinement policies, that prevent plugins from transmitting data read from the local file system, either directly or by exploiting cookies to implement a covert communication channel. Before formally specifying these policies, it is convenient to consider a skeletal implementation of the classes Browser and Plugin.

import java.util.*;
import jisel.policy.PolicyPool;

public class Browser {
    private Map cookies;
    public Browser() { cookies = new HashMap(); }
    public void connect(URL url) throws Exception {
		System.out.print("opening URL connection...");
		URLConnection uc = url.openConnection();
		System.out.print("opening input stream...");
		BufferedReader in = new BufferedReader(new InputStreamReader(uc.getInputStream()));
		System.out.print("opening output stream...");
		BufferedWriter out = new BufferedWriter(new OutputStreamWriter(uc.getOutputStream()));
		// out.write(...)
    public void writeCookie(URL u, String msg) {
    public String readCookie(URL u) {
		return cookies.get(u);
public class BrowserTest {
    public static void main(String[] args) throws Throwable {
		Browser b = new Browser();
		Plugin p0 = new GoodPlugin(b);
		Plugin p1 = new UntrustedPlugin(b);
import jisel.policy.PolicyPool;

public abstract class Plugin implements Runnable {
    private Browser browser;
    private String name;
    private URL codebase;
    Plugin(Browser browser, String name, URL codebase) {
		this.browser = browser; = name;
		this.codebase = codebase;
    public void doIt() {
		try {
			System.out.println("sandboxing " + this + "...");
			PolicyPool.sandbox("plugin-cw", this);
		} catch (Throwable e) {
    public Browser getBrowser() {
		return browser;
    public URL getCodeBase() {
		return codebase;
    public String toString() {
		return name + " [" + codebase.toString() + "]";

We assume that browser plugins extend the Plugin abstract class, by implementing the method run(). The browser starts a plugin by invoking the method doIt(), which is quite peculiar. Actually, it defines a sandbox, which will enforce the policy plugin-out throughout the run of the plugin. This means that all the security-relevant methods called while executing the method run() will be monitored, and blocked if not conformant to the policy. This policy is specified by the usage automaton plugin-out below.

name: plugin-out
read  := (<init>()
read  := (Browser).readCookie( u)
write := (
states: q0 q1 fail
start: q0
final: fail
q0 -- read --> q1
q1 -- write --> fail

The event read is fired whenever a new object of the class FileInputStream is created, or a cookie is accessed through the method getCookie. Similarly, the event write is fired when the method getOutputStream is invoked on a Socket. A transition from q0 to q1 occurs upon reading any file or cookie. A transition from q1 to fail occurs upon opening an output stream on a socket.

The second policy is specified by the usage automaton plugin-cookie below, which introduces another peculiar feature of Jalapa: guards. We start from the state q0. The event init(p,u), signalling the creation of a new plugin p with codebase URL u, causes a transition to q1. Upon a start(p), i.e. when p is launched by the browser, we reach q2. There, all the accesses to a cookie having a URL different from u lead to the offending state. When the control is transferred to another plugin, we reset the state to q1. At run-time, the policy plugin-cookie is enforced for all the possible instantiations of the formal parameters p, u and u'. Since this policy spans over multiple activations of plugins, we enforce it globally throughout the execution of the browser.

name: plugin-cookies
cookie(u) := (Browser).writeCookie( u, java.lang.String m)
cookie(u) := (Browser).readCookie( u)
init(p,u) := (p:Plugin).( u)
start(p)  := (p:Plugin).doIt()
states: q0 q1 q2 fail
start: q0
final: fail
q0 -- init(p,u) --> q1
q1 -- start(p) --> q2
q2 -- cookie(u') --> fail when u'!=u
q2 -- start(p') --> q1 when p'!=p

We produce a bytecode with the needed hooks for the Jalapa runtime environment, yet it is NOT the sandboxed code we are aiming at. Actually, running java Browser is promptly aborted with a NoClassDefFoundError exception. The expected sandboxed program is obtained from the compiled bytecode through a transformation step, implemented by the Jisel bytecode rewriter.

Example: a secure Bulletin Board

We now consider a simple bulletin board system inspired by phpBB, a popular open-source Internet forum written in PHP. We assume as given a Java implementation of the server-side of the bulletin board, and we make it secure through a set of globally enforced usage policies.

The bulletin board consists of a set of users and a set of forums. Users can create new topics within forums. A topic represents a discussion, to be populated by posts inserted by users. Users may belong to three categories: guests, registered users, and, within these, moderators. We call regular users those who are not moderators. Each forum is tagged with a visibility level:

Additionally, we assume there exists a single administrator, which is the only user who can create new forums and delete them, set their visibility level, and lock/unlock them. Moderators can edit and delete the posts inserted by other users, can move topics through forums, can delete and lock/unlock topics. Both the administrator and the moderators can promote users to moderators, and viceversa; the administrator cannot be demoted. The public interface of the bulletin board SecBB is given below.

User addUser(String username, String pwd);
Session login(String username, String pwd);
void logout(User u, Session s); 
void deleteUser(User u0, Session s, User u1); 
void promote(User u0, Session s, User u1);
void demote(User u0, Session s, User u1); 
void addPost(User u, Session s, Post p, Topic t, Forum f);  
void editPost(User u, Session s, Post p, Topic t, String msg);  
void deletePost(User u, Session s, Post p, Topic t);  
void addTopic(User u, Session s, Topic t, Forum f);  
void deleteTopic(User u,  Session s, Topic t, Forum f);
void moveTopic(User u, Session s, Topic t, Forum src, Forum dst);  
void lockTopic(User u, Session s, Topic t);  
void unlockTopic(User u, Session s, Topic t);  
List viewTopic(User u, Session s, Topic t); 
void addForum(User u, Session s, Forum f); 
void deleteForum(User u, Session s, Forum f);  
void setVisibility(User u, Session s, Forum f, Forum.Visibility v);
void lockForum(User u, Session s, Forum f);  
void unlockForum(User u, Session s, Forum f);  
List viewForum(User u, Session s, Forum f);

In this scenario, we assume only the bytecode of the bulletin board is available. We consider below a substantial subset of the policies implemented (as local checks hard-wired in the code) in phpBB, and we specify them through usage automata. We shall globally enforce these policies through the Jalapa Runtime Environment.

Also, some sanity checks can be easily specified as usage automata. For instance: session identifiers must be fresh, users have to logout before logging in again, a message cannot be posted twice, a topic cannot be created twice, a message belongs to exactly one topic, a topic belongs to exactly one forum, a deleted message cannot be edited, a deleted topic cannot be moved, non-existing topics and forums cannot be locked/unlocked, etc.

We now show how to formalize some of the above-mentioned policies as usage automata. It is convenient to introduce some aliases first.

post(u,s,p,t,f) := SecBB.addPost(User u, Session s, Post p, Topic t, Forum f)
edit(u,s,p) := SecBB.edit(User u, Session s, Post p, String msg)
delete(u,s,p) := SecBB.deletePost(User u, Session s, Post p)
lockT(t) := SecBB.lockTopic(User u, Session s, Topic t)
unlockT(t) := SecBB.unlockTopic(User u, Session s, Topic t)
promote(u0,u1) := SecBB.promote(User u0, Session s, User u1)
demote(u0,u1) := SecBB.demote(User u0, Session s, User u1)

Consider first the policy requiring that ``nobody can post on a locked topic''. This is modelled by the usage automaton no_post_locked_topic below. In the start state q0, locking the topic t leads to q1. From q1, posting to the topic t (i.e. firing the event post(*,*,*,t,*), where * is a wildcard matching any resource) leads to the offending fail state, while unlocking t leads back to q0.

name: no_post_locked_topic   
states: q0 q1 fail   
start: q0
final: fail  
q0 -- lockT(t) --> q1
q1 -- unlockT(t) --> q0  
q1 -- post(*,*,*,t,*) --> fail   

Consider now the policy ``only moderators can promote and demote other users''. This is modelled by the usage automaton mod_promote_demote below. The state q0 models u being a regular user, while q1, is for when u is a moderator. The first two transitions actually represent u being promoted and demoted. In the state q0, u cannot promote/demote anybody, unless u is the administrator. For example, the trace T = promote(admin,u1) promote(u1,u2) demote(u2,u1) respects the policy, while T promote(u1,u3) violates it.

name: mod_promote_demote
states: q0 q1 fail
start: q0
final: fail
q0 -- promote(*,u) --> q1
q1 --  demote(*,u) --> q0
q0 -- promote(u,*) --> fail when u!=admin
q0 --  demote(u,*) --> fail when u!=admin

We now specify the policy stating that ``the session identifier used when interacting with the bulletin board must be the one obtained at login''. For simplicity, we only consider post events; adding the other kinds of intraction is straightforward. The needed aliases are defined as follows:

login(u,s) := SecBB.login(String username, String pwd)
              > SessionTable.put(User u, Session s)
logout(u) := SecBB.logout(User u)

Note that the alias for the login event is defined quite peculiarly. This is because the formal parameters of the method SecBB.login are two strings (user name and password), while our policy needs to speak about a User and a Session. To do that, we inspect the code of the method SecBB.login, and find that it implements the action of logging in a user by inserting a pair (User u, Session s) into a SessionTable. This is what the alias above stands for: an event login(u,s) is fired whenever an SessionTable.put(User u, Session s) occurs within the context of a call to SecBB.login(String username, String pwd). The policy post_sid follows. The state q0 models u being a guest user, while in q1, u has logged in. In the state q0, guests are prohibited from posting a message. In the state q1, posting with a session id s2 is prohibited if s is not the same id s1 obtained at login.

name: post_sid
states: q0 q1 fail
start: q0
final: fail
q0 -- post(u,*,*,*,*) --> fail when u!=guest
q0 -- login(u,s1) --> q1
q1 -- logout(u) --> q0
q1 -- post(u,s2,*,*,*) --> fail when s2!=s1

The policy mod_author_post states that ``a message can be edited/deleted by its author (unless it is a guest) or by a moderator, only''. The policy post_after_reply below states that a regular user cannot delete a message after it has been replied to. The states q0,q1, and q2 correspond to the conditions ``not posted'', ``posted, no reply'', and ``posted, replied'', respectively. Clearly, a delete event from q2 triggers failure. The states q0', q1', and q2' correspond to the same conditions, except that u has been promoted to the moderator role. Thus, a user u that attempts to delete the post p from the state q2' does not violates the policy.

name: mod_author_post                     
states: q0 q1 q2 q3 fail                  
start: q0                                 
final: fail                               
q0 -- post(u,*,p,*,*) --> q1              
q1 -- edit(u1,*,p) --> fail when u!=u1    
q1 -- edit(guest,*,p) --> fail            
q1 -- delete(u1,*,p) --> fail when u!=u1         
q1 -- delete(guest,*,p) --> fail          
q0 -- promote(*,u1) --> q2                
q2 -- demote(*,u1) --> q0                 
q2 -- post(u,*,p,*,*) --> q3              
q1 -- promote(*,u1) --> q3                
q3 -- demote(*,u1) --> q1                 
name: post_after_reply
states: q0 q1 q2 q0' q1' q2' fail 
start: q0
final: fail
q0  -- post(*,*,p,t,*) --> q1
q1  -- post(*,*,*,t,*) --> q2
q2  -- delete(u,*,p) --> fail when u!=admin
q0  -- promote(*,u) --> q0'
q0  -- demote(*,u) --> q0
q0' -- post(*,*,p,t,*) --> q1'
q1  -- promote(*,u) --> q1'
q1' -- demote(*,u) --> q1
q1' -- post(*,*,*,t,*) --> q2'
q2  -- promote(*,u) --> q2'
q2' -- demote(*,u) --> q2