[cap-talk] Re: [e-lang] Introducing Emily, "...capabilities are useless too..."

[David Wagner]

Constantine Plotnikov writes:
>Lets make a contrived example:
>1. There is component  A that listen to network commands.
>2. There is a component B that can launch ballistic missiles.
>3. The component B is not reachable from component A using pointers.
>
>By analysis of capability graph we might conclude that component A 
>cannot invoke any function of component B using capability invocations.
>
>However if authors of component A and component B are in conspiracy, it 
>might be still possible to give a command by network to launch ballistic 
>missile using covert channels.

Component B could launch its missiles entirely on its own, even in the
absence of A.  So an upper bound analysis would still conclude that the
missiles can be launched.  If your security goal was "missiles cannot be
launched", my style of reasoning would deduce that this goal is violated.

As for whether it is A or B who "caused" the missile to be launched,
the kind of upper bound analysis I described is indeed not helpful for
assigning blame between these two colluding attackers.  That doesn't make
upper bound reasoning useless in all cases, though.  I think it is still
useful for building secure systems, where one can apply informal reasoning
to convince oneself that the system meets certain security goals.

Let me put it another way.  For certain kinds of security goals ("the
missiles are never launched"; "the missiles are only launched if a human
clicks OK"), my kind of upper bounds analysis makes it possible to build
systems where we can verify that the security goals are met.  There may
be other kinds of security goals where this upper bound analysis is too
coarse or otherwise doesn't help.

>I interpret the text  as the following:
>
>/We should not bother plugging exception data leak hole because it does 
>not gives meaningful guarantees about data leaks. We can leak data 
>anyway using covert channels./

Yes.  Thank you, that is a cleaner re-statement of my position.

>If we apply the same logic to capabilites, we should not bother with 
>them too, because using just them we cannot make guarantees about 
>de-facto authority graph.

I don't think the analogy holds.  Reasoning about the capability
graph does have some uses (despite the fact that it isn't useful for
"allocating the blame" between two conspiring attackers -- if that notion
is even meaningful).

I expect the capability graph to be particularly useful for the following
kind of reasoning task.  Suppose we have divided the system into two
pieces, X and "everything else", and we are trying to establish some kind
of security perimeter between the two.  Look at the interface between the
two.  Assuming that "everything else" can behave arbitrarily maliciously
(don't bother examining the code of "everything else"; just assume that
it can call any available interfaces that cross that perimeter), analyze
the code of X to see what security guarantees X is able to maintain.
This is a kind of modular analysis, because it only involves looking at
the source code of X and the interfaces that X has to the rest of the
world, but not at the source code of anything else in the system.

Note that in a real system, we would probably apply modular reasoning
to every component of the system.  For each component X of the system,
apply the above reasoning to see what we can say about each component.
Then reason about their composition.  This is related to the
"assume-guarantee" proof methodology.