Re: A Framework for Device Drivers in Microkernel Operating Systems

[Jonathan S. Shapiro]

On Mon, 2006-05-15 at 20:29 +0200, Espen Skoglund wrote:
> [Tom Bachmann]
> > I did just have a short look at it, but in section 3.1 you state
> > "L4KA's main eatures are simplicity, speed and *security*.". The
> > last is wrong.  I would not call global names and unprotected IPC
> > secure.
> 
> Just some comments:
> 
>   o L4Ka is a widely defined project that encompasses many
>     sub-projects.  One of these sub-projects is the L4Ka::Pistachio
>     microkernel.  If you want to refer to features such as those above
>     you should really refer to specific microkernel APIs instead.
> 
>   o Regarding unprotected IPCs.  The IPC mechanism in Version X.2 is
>     not completely unprotected.  You do have the Redirectors that can
>     be used for restricting IPCs, albeit not very efficiently.
> 
>   o The problems with global name spaces are being addressed in L4Ka
>     and local name spaces have been implemented in L4Ka::Pistachio.

These three points are all true, but they demonstrate that there is no
such thing as L4. There are only N different implementations sharing
not-clearly-defined portions of a specification. Because of this, it is
difficult to understand which subsystems run on which kernel versions.
It is *impossible* to understand (or substantiate) security claims for
L4 as a whole.

Meta-comment, not really related to my statement above: it is a flaw of
the L4 specification that error behavior is underspecified.


shap