[cap-talk] Nondeterminism and OCap Model (was: Re: Concening entry "ambient authority" in Wikipedia)

[Toby Murray]

On Tue, 2009-06-09 at 22:12 -0700, Mark Miller wrote:
> The ocap model also does not prohibit non-determinism. Indeed, most
> systems considered to be ocap systems are non-deterministic. (Joe-E
> and the single-vat subset of E are the only exceptions I know.)

Let us define an object-capability system, then, as "deterministic" if
the behaviour of each object in the system is a deterministic function
of the messages it receives. Is that what you had in mind?

A non-deterministic object-capability system is one in which the
behaviour of at  least one object, o,  is not a deterministic function
of the messages it receives. Hence, o must have access to some source of
input besides the messages it receives. Call this input a "source of
nondeterminism".

Sources of nondeterminism are covert sources of authority. The ocap
model requires that message sending and receipt are the only overt
sources of authority. Hence, I agree that nondeterministic ocap systems
can exist. However, it is best practice to implement ocap systems in
which /all/ sources of authority (both overt and covert) come from
message sending and receipt. The local subset of E and Joe-E are
examples of this best practice.

Marcus' examples of side-channel attacks in OSes perfectly highlight the
utility of this best practice, even if it is difficult if not impossible
to achieve in an ocap OS on some kinds of hardware. 

I think ocap system designers should be aiming to design deterministic
ocap systems and that this is a principle we should be pushing for,
rather than ruling it as out of bounds of our thinking.

I would even go so far as to define a variant of the ocap model ("strong
ocap model" or something) that prohibits sources of nondeterminism,
since I firmly believe this is something we should be striving for.

> If not confidentiality or availability, what's the ocap model good
> for? Limits on authority propagation and thus support for integrity!

How can one have integrity without confidentiality -- they are duals as
far as I believe. Suppose we have a "relied upon" object that, when
analysed on the assumption that it listens (and is thus affected by)
only overt sources of input (i.e. messages received) is defensively
consistent.

Now suppose, though, that this relied upon subject is operating in a
nondeterministic ocap system and that it is actually listening on some
covert source of nondeterminism that wasn't included in the analysis and
that, in doing so, it becomes corrupted. It is now not defensively
consistent.

Hence, we get integrity only under the assumption that relied-upon
subjects never use sources of nondeterminism.

> Correct code in turn can only depend on overt causality.

Why?