[cap-talk] Capability modelling tools

[Thomas Leonard]

On 26 April 2011 20:25, Ankur Taly <ankur.taly at gmail.com> wrote:
> 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)'

That certainly sounds a lot like what I did, except I used a separate
rule for each assignment. e.g. "x = y" becomes this (assuming x and y
are local/stack variables):

  local(?Object, ?Context, "x", ?Value) :- local(?Object, ?Context,
"y", ?Value).

(?Context makes it possible to consider different groups of calls
separately, such as "all calls by A" or "all calls passing B", as
necessary for the proof).

I don't know enough about the implementation details of Datalog to
know which way is more efficient.

> 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.

That would be interesting. I'd like to see how to model my factory
case using it.

> 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/