A fast and reliable operating system requires fast and reliable device drivers. Most current operating systems sacrifice reliability for speed by executing drivers in kernel mode. Given that drivers account for the bulk of kernel code (70% in Linux), and that driver developers are typically not kernel experts, it does not come as a surprise that the majority of OS failures nowadays are caused by bugs in device drivers.
In a microkernel-based system, such as one based on seL4, device drivers run in user mode, as normal processes, encapsulated in their own address space. This encapsulation can be enforced through hardware mechanisms, such as the memory-management unit (MMU) and, for devices performing direct memory access (DMA) an I/O MMU. In our previous research we showed that this approach, if done right, does not impose much overhead, and allows isolating the rest of the system from device-driver failures.
While this approach removes a device driver from the trusted computing base (TCB) of a subsystem which does not use the device, many devices are essential to the overall system function, and a system may be unable to operate correctly if a critical driver fails even temporarily.
We are therefore continuing to work on making the drivers themselves reliable. We are pursuing a number of approaches, distinguished by the time to practical deployment: