Inlined Reference Monitors for Multithreaded Java: Case-Studies

This page describes the different case-studies.

At the bottom of the page you'll find the files required to try the case studies out.

A screen cast is available, demonstrating the first and second case study.

Web Banking Demo: Secure Sessions

Many (not to say most) web applications allow you to login from one network and then access the webpage from another network. Provided that the session id is kept secret, this poses no security issues. "Session hijacking" as it is called, is however a real problem. The session id can be leaked due to

This type of threat is part of item 3 (Broken Authentication and Session Management) in the OWASP Top 10 security threats. The primary counter measurement against this, is to prevent the user from changing IP adress in the middle of a session.

In this case study start with a simple banking web application that allows the user to change his IP adress. We then inline the neccessary checks to disallow this.

The Application

The application is a standard Java web application built with the Winstone Servlet Container. The application stores users in a HyperSQL database (though any JDBC-compliant DBMS would do). Users may login, transfer money and logout. The session management is based on the traditional session API provided by the Servlet API and relies on cookies. The application also provides an administration interface, based on HTTP authentication. More about that in the next case study.

The Policy

In words, the policy says

Before each request,

In ConSpec:

SCOPE Session

SECURITY STATE HashMap sessionMap = new HashMap();

BEFORE HttpServlet.service(HttpServletRequest req, HttpServletResponse resp) PERFORM
    !sessionMap.containsKey(req.getSession(true).getId()) -> {
        sessionMap.put(req.getSession(true).getId(), req.getRemoteAddr());
    sessionMap.get(req.getSession(false).getId()).equals(req.getRemoteAddr()) -> {

How to run the case study

In order to run this case study, you'll need to be able to edit your cookie information manually. If you're using Firefox, you can do this using the Web Developer plugin. Simply click Tools / Web Developer / Cookies / View Cookie Information

To try out the case study, you need two computers.
StepComputer 1Computer 2
1Download and unpack the case study files
2Go to the case study directory: cd WebBankingStudy
3Start the original version of the web app: ant -f webbankingapp.xml run_original
4Browse to http://localhost:8000/accounts. (Expected result: "Access Denied.")
5Browse to http://[ip of Computer 1]/login
6Login using for instance username alpha and password a.
7Take a note of the value of the JSESSIONID cookie (for simplicity, this is printed in the bottom of the page).
8Create (or edit) a cookie called "JSESSIONID" on localhost with the same value as the cookie on the other computer.
9Reload the http://localhost:8000/accounts page. (Expected result: The account page of the "alpha"-user.)
10Terminate the server using Ctrl-C.
11Inline the policy and start the secured version of the web app: ant -f SecureSessions.xml run_inlined
12Repeat steps 4-9. (Expected result: No access to the account page of alpha.)


A limitation in the current version of the inliner is that the only option when it comes to policy violations is to call System.exit. This doesn't make lot of sense for a webserver. A servlet container however forbids this, and the result is that a security exception is thrown.

Web Banking Demo: HTTP Authentication

The HTTP authentication is widely used mechanism for protecting administrative webpages. The security it provides, is on the level of HTTP-commands, such as GET and POST. This may however not be as fine grained as one may want.

The Application

The application in this case study is the same as the application in the secure sessions case study above. In this case study however, we will focus on the administration interface, which allows administrators to create, search for and delete account holders (i.e. regular users). The create and delete operations are done through JDBC's PreparedStatement.executeUpdate and the search is done through PreparedStatement.executeQuery.

The administration pages (URLs on the form /admin/*) are protected using the HTTP authentication mechanism. It currently uses the BASIC authentication method, but it could just as well use for instance the form-based authentication method. Here is the relevant snippet of the web.xml:

        <display-name>Administration Security Constraint</display-name>
            <web-resource-name>Protected Area</web-resource-name>

        <realm-name>Administration Area</realm-name>

The configuration allows for users in the administrator role or secretaries role to access the administration-page. Both types of users are allowed full access, that is GET, POST, DELET, PUT.

The Policy

The policy in this case, states that only users in the role administrator should be allowed to update the database. Other users (the ones in role of secretary) are only allowed to query the database.

SCOPE Session

    boolean initialized = false;
    ThreadLocal adminUrl = new ThreadLocal();
    ThreadLocal adminChecked = new ThreadLocal();

BEFORE HttpServlet.service(HttpServletRequest req, HttpServletResponse resp) PERFORM
    req.getRequestURI().startsWith("/admin") -> {
        initialized = true;
    ELSE {
        initialized = true;

AFTER boolean isInRole = WinstoneRequest.isUserInRole(String role) PERFORM
    role.equals("administrator") && isInRole -> {
    ELSE {

// Disallow arbitrary SQL-commands.
BEFORE PreparedStatement.execute() PERFORM
    false -> {

// Allow executeUpdate, only if admin is checked and true.
BEFORE PreparedStatement.executeUpdate() PERFORM
    (!initialized) ||
    adminUrl.get().equals(java/lang/Boolean.FALSE) ||
    adminChecked.get().equals(java/lang/Boolean.TRUE) -> {

How to run the case study

  1. Download and unpack the case study files
  2. Go to the case study directory: cd WebBankingStudy
  3. Start the orinigal version of the web app: ant -f webbankingapp.xml run_original
  4. Browes to http://localhost:8000/admin/accountholders.
  5. Login as administrator using admin as username and pass as password.
  6. Try adding / removing account holders.
  7. Logout (in Firefox: Tools / Clear recent history / Active Logins)
  8. Login (refresh page) as secretary using johndoe as username and john as password.
  9. Try adding removing users. (Expected result: Adding disallowed, removing accidentally allowed!)
  10. Terminate the server using Ctrl-C.
  11. Inline and start the secured version of the web app: ant -f HttpAuth.xml run_inlined
  12. Repeat steps 8-9. (Expected result: Removing accountholders as secretary not possible!)


As noted in the secure sessions case study, shutting down the server is not a desirable option here. However, this is forbidden, so the actions result in a SecurityException anyway.

Ad Applet: Restricted Browser Redirection

In this case study we look at a simple ad-banner that redirects the browser to another URL when the user clicks on it. The inliner enforces a same-origin-policy for redirections.

The Application

The application is in this case an applet embedded in a webpage. The applet redirects the browser to a new URL as the user clicks on it.

The Policy

The policy states that the URL that the applet sends the browser to, must have the same host as the document base url of the webpage that the applet is embedded in.

SCOPE Session

SECURITY STATE String origin = "";

AFTER URL docBase = Applet.getDocumentBase() PERFORM
    true -> {
        origin = docBase.getHost();

BEFORE AppletContext.showDocument(URL url, String target) PERFORM
    url.getHost().equals(origin) -> {

How to run the case study

  1. Download and unpack the case study files
  2. Go to the case study directory: cd AdAppletStudy
  3. Create a webpage with the original version of the applet: ant webpage_uninlined
  4. Set up a webserver to serve pages from AdAppletStudy/build
  5. Browse to http://localhost/uninlined/adpage.html
  6. Click on the ad. (Expected result: Browser is redirected to
  7. Create an inlined version of the applet and a new webpage: ant webpage_inlined
  8. Browse to http://localhost/inlined/adpage.html
  9. Click on the applet. (Expected behavior: Browser is not redirected.)
  10. Optional step: Modify the code so that it respects the document base: Change "" to super.getDocumentBase().getHost() and repeat steps 7-9 (Expected behavior: The redirect goes through).

JPicEdt: Swing API Usage

The Swing API is designed to be powerful, flexible and easy to use. In particular it is designed to be easy for programmers to build new Swing componetns, whether from scratch or by extending components that is provided in the API. For this reason, Swing components are not thread safe, i.e., do not allow access from different threads.

This rule may be hard to remember when writing code, and even if the programmer does remember it, it is sometimes hard to forsee all flows of a program, and whether or not some code will be executed on the event dispatch thread (EDT from now on). What's even worse is that a violation of the rule may result in random deadlocks that are hard to debug.

In this case study we monitor the Swing API usage of a large drawing program, and make sure that the relevant API methods are executed on the EDT.

The Application

The application we chose for this case study is a fairly complex (68 kloc) drawing program called JPicEdt. It is a drawing program that can save in various vectorized formats including LaTeX code.

This program turned out to be quite interesting to analyze. The original program actually violated the policy during startup. By printing the stack trace at the point of violation we managed to patch the program. The original program and the patch is included in the case study archive.

The Policy

The policy has two security states: realized and not realized. Once the EDT is created (through, Window.pack() or Window.setVisible(true)) no Swing method may be called from any other thread than the EDT.

How to run the case study

  1. Download and unpack the case study files
  2. Go to the case study directory: cd SwingStudy
  3. Run the original program: ant run_original
  4. Inline and run the inlined program: ant run_inlined (Expected behavior: Policy violation for JFrame.setDefaultCloseOperation(I).)
  5. Optional step: Apply the patch: ant patch_source and redo step 4. (Expected behavior: No policy violation.)


For more information on Swing and threads, here is an article by Hans Muller and Kathy Walrath.

The list of methods in the policy is not the complete list of non-thread safe Swing methods. To create the policy we instead searched for all Swing methods mentioned in the JPicEdt program.

According to some specifications, it is ok to create and manipulate Swing components off the EDT, if that particular component has not yet been realized. In this case study however we take a slightly more restrictive approach and require that all gui related work must take place on the EDT once any ui has been realized. Here is a quote by Josh Marinacci (former member of the Swing Team) supporting this approach:

"As a former member of the Swing Team I'm going to go ahead and say that creating UI objects (not just components) off of the EDT is a bug in your program. Until the 1.4/1.5 timeframe we said it was okay to create your UI objects off of the EDT in certain cases (main frame not initalized). This was our mistake. We should have said this because it depends on particular implementation details of Swing (the order in which things are initialized internally), and it turns out we were wrong in some cases. Therefore we now say that creating or manipulating any UI object off of the EDT is a bug. Doing so will probably work fine in 99% of the cases, but you have now introduced potential race conditions in your app that may give you strange behavior later on. One more detail, and this is important. As we work to further improve startup time of the VM and the Swing infrastructure, we will likely change the internals of Swing. This may increase the likely hood that code which used to work fine off of the GUI thread will now break. Therefore it is *very* important that you stay on the GUI thread; and that's why I say: yes, it's a bug!"

CashDesk: ABS Bytecode Constraints

This case study builds on an ABS case study from the HATS project.

The Application

The application comes from an ABS model of a cash desk system featuring bar code scanners, cash boxes, printers, inventories, banks, cashiers and customers. Since our inliner works on java bytecode level, we first compiled the ABS code into Java code. The original ABS model was implemented on 1200 lines, and the compilation resulted in 7300 lines of Java code.

The Policy

The policy in this case counts the number of active sales (+1 for newSaleStarted, and -1 for saleFinished), and asserts that the number of active sales is always greater than or equal to 0.

SCOPE Session

    int salesInProgress = 0;

AFTER CashDeskAll/CashBoxEventReceiver.newSaleStarted() PERFORM
    true -> {
        salesInProgress = salesInProgress + 1;

BEFORE CashDeskAll/CashBoxEventReceiver.saleFinished() PERFORM
    salesInProgress > 0 -> {
        salesInProgress = salesInProgress - 1;

How to run the case study

  1. Download and unpack the case study files
  2. Go to the case study directory: cd CashDescStudy
  3. Run the original application: ant run_original (Expected behavior: No events monitored.)
  4. Terminate the application using Ctrl-C.
  5. Inline and run the inlined version of the application: ant run_inlined (Expected behavior: sale started / sale finished monitored and printed on standard out.)
  6. Terminate the application using Ctrl-C.
  7. Optional step: Set the initial value of salesInProgress to 0-1. Repeat step 5 and watch it terminate on the second invokation of saleFinished.

Download Case Study Files

Download the case study files here and extract them using using tar xzf Inlining_case_studies.tar.gz.