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

[Constantine Plotnikov]

David Wagner wrote:

>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.
>  
>
Security goal was to ensure that there is no back door that allows to 
launch missiles by giving command using network. There might be 
additional security goals during security audit. The sample shows that 
no audit that takes into account only local properties of the object can 
make sure that system is secure from certain kinds of attack.

You remove a critical component from the statement and as result 
receives some strange results. If upper case analysis is used, we have 
just to conclude that everything is possible until we have reviewed 
every line of the code. Capability graph is not generally equal to 
authority graph due to covert channels. And if want to check properties 
of authority graph, we should not limit itself to capability graph analysis.

>>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).
>
>  
>
Lets get back to you two doors analogy. Why we should be bother close 
one door (using capabilities) if leave other door (covert authority 
channels) open?

So reformulating your statement about exceptions/data to 
capabilities/authority:
/We should not bother plugging authority leaks [using capabilities], 
because it does not give meaningful guarantees about authority leaks. We 
can leak authority anyway using covert channels./

The statements has the same logical structure and talking about the same 
thing, so to be consistent one should accept or reject both IMO.

Reasoning about data flow in the program also has some usages for 
security guarantees. All covert channels are flows of data that bypass 
capabilities after all. If we add additional overt channel to the 
system, we will just make security analysis more difficult.

>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.
>  
>
I'm not denying usefulness of capabilities for security analysis. I'm 
arguing that data flow analysis over overt channels is essential for 
security analysis too. Like capabilities allows us to reason about local 
authority flow, exception guards and value guards allow us to reason 
about local data flow (note that if we use "union" interpretation of 
exceptions than exception guards are just kinds of value guards that 
checks the failure case of union). In the end, we can reason about data 
and authority flow in larger system using results from local analysis. 
And we will need both parts of analysis to understand global properties 
of the system.

Constantine