[e-lang] Security and Vulnerability Assessment of an E Program

Toby Murray toby.murray at comlab.ox.ac.uk
Tue Aug 26 12:38:04 CDT 2008

On Tue, 2008-08-26 at 10:49 -0500, Jimmy Wylie Jr. wrote:
> I am having problems with is proving that the program is secure.
>   How do I conduct some sort of security assessment of the program?

In order to do this, you first need to define what you mean by "secure".
What is is you want to prove?

The answer here is probably dependent on what the purpose of the program

For example, an obvious property to show for the CapDesk desktop shell
(which was constructed in E as part of the DarpaBrowser project, I
believe) is that it enforces the property that "The CapEdit program
cannot write to any file other than that which the user currently has
open". This property is useful to show because of CapDesk's
function/purpose as a POLA desktop shell. (There are many, many others
that would also be interesting to show for CapDesk, of course.)

Any such proof is necessarily dependent on the assumption that E
correctly implements its intended semantics. Before worrying about this
assumption, however, I would first try to articulate what it is you want
to prove.

Having done so, you then need to work out to what level of detail you
want to prove each property. There are, currently, two ends of the
spectrum at which you can work. At one end is (1) "in/semi-formal
analysis of the real code" while at the other is (2) "formal analysis of
a [crude] model of the code". Both ends of the spectrum rely on the
assumption that the runtime (e.g. E language implementation, etc.)
correctly enforces its intended semantics.

(1) "informal / semi-formal analysis of the real code"

For example, many informal arguments have been made about the security
of many object-capability programs. A great example is the analysis that
Marc Stiegler performs on the Sash powerbox shell during his Google
TechTalk "From Desktops to Donuts".

This is a good place to start to get a feel for the sort of informal
arguments that one would want to formalise in order to more rigorously
prove such a property.

Other proofs have been more formal again. For example, the Joe-E project
(to create an object-capability subset of Java) has done some good work
on semi-formal proofs of properties like functional purity, again
predicated on the assumption that Joe-E implements its intended
semantics correctly. (see
http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf ).

Less formal "proofs" and arguments have been made about properties
enforced by other Joe-E code, such as the recent discussion about the
JSONSerializer code that is part of the Waterken server (see e.g.
http://www.eros-os.org/pipermail/e-lang/2008-August/012821.html ).

(2) "formal analysis of a model of the code"

This involves modelling your object-capability program and using a
model-checker to formally prove the security properties of the model,
with a hope that they translate back to the original program. In
building the model, you incorporate the assumptions of object-capability
semantics etc. Fred Spiessens' has done some good work in this area, and
I've been trying to make some progress here as well using the CSP
process algebra and its model checker, FDR (see e.g.
http://web.comlab.ox.ac.uk/people/toby.murray/papers/AOCS.pdf ). 

I hope others on this list have better answers here, as this is a topic
that I'm also heavily interested in.



More information about the e-lang mailing list