[cap-talk] - Bellizzomi - Capabilities and Shapiro's focus, Coyotos, etc.
Karp, Alan H
alan.karp at hp.com
Wed Nov 29 10:31:43 CST 2006
> "Verifying the EROS Confinement Mechanism"
> to convince myself that Jonathan Shapiro is not addressing wall
> banging with at least EROS and likely not with Coyotos (though
> as they say 'I'm all ears' - I'd love to see a solution in that area).
> In "From EROS to Coyotos/BitC: Open Source Meets Open Proofs"
> he says:
> The Coyotos effort inherits two useful successes
> from the EROS effort:
> A verification proof that the architecture can en-
> force a security property known as "confinement."
> and ...
> but then in "Verifying the EROS Confinement Mechanism" he says:
> "In this paper, we will ignore issues of covert channels.
> While important,
> reducing such channels is of interest only when it has been
> shown that overt
> channels have been closed."
I've been waiting for MarkM to chime in on this topic, but since he
hasn't, I'll say what I think he would say.
While you can't prevent wall banging, you can prevent wall listening by
removing all forms of indeterminacy, such as access to the system clock.
Any process that is deterministically replayable meets this criterion.
Did I get that right, MarkM?
Virus Safe Computing Initiative
1501 Page Mill Road
Palo Alto, CA 94304
(650) 857-3967, fax (650) 857-7029
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Karp, Alan H.vcf
Size: 423 bytes
Desc: Karp, Alan H.vcf
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20061129/9b807145/attachment.vcf
More information about the cap-talk