[cap-talk] Reinterpreting POLA - "Authority Must Not Exceed Trust"

[Toby Murray]

On Tue, 2007-09-18 at 13:42 -0700, David Wagner wrote:
> Toby Murray writes:
> >Indeed. In either case, however, the user would be unhappy were the
> >mailer to have the (behaviour and) ability to insert "not" into the
> >user's message or otherwise corrupt its meaning. When analysing a model
> >of the mailer, what I care about, then, is whether the behaviour
> >represented by the model allows the mailer to acquire authority that
> >exceeds that which the user is willing to trust it with -- i.e. whether
> >in the model (which is assumed to capture all possible behaviours of the
> >relevant mailer) the mailer can perform or cause the user's message to
> >be corrupted.
> 
> Got it.  Now I understand where you are going.  It makes sense.
> 
> Your final (nicely worded) paragraph illustrates a confusion of my own.
> You point out the distinction between ability and behavior.  The ability
> of the mailer is independent of its code and is determined by things like
> what capabilities it is provided with, what restrictions the underlying
> platform or OS enforce, and the behavior of other entities that it
> interacts with.  The behavior of the mailer depends on the code of the
> mailer as well as on its ability.  When we talk about the authority that
> the mailer has, do we mean to take its behavior into account, or only
> its ability?  I am used to thinking about the authority of an entity
> only in terms of that entity's ability, not its behavior.

Good question.

There is a very real distinction between "potential" authority and
"actual" authority. Potential authority should always be a superset of
actual authority. 

One can compute potential authority of an object by making no
assumptions about its behaviour and, therefore, modelling the object to
exhibit all legal possible behaviours.

Often, I think the choice of whether to try to model potential or real
behaviour (which will lead to computing potential or real authority,
respectively) will be based on how much one knows about the software
they are modelling.

Suppose we had some magical means to produce CSP models from real code,
such that the model produced was guaranteed to exhibit all possible
behaviours of the code. Suppose further we have some abstraction that
has been coded and we want to reason about its properties. We can derive
the (accurate) CSP model from the code and then reason about the actual
authority of internal entities that make up the abstraction.

But now suppose we want to know how that abstraction affects the
authority of the objects, o,p,q,... with which it is composed. Then the
correct thing to do, imo, is to model o,p,q so as to exhibit all
possible legal behaviours, within the constraints of the model and the
behaviour of the abstraction. Now we're reasoning about potential
authority.

Hence, I see that both have their uses.