If comprehensive static proofs are in the picture, there's little benefit to running trusted code in user mode. It's just adding a protection boundary to something that could already be proven as safe via static analysis. IO-MMU however could still be useful since it somewhat obviates the need to trust the device itself, and devices are much harder to characterize properly.
If comprehensive static proofs are in the picture, there's little benefit to running trusted code in user mode. It's just adding a protection boundary to something that could already be proven as safe via static analysis.
Try seeing it the other way around. It minimizes what needs proving (it isn't cheap) by having the microkernel (small and proven) enforce separation.
Capabilities (not to be confused with POSIX capabilities, which are something else) do help massively here. Refer to the Genode Book[0] introduction chapter for an introduction to capabilities.
In the driver example, running the driver unprivileged means the damage a faulty driver can be contained. In combination with a iommu, it can be made so that the hardware can only talk to the driver, to complete the protection. This is only possible if the kernel itself can be trusted, which would mean the kernel has to be proven, and that's unrealistic unless it's a microkernel, as it is a very costly process that doesn't even scale linearly with LoC.
The alternative is to make all drivers part of the TCB, which isn't realistic for the same reason. Unfortunately, on top of this, driver code quality is known to be particularly bad.
Comments
If comprehensive static proofs are in the picture, there's little benefit to running trusted code in user mode. It's just adding a protection boundary to something that could already be proven as safe via static analysis. IO-MMU however could still be useful since it somewhat obviates the need to trust the device itself, and devices are much harder to characterize properly.
Try seeing it the other way around. It minimizes what needs proving (it isn't cheap) by having the microkernel (small and proven) enforce separation.
Capabilities (not to be confused with POSIX capabilities, which are something else) do help massively here. Refer to the Genode Book[0] introduction chapter for an introduction to capabilities.
In the driver example, running the driver unprivileged means the damage a faulty driver can be contained. In combination with a iommu, it can be made so that the hardware can only talk to the driver, to complete the protection. This is only possible if the kernel itself can be trusted, which would mean the kernel has to be proven, and that's unrealistic unless it's a microkernel, as it is a very costly process that doesn't even scale linearly with LoC.
The alternative is to make all drivers part of the TCB, which isn't realistic for the same reason. Unfortunately, on top of this, driver code quality is known to be particularly bad.
[0] https://genode.org/