Device Untyped Memory

Modelling the hardware more closely to improve robustness of configuring device driver access to the machine.

User-level driver Background

The L4 family of microkernels have a long history of running device drivers as user-level processes. The microkernel itself only has the bare minimum of drivers to initialise the CPU and manage time — the rest runs in user space.

User-level device drivers only have direct access to the virtual address space they execute within (DMA notwithstanding). In a typical system, a driver’s virtual address space is configured to have access to both, normal RAM and the registers of the device it drives, thus enabling the driver to present a higher-level interface to the device to the rest of the system.

This configuration of virtual memory mappings for device drivers was the trigger for the Device Untyped Memory change we introduced recently into seL4. The component configuring access to physical devices is trusted to not misconfigure the system. However, before this change, this configuration component could theoretically undermine the system by misconfiguring device registers as RAM, which could in the worst case lead to a kernel crash. This is more a robustness issue than a security issue — the configuration was always handled by software that needed to be trusted anyway. Yet, a verified kernel should not crash, not even under these circumstances. How can this be and what went wrong? Nothing was wrong with the verification, of course. What is happening here is the violation of one of the stated proof assumptions. Read on to see what we did about this and how verification ensures that this kind of problem is excluded in the future.

Improving Robustness via Device Untyped

To avoid the need to trust the low-level system configuration code as much, we have introduced Device Untyped memory objects.

What is Device Untyped and what’s changed?

User-level device access is now treated as a first class citizen in the microkernel. At boot time, for accessing device registers the initial thread will receive capabilities to untyped device memory rather than regular memory frames. Device untypeds can only be retyped into device frames, and so you cannot create other kernel objects from device untypeds. In addition, device frames cannot be used in the same way as regular frames — there are explicit checks in all places where the kernel might dereference memory to ensure the kernel doesn’t access device frames believing them to be RAM.

How does this relate to verification?

As with any formal verification, the verification of seL4 relies on assumptions, including that the hardware behaves as modelled. Device registers were not modelled in the kernel previously — the proof explicitly assumed that any frames mapped into a user’s virtual address space behaved like memory, which is not true for devices. This means that the proof guarantees were dependent on frames for device registers not being misconfigured, something which is true in practice, but is not guaranteed by proof.

By modelling device untypeds in the proof, and additionally asserting that the kernel does not access device untyped or device frames derived from them, the proof now forces us to rule out the whole class of potential bugs involving a trusted component maliciously attempting to coerce the kernel into treating devices as RAM.

In more detail, the proof is now aware of device frames, and reflects the C code changes in both the abstract Isabelle/HOL specification and the intermediate Haskell representation. We also strengthened the invariants to include statements about device frames, including:

• We added requirements for non-device caps to the validity conditions for IPC buffers in TCB objects;
• We formally separated user memory and user device memory in both the invariants and in the ADT model of the kernel’s operation;
• That is, user operations now have components for both user memory modification and device memory modifications;
• We added new invariants to ensure that caps and kernel objects do not overlap device/non-device memory.

These invariants allow us to prove that any kernel memory access is not to a device register, no matter what the initialisation component does, and no matter whether it is trusted or not. This means, verification helped us to not only improve one specific case, but also makes sure this entire kind of problem will not re-occur, and to reduce the trust that is necessary in the rest of the system.

What does this mean in practice?

In the setup of device drivers on seL4, there is now much stronger sanity checking of the virtual address space created for a device driver. There is also less trust in the software that can manipulate the driver virtual address space. The focus of safety and security of the overall system with respect to a hardware device can now focus on the behaviour of the individual device itself.

Added benefit: Large-memory support

As an aside, device untypes can be used to utilise large physical memories that where previously restricted by seL4’s design on 32-bit systems. Large RAMs in excess of seL4’s existing memory limit can be mapped as device memory for applications which just use it as normal memory.