[hackpelican]

Does the OS that lies on top of this kernel need to be formally verified as well for the security guarantees to hold?

[snvzz]

The guarantees offered by the kernel cannot be subverted by unprivileged processes running on it.

Of course, the kernel is not very useful on its own, thus the design of drivers, filesystem servers and other services running on top of the kernel is still relevant.

Note that, unlike most other systems (including Linux) which are flawed at a fundamental level, seL4 actually enables the construction of a secure and reliable system.

[marcosdumay]

Well, as long as the hardware underneath it also enables the construction of a secure system.

I don't think we have any such option right now.

[rubenbe]

No, that's the advantage is that the kernel/processes don't need to be trusted since your kernel guarantees the isolation. So you can have a Linux kernel running next to some high security process with the guarantee that they will be isolated (with the exception of allowed IPC)

[nabla9]

No.

But there are limitations. DMA off, only formally verified drivers

It's also important to note that se4L multicore kernel is not yet verified.

[snvzz]

An IOMMU can help significantly with the driver problem, preventing a properly initialized driver from misbehaving and compromising the system.

[Koshkin]

In absolute terms, sure. At the practical level, you can find a partial answer in the section 7.2 of the paper.