On Tue, Jun 9, 2009 at 7:51 PM, David-Sarah Hopwood<<a href="mailto:david-sarah@jacaranda.org">david-sarah@jacaranda.org</a>> wrote:<br>> No, just a mistake. You are quite correct, access to load/store instructions<br>
> *can* sometimes lead to a devastating leakage of authority via side<br>> channels.<br>><br>> It is important to distinguish, however, between an system that was intended<br>> to be an obj-cap system but is subject to a side channel attack, and a<br>
> system that was never intended to be an obj-cap system in the first place.<br>> Traditional Unix is in the latter category.<br>><br>> The distiction is important because the side-channel attack in the obj-cap<br>
> system is potentially fixable, *or* is grounds for considering the system to<br>> be broken relative to its security goals.<br><br><br>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.<br>
<br>Footnote 1 Chapter 8 of <<a href="http://erights.org/talks/thesis/index.html">http://erights.org/talks/thesis/index.html</a>> says:<br><blockquote style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;" class="gmail_quote">
Semantic models, specifications, and correct programs deal only in overt causation. Since this disser- <br>tation examines only models, not implementations, we ignore covert and side channels. In this dissertation, <br>except where noted, the “overt” qualifier should be assumed.<br>
</blockquote><br>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.<br>
<br>The original formal expression of approximately[1] the ocap model is the locality laws of Hewitt & Baker's "<a href="http://www.lcs.mit.edu/publications/specpub.php?id=762">Actors
and Continuous Functionals</a>". Though it <a href="http://erights.org/history/actors.html#locality-laws">speculates</a>
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.<br><br>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.<br>
<br>If not confidentiality or availability, what's the ocap model good for? Limits on authority propagation and thus support for integrity! As Fred Spiessens <a href="http://www.evoluware.eu/fsp_thesis.pdf">points out</a>, 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.<br>
<br>[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.<br>
<br>-- <br>Text by me above is hereby placed in the public domain<br><br> Cheers,<br> --MarkM<br><br><br>