[cap-talk] Is "Authority" Subjective?

[Jonathan S. Shapiro]

On Sun, 2007-06-24 at 10:04 -0700, David Wagner wrote:
> For instance, one could argue that the ability to perform pure computation
> is itself an authority (it consumes electricity and so has an externally
> visible effect on your electric bill, for instance; also, it uses some of
> your CPU and so has an externally visible effect on how responsive your
> machine is to remote clients).  But for the most part, for the authority
> analyses we tend to do, this is usually not the kind of authority we
> usually care about.  Therefore, we deem that kind of authority "below
> notice" and "ignorable".

I think this is incorrect -- I agree that we do not usually deal with
computation explicitly, but I think that this explanation is not the
right explanation.

One surprise -- until we thought about it -- in the SW model was that
*data* operations have no interesting semantics in the permissions
model. Other than the fact that it causes the page to be mutated, there
is no semantics to a data store operation. On reflection, it is obvious
that this should be so. It would be very unfortunate if a security model
relied on untrusted user-mode state as a requirement for correctness.

The reason that computation can be ignored in this class of model is
that its effects within the model consist entirely of state updates to
data, and these effects have no semantics.


Having said this, let me also note a serious problem with it. *Because*
we do not model state, we cannot model the effect of trusted programs or
the relationship between the model operational semantics and the program
obeyed by the application. This means that in the classical models we
cannot rely on checkable program safety properties when reasoning about
information flow. The usual workaround is to "build those programs in"
to the model.

Scott Doerrie in my lab is currently automating a variant of the SW
model. One of the changes he will be making is to add indices into the
invoke operation. This will allow us to admit analysis of trusted
programs.

shap