Information on implementing L4

[Andrew Warkentin]

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

>
> 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: <http://os.inf.tu-dresden.de/pipermail/l4-hackers/attachments/20180914/65508ff1/attachment.htm>