On 11/22/20 4:33 AM, Heiser, Gernot (Data61, Kensington NSW) wrote:
Yes. While this is a reasonable use case, it’s not one we see happening. Very few real-world systems are built from scratch, they almost inevitably are an evolution of something existing. And, compared to pulling out critical assets to run native (as in the Cog phone), the additional security gain from running *everything* native is small, compared to the huge refactoring/porting effort. That’s why just about everyone opts for the HACMS-style incremental cyber retrofit, as Cog have done it.
Are there any situations where the amount of critical code is so large that running everything native is worthwhile? Large avionics systems with millions of lines of critical flight control code are the first one that comes to mind, but I wonder if there are others. Perhaps a reasonably secure web browser? (Speaking of avionics: is it possible to scale formal verification to systems of that scale? I would love to see formally-verified avionics software.)
But if you think you gain enough by going fully native on an unverified microkernel OS, then Genode is what you should use. If you want high assurance for your critical assets, then the seL4 Core Platform is the way to go (at least once it supports VMs).
Gernot
Sincerely, Demi