This page describes the different case-studies.
A screen cast is available, demonstrating the first and second case study.
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
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 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.
In words, the policy says
Before each request,
- If there is no IP associated with the session id, then associate the session id with the IP address
- If there is an IP associated with the session id, require that the current IP matches the associated IP
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()) -> {
}
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.
| Step | Computer 1 | Computer 2 | |
|---|---|---|---|
| 1 | Download and unpack the case study files | ||
| 2 | Go to the case study directory: cd WebBankingStudy | ||
| 3 | Start the original version of the web app: ant -f webbankingapp.xml run_original | ||
| 4 | Browse to http://localhost:8000/accounts. (Expected result: "Access Denied.") | ||
| 5 | Browse to http://[ip of Computer 1]/login | ||
| 6 | Login using for instance username alpha and password a. | ||
| 7 | Take a note of the value of the JSESSIONID cookie (for simplicity, this is printed in the bottom of the page). | ||
| 8 | Create (or edit) a cookie called "JSESSIONID" on localhost with the same value as the cookie on the other computer. | ||
| 9 | Reload the http://localhost:8000/accounts page. (Expected result: The account page of the "alpha"-user.) | ||
| 10 | Terminate the server using Ctrl-C. | ||
| 11 | Inline the policy and start the secured version of the web app: ant -f SecureSessions.xml run_inlined | ||
| 12 | Repeat 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.
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 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:
<security-role>
<role-name>administrator</role-name>
</security-role>
<security-role>
<role-name>secretary</role-name>
</security-role>
<security-constraint>
<display-name>Administration Security Constraint</display-name>
<web-resource-collection>
<web-resource-name>Protected Area</web-resource-name>
<url-pattern>/admin/*</url-pattern>
<http-method>DELETE</http-method>
<http-method>GET</http-method>
<http-method>POST</http-method>
<http-method>PUT</http-method>
</web-resource-collection>
<auth-constraint>
<role-name>administrator</role-name>
<role-name>secretary</role-name>
</auth-constraint>
</security-constraint>
<login-config>
<auth-method>BASIC</auth-method>
<realm-name>Administration Area</realm-name>
</login-config>
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 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
SECURITY STATE
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;
adminUrl.set(Boolean.TRUE);
adminChecked.set(Boolean.FALSE);
}
ELSE {
initialized = true;
adminUrl.set(Boolean.FALSE);
}
AFTER boolean isInRole = WinstoneRequest.isUserInRole(String role) PERFORM
role.equals("administrator") && isInRole -> {
adminChecked.set(Boolean.TRUE);
}
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) -> {
}
cd WebBankingStudyant -f webbankingapp.xml run_originaladmin as username and pass as password.johndoe as username and john as password.Ctrl-C.ant -f HttpAuth.xml run_inlinedAs 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.
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 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 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) -> {
}
cd AdAppletStudyant webpage_uninlined
AdAppletStudy/buildhttp://thedarkknight.warnerbros.com/dvdsite/index.htmlant webpage_inlined"thedarkknight.warnerbros.com" to super.getDocumentBase().getHost() and repeat steps 7-9 (Expected behavior: The redirect goes through).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 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 has two security states: realized and not realized. Once the EDT is created (through Window.show(), Window.pack() or Window.setVisible(true)) no Swing method may be called from any other thread than the EDT.
cd SwingStudyant run_originalant run_inlined (Expected behavior: Policy violation for JFrame.setDefaultCloseOperation(I).)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!"
This case study builds on an ABS case study from the HATS project.
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 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
SECURITY STATE
int salesInProgress = 0;
AFTER CashDeskAll/CashBoxEventReceiver.newSaleStarted() PERFORM
true -> {
salesInProgress = salesInProgress + 1;
}
BEFORE CashDeskAll/CashBoxEventReceiver.saleFinished() PERFORM
salesInProgress > 0 -> {
salesInProgress = salesInProgress - 1;
}
cd CashDescStudyant run_original (Expected behavior: No events monitored.)Ctrl-C.ant run_inlined (Expected behavior: sale started / sale finished monitored and printed on standard out.)Ctrl-C.salesInProgress to 0-1. Repeat step 5 and watch it terminate on the second invokation of saleFinished.Download the case study files here and extract them using using tar xzf Inlining_case_studies.tar.gz.