Information on implementing L4

Andrew Warkentin andreww591 at
Fri Sep 14 08:18:24 CEST 2018

On Thu, Sep 13, 2018, 11:15 PM Gernot Heiser <gernot at> wrote:

> I think when you say “language-based OS” you mean type-system enforced
> security rather than MMU-enforced security

Yes, basically. I'm talking about OSes that integrate some form of
language-specific VM at a fundamental level, often depending on the VM for

> I haven’t seen any approach of this sort that didn’t end up with an unsafe
> but trusted blob of code (language run-time) that’s as big if not bigger
> than your typical L4 kernel, besides having higher run-time overheads. I
> fail to see how this would be better in any way. Particularly when you can
> have your L4 kernel formally verified (i.e. seL4).

Yes, that's basically the same thing I was saying. Managed code has higher
overhead and a bigger TCB (which often contains a lot of unsafe code) than
safer native code (either formally verified or just written in a safer
language like Rust) does.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the l4-hackers mailing list