Re: How to add confinement to the Hurd?

[Marcus Brinkmann]

At Sun, 30 Apr 2006 21:52:18 -0400,
"Jonathan S. Shapiro" <address@hidden> wrote:
> 
> On Mon, 2006-05-01 at 03:05 +0200, Marcus Brinkmann wrote:
> > At Sun, 30 Apr 2006 19:56:05 -0400,
> > "Jonathan S. Shapiro" <address@hidden> wrote:
> 
> > > We will certainly work to find one. But if we
> > > *fail* to find one, this is an insufficient reason to reject such a
> > > foundational mechanism.
> > 
> > You are omitting the other half of my argument, where I said that I
> > have good reasons to belief that inclusion of this feature is harmful
> > (based on the use cases that _do_ exist), and that in fact there is
> > reason to belief that it has properties which make it intrinsically
> > unfit for a free software operating system.
> 
> Yes. You have said this repeatedly. Unfortunately, you have not clearly
> *stated* what your reason is, or even sketched it. You have instead said
> again and again that you wish to wait.
>
> This leaves me in the uncomfortable position that you are saying "trust
> me -- I will tell you later" on a decision that is very fundamental.

Given the fact that we have discussed this issue for months now (it
first cropped up in the oct/nov threads), and there has not been a
*single* convincing, specific use case proposed that is relevant to
the Hurd, I think you are exaggerating your case.  I do not believe
that this issue is of fundamental nature to the Hurd.  I do believe
that other issues are of fundamental nature, for example debugging and
reverse engineering (including reverse engineering of proprietary
software).

It's time to put up the facts what we are talking about.  The abstract
discussion doesn't cut it.  If this feature is so important, why
hasn't there been a list of motivating use cases that are relevant to
the Hurd?

> > > Even if other mechanisms can apparently achieve
> > > similar results, those other mechanisms will not have the strength of
> > > formal foundations that the confinement mechanism already has today. We
> > > will be unable to reason about the correctness of those systems --
> > > merely to get back to where we stand today with confinement in this
> > > regard will be more than a decade of work.
> > 
> > This is not true.  Because the trivial confinement property still
> > holds true, you can still apply the same tools of reasons that you can
> > in the EROS system.
> 
> Marcus: this is simply not correct. There is no way right now (in
> EROS/Coyotos) to *check* whether instantiator == builder. Adding such a
> mechanism would completely invalidate the current verification proof. It
> is possible that the new system could be verified. Since you are the
> person proposing the change, I think that the burden of verification
> must come from you.

Pfft, the instantiator *knows* that it is the builder.  No further
mechanism is necessary to check this.  You seem to have a wrong
picture of how process instantiation would work in such a system.

If you want to talk about validation, you need to name the property
you want me to validate.

Thanks,
Marcus