[cap-talk] - Bellizzomi - Capabilities and Shapiro's focus, Coyotos, etc.
devbox at selnet.org
Wed Nov 29 14:24:15 CST 2006
On 28/11/2006, at 16.44, Jed at Webstart wrote:
>At 03:38 PM 11/28/2006, Valerio Bellizzomi wrote:
>>On 28/11/2006, at 13.49, Jed at Webstart wrote:
>> >At this point I personally think any such efforts <to block wall
>> >are likely a waste of time and effort. I believe that the only way to
>> >with wall banging (which effort is in itself likely not a good use of
>> >is to limit shared resources. I think the
>> trade-offs are clear in this area.
>>I believe limiting shared resource is one of the objectives of Shap's
>>research (read the "Debunking Linus's Latest" and "From EROS to
>>Coyotos/BitC: Open Source meets Open Proofs" papers). I think we have to
>>sit down and wait that Coyotos is ready for prime time. Meanwhile I
>>continue to learn BitC at least theorically, until I put myself in
>>condition to build the compiler (which means installing FC6 and the
>>Coyotos development tree on a new machine) and start programming.
>I believe I've read enough from the above papers and from:
>"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"
>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.
>but then in "Verifying the EROS Confinement Mechanism" he says:
>"In this paper, we will ignore issues of covert channels. While
>reducing such channels is of interest only when it has been shown that
>channels have been closed."
>Perhaps we'll hear from Jonathan if I've got the above wrong.
I don't think you've got it wrong, but the paper "Verifying the EROS
Confinement Mechanism" has been written some years before the "From EROS
to Coyotos/BitC: Open Source Meets Open Proofs" paper. At the time Shap
wrote "Verifying the EROS Confinement Mechanism", Coyotos and BitC didn't
>> >We (the capability community) have to make convincing arguments,
>> >demonstrations, etc. in this area to swing
>> people over to our position (or not...).
>>I'm not a fan of pure theoric demos,
>>I think we should start using capability systems in our daily work,
>That's what wideword, CapWiki, and many more URLs as
>capabilities are. They are in daily use and increasing. I believe
>they form the foundation for a capability based IT sharing
>>and then show that they really work very well for us. This would
>>be the better demonstration we can do.
>Given what you said above I fear you are referring to Coyotos or
Yes, I refer to Coyotos, AFAIK Coyotos and L4.sec are the most recent and
>some other OS (e.g. research) implementation. Unfortunately
>I used capability OSs to good effect for some 20 years
>(~1972 - 1992) and they really worked for us. That didn't help
>things any as after that capability systems effectively disappeared
>(e.g. KeyKOS, NLTSS, Amoeba and variants, Monash, etc., etc.).
>Perhaps you will understand why I'm not very optimistic about
>that approach. Still, I wish it success and am glad that many
>approaches are being pursued. In some ways efforts at the OS
>level and at the network level and even at the language level are
>complimentary. Unfortunately the work at the OS level seems to
>stay in the R&D/academic community where Butler Lampson's
>statement still seems to hold:
>"Capability based systems are the way of the futureand they
>always will be."
>Sure I know of many of the commercial projects and even
>products based on capabilities (e.g. going back to the
>Plessey 250), but such systems (hardware and software)
>have been and continue to be commercially insignificant.
If I remember correctly, CapROS is being developed commercially.
>I'm more hopeful for change sooner at the network level.
>Hey, I hope object/capabilities at some point become the
>next "big thing" from networks to OSs to languages. That
>would finally prove Lampson wrong. We have a ways to go
>before we're at that point.
>Please don't oversell capabilities and suggest that they can
>solve covert channel problems like wall banging. I think it's enough
>to deal with overt communication channels as Jonathan suggests.
I don't suggest that capabilities can solve covert channel problems, but I
say that some covert channel problems have at least been addressed.
>The rest is mostly details for Val - can probably be ignored by others:
>> >I consider the above a nit:
>> >1) In information technology as elsewhere, a nit (pronounced NIHT) is
>> >a small, usually unimportant imperfection in something. People who
>> >have unusually high or unreasonable standards for the quality of a
>> >thing are sometimes referred to as nitpickers.
>>It is a question of standpoints, define "unreasonable".
>Let me see if I have this straight. You want me to justify why
>I consider an issue (how/whether a user's shell lowers and/or
>raises it's authority when the user goes through various states
>of activity on a connection) a nit? Now we're talking nits on nits?
>Even I won't write that much email ;-)
You write always a lot, in any case more than me :-)
>> >>I was suggesting to make the login process strictly tied to the
>> >>kernel model of operation.
>> >I'm afraid I still don't understand what you mean by the "kernel model
>>The meaning is Atomic action kernel: setup phase -> commit point ->
>>The action phase either succeeds entirely or fails entirely, this is the
>>notion of "atomic" as Shap defines it.
>Fine. I don't see what the term "kernel" adds to the notion of an atomic
>operation, but I don't think it matters.
It is Atomic operation, ok, I added "kernel" because the Coyotos kernel
works that way.
>> >Proxying is a means to do sharing. Copying data does no "sharing"
>> >as I was describing above (shared access). I'm not sure where we're
>> >going with this thread.
>>You said copying isn't like sharing because you can't read future
>>so proxying isn't sharing.
>No, I don't agree. Proxying is a type of sharing. A copy happens
>once. A proxy happens for some extended time.
>>I agree, but now you say that proxying is a
>>means to do sharing, you need to pick a consistent position here.
>The above sounds like mostly email flap to me. However, I do say
>that proxying is sharing. It allows future access - through the proxy.
>That's what sharing access to a resource is.
I thought we were talking about proxying by mail, which is usually done
More information about the cap-talk