[seL4] Re: RFC-5: seL4 Core Platform

On 11/22/20 2:56 AM, Andrew Warkentin wrote:

On 11/21/20, Heiser, Gernot (Data61, Kensington NSW) wrote:

...

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.

Do you believe that an seL4-native general-purpose OS is practical? I certainly hope so! What do you believe such an OS would look like? Regarding security, I mostly agree with you, but I do have one caveat to point out. There is a distinction between assurance (essentially, correctness) and security. For instance, a legacy VM can still be very secure if there is no way for untrusted data to enter it, or if its interactions with untrusted data are extremely limited. That’s how QubesOS works, and it has proven to be quite successful. In the case of QubesOS, this has allowed Linux-native desktop environments (such as XFCE and KDE) to be used in security-critical areas. This in turn allows for a much better user experience than would otherwise be possible given the project’s resources, and has been critical in QubesOS’s success in the desktop space. Sincerely, Demi