On 11/21/20, Heiser, Gernot (Data61, Kensington NSW)
As the design document states: It’s meant to be simple but sufficient for the target domains. More generality means more complexity. The proposed model should serve almost all present use cases. Even Cog System’s “ultra-secure phone" fits this model: All the dynamicism, such as run-time installable apps, happen inside a virtual machine with an Android guest. From the seL4 PoV, the phone is a simple, static architecture with a fixed number of protected components: the “use VM” containing a full Android system with virtual drivers, the VMM, a console, a I/O multiplexing component, a “driver VM” (which should eventually become individual driver components), a network encryption component and a storage encryption VM. If the Platform supports this use case, it will definitely support most others.
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.