This is best complemented with a multiserver, microkernel architecture. With an IOMMU, and with near everything including drivers running in userspace, all of this can be achieved:
With a monolithic kernel such as Linux, the reliability benefits of running some drivers in userspace are negligible, as the TCB is still millions of LoCs with no proofs.
Fuchsia, Genode and HelenOS are relatively active, promising open source operating systems with a microkernel, multi-server architecture and drivers running as unprivileged processes.
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
This is best complemented with a multiserver, microkernel architecture. With an IOMMU, and with near everything including drivers running in userspace, all of this can be achieved:
https://en.wikipedia.org/wiki/MINIX_3#Reliability_policies
With a monolithic kernel such as Linux, the reliability benefits of running some drivers in userspace are negligible, as the TCB is still millions of LoCs with no proofs.
Fuchsia, Genode and HelenOS are relatively active, promising open source operating systems with a microkernel, multi-server architecture and drivers running as unprivileged processes.
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/