Information on implementing L4
andreww591 at gmail.com
Fri Sep 14 08:18:24 CEST 2018
On Thu, Sep 13, 2018, 11:15 PM Gernot Heiser <gernot at cse.unsw.edu.au> 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...
More information about the l4-hackers