Re: How to add confinement to the Hurd?

[Jonathan S. Shapiro]

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.

> But, you have at least to give me credit for being consistent

I do.

> and rejecting a feature which I feel violates an important design goal
> (user freedom, which I have not yet formally stated, but will), _and_
> which is proposed to be included on the pure speculation that it may
> be useful in the future, _but_ with the full knowledge that it is
> harmful in the short and medium run.

If there is a goal that you are actually trying to achieve, state the
goal. There may be multiple ways to achieve it. Perhaps it is achievable
with a smaller deviation from the current design. But one thing I *do*
know: if the goal cannot be clearly stated, the proposed "solution" is
almost always the wrong thing.

> > 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.

Please, let us look to see whether a less dramatic change will suffice.
State your goal so that we can make this determination!


shap