[cap-talk] Capability modelling tools

[Ankur Taly]

Hi Thomas,

I along with Mark Miller, Jasvir Nagra and Ulfar Erlingsson worked on a tool
ENCAP for
automatically verifying confinement properties of JavaScript(JS) APIs. From
your
description it seems that ENCAP may be useful to you.

The problem we were solving is as follows: We are given the implementation
of a trusted
JS API (think of this as a bunch of function written in JS) and a set of
security critical objects
(think of this as certain object creation sites in the code marked as
critical).
This API is handed over to the untrusted code via a loader and the goal is
to verify
that no legitimate invocation of the API by the untrusted code can ever lead
to a
an object created at a critical site. The untrusted code initially only
holds
the API function objects, it invoke them in various ways to obtain new
objects.

Our tool ENCAP directly works on the implementation of the API. The tool is
SOUND (no false negatives)
for all APIs written in the SES_light subset of the ES5-strict language.
The language is approximately the strict mode - setters/getters of the 5th
edition of the JS standard.

We verify confinement by encoding the API as a set of facts in Datalog.
For example the statement x = y is encoded as Assign(x,y)
The semantics of the language is modeled as set  of Horn Clauses.
For example the semantics of assignment are 'Stack(x,l) :- Stack(y,l),
Assign(x,y)'

ALL possible API invocations are encoded as follows: The untrusted code
initially owns
a set of objects which are the API functions. It then recursively traverses
all the fields of
all objects and collects all objects obtained along the way. All the
function objects
obtained along the way are invoked with all possible objects from the set as
arguments,
and the return values are collected and so on. In some sense this is the
authority-closure
of the API objects. Fortunately this can be described by small number of
Datalog horn clauses.
As an example : UntrustedReach(m) :- UntrustedReach(l), Heap(l,f,m).

The above approach can soundly handle functions calls, higher order
functions,
try-catch-finally statement and side effects. The analysis is flow context
insensitive and
is therefore not free of false positives, but it terminates in polynomial
time.
You can  take a look at the associated paper for all the the technical
details:

http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf

If you want to play with the tool then I can send that to you as well.
The description in the paper with JavaScript oriented but the main technique
should be applicable to other languages as well.

Best Regards,
Ankur.

On Tue, Apr 26, 2011 at 2:17 AM, Thomas Leonard <talex5 at gmail.com> wrote:

> Hi all,
>
> I'm doing a bit of modelling work at the moment, looking to see how
> capabilities may propagate through a system, and the effects of
> various components being compromised, etc. I found the Scollar and
> Authodox tools for this, but they didn't quite fit what I wanted to
> do.
>
> As a simple example, we have a lot of factory objects with multiple
> clients. We'd like to be able to prove things such as:
>
>        "If a client, A, creates a new object using the factory, then no-one
> else (including other clients of the factory) can get access to it".
>
> The basic strategy seems simple enough:
>
> 1. Aggregate all new objects created in the real system for client A
> as "objectsForA" and all others as "objectsForOthers" in the model.
> 2. Have the factory return objectsForA when invoked by A, and
> objectsForOthers otherwise.
> 3. Show that no-one except A gets a reference to objectsForA in the model.
>
> This is a bit tricky in Scoll, because the behaviour you define for
> objects is supposed to correspond to the actual implementation, and
> therefore can't do things the real code can't (such as returning a
> different object depending on who called it, since the real code
> wouldn't know who called it).
>
> Authodox does allow code to behave differently depending on who called
> it, but translating real code into CSP with the aggregation rules
> mixed in looks hard, and
> modelling re-entrancy looked hard too.
>
> In the end, I wrote a little modeller of my own. It's similar to
> Scollar in many ways, but it also models "invocations" (not just
> objects). An invocation is a particular call to a method, representing
> the stack-frame that is created and the local variables of this stack
> frame. You can then (separately) specify how the real invocations are
> to be aggregated.
>
> For example, you can say that all invocations of the factory by A
> should be grouped into "callsFromA" and all others into
> "callsFromOthers". As long as the factory doesn't store the reference
> to the new object in a field, the system can then prove the goal
> above.
>
> It also allows you to specify the behaviour of the objects using a
> (very simple) Java-like syntax, which I find easier than using logic
> rules to express behaviour, and when a goal fails it prints a simple
> proof explaining why.
>
> Does this sound like a sensible approach? I've put up an initial
> release with a tutorial here if anyone wants to take a look:
>
>  http://www.serscis.eu/releases/docs/sam-0.1/
>
> It currently only runs on Linux, but hopefully Windows will be
> supported in the next release.
>
>
> --
> Dr Thomas Leonard
> IT Innovation Centre
> Gamma House, Enterprise Road,
> Southampton SO16 7NS, UK
>
>
> tel: +44 23 8059 8866
>
> mailto:tal at it-innovation.soton.ac.uk
> http://www.it-innovation.soton.ac.uk/
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20110426/a573472b/attachment.html