[cap-talk] Capabilities and Freedom vs. Safety

[Toby Murray]

On Thu, 2007-07-26 at 12:39 -0400, Jonathan S. Shapiro wrote:
> On Thu, 2007-07-26 at 16:39 +0100, Toby Murray wrote:
> 
> > This of course depends on one's definition of "adequate". However, my
> > definition of adequate includes the ability to discover when
> > (subject/object) Alice has the authority to invoke Bob but can't acquire
> > the permission to do so. This requires (counterfactual) causal reasoning
> > in order to make this determination. (I know you know, but for the
> > benefit of anyone else reading) we've discussed this somewhat recently
> > on the list. My own work with CSP is trying to do exactly this.
> 
> Toby:
> 
> Just to confirm that I understand you, your goal here is to reduce the
> degree of conservatism that is inherent in equating statically
> determined authority with feasible actions, yes?

I'm trying to fix the problem inherent with equating (an upper bound
for) authority with acquirable permissions. Acquirable permissions are
NOT a conservative estimate for authority. They are an underestimate.
The confused deputy example shows this. 

A user that has permission  to invoke a compiler and cause that compiler
to overwrite the billing log has authority to overwrite the log but not
permission. Hence, reasoning about acquirable permissions doesn't tell
you that the logfile can be overwritten -- you've underestimate the
user's  authority, not overestimated it.

This demonstrates that analyses for the safety problem provide inherent
underestimate of a subject's authority. This is what I want to overcome.

> 
> I can see that CSP might be appropriate here, but I am curious about
> something. It seems to me that no analysis of the form you contemplate
> is feasible without reasoning about program behavior.

Precisely. We model program behaviour in CSP.

>  One can simplify
> the problem by reasoning about a *model* of the program (that is: about
> an alleged program).

The more trusted the program is, the more precise your model can be. The
less trusted the program  is, the more behaviours the model must
exhibit. Exhibiting multiple behaviours is achieved through the use of
nondeterminism when modelling the programs in CSP.