System Software Design for Undiluted Attestation
Charly Nicolas Lucien Castes · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · 2026
In trusted execution environments, the authenticity and security properties of a computer system are determined by examining its attestation. Reviewing the attestation should be sufficient to evaluate the system's correctness; however, this is not the case today. Proprietary system software cannot be audited for security, while existing isolation abstractions fail to capture important nuances, such as the existence of transient-execution attacks. In this thesis, we demonstrate that, through software-only changes, it is possible to design systems for which correctness can be derived solely from examination of their attestation, assuming only the correctness of hardware and of software that can be audited. We address this problem in two steps. First, we ensure that system software can be relied upon for isolation and for producing the attestation. Then, that trusted system software can enforce strong isolation policies whose security properties can be verified from the attestation. In Part I we tackle the challenge of proprietary software running at the highest privilege level - #ie in firmware mode. We introduce the concept of virtual firmware monitors, a new kind of system that can virtualize unmodified vendor firmware, and thus remove proprietary code from the highest privilege mode. We discuss the design and implementation of Miralis, a RISC-V virtual firmware monitor, and demonstrate the virtualization of unmodified firmware on three off-the-shelf RISC-V computers from different vendors. To ensure the isolation guarantees of virtual firmware monitors cannot be bypassed by the virtualized firmware, we propose a framework for automated verification of firmware mode virtualization, and discuss the verification of Miralis. Our framework leverages existing ISA specifications and lightweight formal verification tools, such as model checkers. As a result, we enable safe and efficient sandboxing of untrusted vendor firmware. In Part II we focus on the isolation mechanisms and their integration with the system's attestation. We propose core gapping, a new technique that provably prevents an attacker and a victim from being co-scheduled on the same core, eliminating all same-core attacks - and thus the majority of transient-execution attacks. We demonstrate its application to confidential VMs on Arm CCA platforms, and discuss how to integrate core gapping with minimal changes and performance overhead on existing systems. We then introduce the idea of capability-based security monitors, inspired by the design of micro-kernels, but with support for confidential memory and integration with the system's attestation. We present the design and implementation of Tyche, a capability-based security monitor for x86-64 and RISC-V. We show that Tyche can reconstruct existing abstractions such as enclaves and confidential VMs, while also enabling new use cases including multi-domain attestation and shared confidential memory.