[cap-talk] Concening entry "ambient authority" in Wikipedia

[Mark Miller]

On Tue, Jun 9, 2009 at 7:51 PM, David-Sarah Hopwood<
david-sarah at jacaranda.org> wrote:
> No, just a mistake. You are quite correct, access to load/store
instructions
> *can* sometimes lead to a devastating leakage of authority via side
> channels.
>
> It is important to distinguish, however, between an system that was
intended
> to be an obj-cap system but is subject to a side channel attack, and a
> system that was never intended to be an obj-cap system in the first place.
> Traditional Unix is in the latter category.
>
> The distiction is important because the side-channel attack in the obj-cap
> system is potentially fixable, *or* is grounds for considering the system
to
> be broken relative to its security goals.


The ocap model is not defined by its security goals. It is defined by its
formal properties. Any system which has these formal properties is an ocap
system. Unix and Java aren't, and neither is Unix with Chroot, for reason
already explained. A given system may be designed according to the ocap
model, and may be designed to satisfy some security goals. Some of these
goals may be satisfied or satisfiable simply because of the system's
adherence to the ocap model. For other goals, a given ocap system may
satisfy these goals for reasons outside the properties of the ocap model.

Footnote 1 Chapter 8 of <http://erights.org/talks/thesis/index.html> says:

> Semantic models, specifications, and correct programs deal only in overt
> causation. Since this disser-
> tation examines only models, not implementations, we ignore covert and side
> channels. In this dissertation,
> except where noted, the “overt” qualifier should be assumed.
>

This is too glib but its implication is correct. The ocap model deals only
in overt causality. 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.)
Together, this means that the ocap model alone provides no protection
whatsoever against non-overt (covert and side) channels. A given system may
be designed to provide some assurances about the absence of such channels.
For example, KeyKOS attempts to limit, but not prevent, non-overt outward
communication only. The deterministic subset of E can prevent non-overt
inward communications only, and only under rarely-realistic conditions. In
both cases, these assurances derive from properties of these systems beyond
their adherence to the ocap model. To reason about KeyKOS's resistance to
non-overt communication, one must reason non-modularly about the
implementation. No one knows how to write a practical specification that
would enable modular reasoning about these issues in a similar system.

The original formal expression of approximately[1] the ocap model is the
locality laws of Hewitt & Baker's "Actors and Continuous
Functionals<http://www.lcs.mit.edu/publications/specpub.php?id=762>".
Though it speculates
<http://erights.org/history/actors.html#locality-laws>on using the
locality laws to solve Lampson's confinement problem, because
the actor model is pervasively non-deterministic, it can only solve the
overt subset of Lampson's problem.

So the ocap model by itself doesn't enable us to reason about
confidentiality. Because the ocap model only specifies what actions must
eventually happen, without being able to place any bounds or even talk about
how long the delay is until these thins happen, the ocap model by itself
also doesn't enable us to reason about availability (beyond a vacuous
"eventually" claim). Likewise for the Actor model. KeyKOS and its
descendants all give us quite strong availability guarantees, but again
because of properties of KeyKOS beyond their adherence to the ocap model. In
this case, I believe one can reason about KeyKOS availability in modular
fashion based on a practically writable specification.

If not confidentiality or availability, what's the ocap model good for?
Limits on authority propagation and thus support for integrity! As Fred
Spiessens points out <http://www.evoluware.eu/fsp_thesis.pdf>, integrity
only depends on relied-upon code engaging in less causality than it is
permitted to do. Modular reasoning about relied-upon code depends on that
code being correct. Correct code in turn can only depend on overt causality.
The confinement properties that can be modularly derived in terms of only
the ocap model is overt-only confinement. This is a sound for reasoning
about integrity but not confidentiality.

[1] The Actor locality laws leave out precisely the elements left out of
Paradigm Regained but explained (badly) in Chapter 10 of my thesis. As a
result, the Actor model by itself also cannot explain why Java and Unix are
not ocap systems. They can be modeled so as to obey the locality laws.

-- 
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/20090609/a8fbfd1a/attachment.html