Re: A Framework for Device Drivers in Microkernel Operating Systems

[Espen Skoglund]

[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 Depending on your definition of security, the presence of global
    names does not necessarily mean that the system is unsecure.

  o The problems with global name spaces are being addressed in L4Ka
    and local name spaces have been implemented in L4Ka::Pistachio.

        eSK