Information on implementing L4

[Gernot Heiser]

On 14 Sep 2018, at 15:00, Andrew Warkentin <andreww591 at gmail.com> wrote:
> 
> To me, language-based OSes have always seemed interesting but a bit
> impractical and limiting. A language-based OS would face more of a
> challenge when it comes to success in the real world than a
> conventional OS would (that's one reason why I'm writing an advanced
> Unix-like OS, since that is what is most likely to be used in the real
> world).


I think when you say “language-based OS” you mean type-system enforced security rather than MMU-enforced 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).

Gernot
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://os.inf.tu-dresden.de/pipermail/l4-hackers/attachments/20180914/cd9db560/attachment.htm>