Our Partners

Device Virtualisation on seL4

Aim

Support secure and low-overhead sharing of devices between native components and virtual machines on seL4.

Context

The seL4 device driver framework (sDDF) provides interface specifications, libraries and tools for writing device drivers for seL4 that allow accessing devices securely and with low overhead.

We are completing and optimising the sDDF and extending it to support secure sharing of devices.

Problem

Virtualisation is an attractive mechanism for incorporating (untrusted) legacy code into an seL4-based system. This is straightforward as long as each virtual machine (VM) requires either no access to I/O devices, or can be given exclusive access to a device (using pass-through I/O).

However, in practice, VMs require access to I/O devices that are also needed by native components, the network card (NIC) is a typical example. In such a case, the device must be securely shared between VMs and native components.

There are also issues around device discovery, initialisation, and management, already solved in monolithic operating systems such as Linux, that need to be addressed for systems built on seL4.

Solution

We achieve secure device sharing by having access to the driver mediated through a multiplexer (MUX) component, which connects clients to the driver according to a policy implemented by the controller. Multiplexer and controller are security-critical components that should ideally be formally verified. It is therefore important to keep them simple.

Issues around device discovery and management are for the time being deferred.

Approach

We are working towards the above architecture in multiple stages. As shown in the diagram on the left, the first stage uses a Xen-like architecture, where a separate driver VM hosts a Linux OS with pass-through drivers. Linux user VMs interface to the driver VM using VirtIO drivers and the transport layer provided by the sDDF. Devices will be able to be shared at this stage using user-space code in the driver VM, which will prototype the multiplexers to be introduced in a later project phase.

A second step then splits up the driver VM, wrapping each Linux driver in its own VM running a minimised Linux guest, still using pass-through I/O.

The third step enables device sharing by introducing multiplexers and control components, as shown in the diagram on the right. Drivers are still hosted in (individual) Linux VMs with pass-through access, but the multiplexer now shares them between multiple users (VMs or native seL4 processes). The multiplexers can be prototyped in userspace inside the driver VMs.

Multiplexers and controllers are per-device, and their implementations are device-class specific. For example, the multiplexer and controller for an Ethernet card will look quite different from those for an audio device or a frame buffer.

The fourth step will see seL4-native drivers and the final architecture. Such drivers will depend on a very small trusted computing base, and should be able to be verified (separate project).

However, not all drivers are safety-critical, and the effort of porting or re-implementing them on seL4 is not justified. Hence the final architecture will continue to support Linux driver VMs for such devices.

Support

The sDDF project is financially supported by the Technology Innovation Institute (TII).

Collaborations

We are collaborating with researchers from TII as well as with Breakaway Consulting.

Latest News

• 2021-12-10: The research agreement between UNSW Sydney and TII is signed.

Contact

• Gernot Heiser, gernot<at>unsw.edu.au

People