On 22 Nov 2020, at 18:56, Andrew Warkentin <andreww591@gmail.commailto:andreww591@gmail.com> wrote:
Of course, in a system that runs a legacy general-purpose OS in a VM on top of a static system, only applications that are specifically written to use the secure APIs can actually be properly secured (and that's assuming that the secure static part of the system is actually capable of doing what the application needs). An seL4-native general purpose OS could apply the same security model to everything, including unmodified applications for legacy OSes assuming it provides a compatible environment, albeit at the very likely expense of formal verification of most OS components and subsystems above the kernel. However, even a mostly-unverified microkernel OS should still be considerably more secure than a legacy OS assuming the design is remotely reasonable.
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.
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