TUM Logo

Confidential Computing with seL4 on RISC-V

Confidential Computing with seL4 on RISC-V

Supervisor(s): Alexander Weidinger, Lukas Auer
Status: finished
Topic: Others
Author: Philipp Alexander Grögel
Submission: 2024-10-10
Type of Thesis: Bachelorthesis
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching

Description

Multi-tenant systems in data center environments serve as the foundation for a substantial
number of software products. While data at rest can be encrypted, data in
use is commonly unencrypted and thus accessible by the cloud operators or other
unauthorized parties. To maintain confidentiality in a zero-trust environment, confidential
computing ensures that tenant data is isolated from unauthorized entities. On
RISC-V systems, confidential computing is facilitated by CoVE, which introduces this
technology to virtual machines. One of the core objectives of CoVE is to reduce the
TCB of a VM, which in turn improves the data confidentiality and trust associated with
the virtualized workload.
Microkernels, such as seL4, pursue a similar goal by design: the reduction of the
kernel’s TCB. This is achieved by relocating the majority of functionality, including
drivers such as the system’s network driver, from the kernel space to the user space.
Thus, the microkernel paradigm aligns seamlessly with CoVE by offering an extra
layer of security. However, seL4 is currently unable to operate correctly within a CoVE
confidential computing VM.
To further RISC-V’s confidential computing ecosystem, this thesis outlines changes
to seL4 and its build system which allow this kernel to work inside a confidential
computing VM. The changes to seL4 — utilizing RISC-V’s confidential computing
extension CoVE — are limited to interrupt management, necessitating only minor
adjustments. The unimpaired functionality of the modified microkernel is subsequently
confirmed using an seL4-native test suite.