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

[Mark Miller]

On Wed, Jun 10, 2009 at 2:09 AM, Toby Murray <toby.murray at comlab.ox.ac.uk>wrote:

> 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?
>

No. Think Actors. Even if each object is individual object is deterministic
in your sense, if Alice and Bob are both sending messages to Carol, and if
the arrival order with which these messages are delivered to Carol is
non-deterministic, then even if Alice, Bob, and Carol are each individually
deterministic, the system composed if the three of them are not.


>
> 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".
>

That's fine. Works as well for arrival order non-determinism.


>
> Sources of nondeterminism are covert sources of authority.


They are covert sources of information but not authority. I was mostly[1]
careful about this:

>From section 8.1

> When Alice and Bob arrange this relying only on the “legal” overt rules of
>> the system, we
>> say Alice is providing Bob with an indirect access right to write
>> /etc/passwd, that she is
>> acting as his proxy, and that Bob thereby has authority to write it.
>>
>
> One can derive a bound on possible overt causal-
>> ity by reasoning only from the current topology of permissions. This
>> corresponds to Bishop
>> and Snyder’s “potential de facto analysis” [BS79], and gives us a
>> topology-only bound on
>> authority (TA).
>>
>
If authority included covert causality, then it would not be bounded by the
topology of permissions.

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.
>

As Hewitt (cc'ed) pointed out a long time ago (perhaps first in "Challenge
of Open Systems" in Byte?), in distributed systems, arrival order
non-determinism is an irreducible source of non-determinism. When a bank
receives a withdraw request, it cannot wait forever to see if any deposit
requests would have arrived "earlier" according to some deterministic
account.


>
> 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.
>

If the potentially listening process is denied access to a clock and is
constrained to operate in a locally deterministic manner, then it doesn't
much matter what timing side channels the hardware leaks. These other
constraints could be enforced either at the OS level or language level,
again with no special help from the hardware. However, it has a terrible
cost on schedulability -- only timing insensitive processes can be
co-scheduled on the same CPU or cache as a secret bearing process. I am not
suggesting this is yet a practical suggestion.


>
> 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.
>

To the degree practical, I quite agree. But it's good to keep separable
issues separate. The ocap *model* makes no such demands.


> 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.
>

The term used in "Verifiable Functional Purity in
Java<http://www.cs.berkeley.edu/%7Edaw/papers/pure-ccs08.pdf>"
is "deterministic object-capability system". I like that.

>
> > 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.


Yes, they are some weird kind of duals. However, as we go through the
looking glass, we must be careful to reverse everything that needs reversal
to get the duality right.

Here's a gedanken experiment demonstrating that one can have integrity
without confidentiality. Start with, say, KeyKOS. Now add a user mode
instruction to the hardware that lets any process read any word of physical
memory by physical memory address. Also provide instructions for reading the
state of the MMU and any other relevant hardware registers that can be read
without causing effects.

I hereby coin the term "fully transparent capability system" for the result.
In this system, it is not *possible* for any subjects to keep any secrets
from any other subject. In some real sense, cryptography is not possible on
this platform. However, because KeyKOS's protection rely only on
unforgeability, not unguessability, it does not weaken any of KeyKOS's
integrity properties in the slightest.



> 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.
>

This is not adequate for defensive consistency.


>
> 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.
>


Section 5.5:

> a program P is defensively correct if it continues to provide correct
>> behavior to well behaved
>> clients despite arbitrary behavior on the part of its other clients.
>>
>
Section 5.6:

> Given that all the objects it relies on themselves remain consistent, a
>> defensively consistent
>> ob ject will never give incorrect service to well-behaved clients, but it
>> may be prevented from
>> giving them any service. While a defensively correct object is
>> invulnerable to its clients, a
>> defensively consistent object is merely incorruptible by its clients.
>>
>
(This difference between defensive correctness vs defensive consistency
affects only availability and is orthogonal to issues of confidentiality.
The point is what they have in common.)


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

>
Why
>

By definition. To enable modular reasoning, the correctness of correct
program P may rely only on the specified properties of the abstractions in
its reliance set. To depend on covert causality *for one's correctness*
means that one's correctness depends on unspecified incidental properties of
an implementation. If P's correctness depends on covertly received
information, then the implementations of abstractions in its reliance set
can be changed in ways that do not violate their specification but
nevertheless break P. For example, say P has a race condition bug that
happens never to get hit by the current scheduling policy. If the scheduler
changes in ways allowed within its specification, P would break. Even if the
scheduler is never actually changed in this way, this possibility means that
P is already incorrect.

[1] There are in fact some places in the thesis, such as the rest of section
5.5, where I say "authority" while meaning to include some covert effects.
Oops.

-- 
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20090610/9682e0de/attachment.html