Re: New paper: Fine-Grained Privilege Separation for Web Applications

Toby Murray  wrote:
>One question struck me while reading the following  (from the "Session
>Initialisation" part of the Section 5.1.1) that the paper doesn't
>appear to address.
>"We reviewed the application's session initialisation code and
>confirmed that it doesn't use unsafe Java features to violate the
>isolation properties that Joe-E guarantees ..."
>
>How much more difficult would this step be for user's unfamiliar with
>the design of Joe-E ?

Hmm!  Good question.  I'm not sure.  Maybe Adrian or Akshay
have some thoughts on this.

If you want to try reviewing the relevant session initialization
code for yourself, you can take a look.  It's here:
  http://code.google.com/p/joe-e/source/browse/trunk/apps/servlet/src/org/joe_e/servlet/mail/notjoe_e/SessionInit.java
  http://code.google.com/p/joe-e/source/browse/trunk/apps/servlet/src/org/joe_e/servlet/mail/notjoe_e/PostfixClient.java
  http://code.google.com/p/joe-e/source/browse/trunk/apps/servlet/src/org/joe_e/servlet/mail/notjoe_e/TransportAgent.java

Tyler's Waterken is a more sophisticated example of an app that mixes
Java and Joe-E code.  I don't know if Tyler has any experience to share
on what you have to review about the Java code to know that mixing it
with Joe-E code doesn't negate all the good properties of Joe-E.

>Is there a set of simple rules that users can follow when writing Java
>code that sits alongside a Joe-E application to ensure that the Joe-E
>semantics are maintained for the Joe-E part of that application? This
>seems like something that would be required in order to make this step
>of the security review easy for end users.

My rough intuition says: the typical case is that the Java code ought
to be valid Joe-E, with the one exception that it might construct
capabilities out of thin air by using untamed Java APIs (which is
something Joe-E code isn't supposed to do).  So maybe one could eyeball
those files to make sure that this is the only way that it violates
Joe-E rules.  I don't know if this is exactly the right set of rules
to use, and I don't have a lot of experience with this.

I wonder if one could run the Joe-E verifier on those files, note all
violations of the Joe-E rules, and then check that those violations
are intended and necessary for functioning of the app.

In my mind the use of Java files together with Joe-E is a definite
hazard and a source of risk, and reviewing those Java files seems likely
to be tricky and potentially error-prone, particularly if there is a
non-trivial amount of Java.

>Of course, such a guide is likely to be useful for all Joe-E
>applications, so maybe it already exists? Apologies if it's just my
>ignorance.

As far as I know this does not already exist.  Unfortunately there is
very little in the way of documentation for Joe-E, I'm afraid, beyond
the spec, the published papers, and some Javadoc.