Citadel: Simple Spectre-Safe Isolation For Real-World Programs That Share Memory

TL;DR

Citadel introduces Relaxed Microarchitectural Isolation (RMI) to defend against transient execution side channels while enabling memory sharing for non-constant-time programs. It combines strong microarchitectural isolation (inspired by MI6) with simple hardware controls to limit speculative leakage, offering Safe mode (no speculative shared memory) and Burst mode (bounded speculation) backed by lightweight static analysis. The end-to-end FPGA prototype demonstrates low overheads (<5%) and practical portability to cryptographic libraries and private ML inference, with minimal hardware and software changes. This work establishes a coherent hardware-software contracts framework and shows how dynamic LLC partitioning and an enclave-aware security monitor can achieve real-world TES defense with shared memory.

Abstract

Transient execution side-channel attacks, such as Spectre, have been shown to break almost all isolation primitives. We introduce a new security property we call relaxed microarchitectural isolation (RMI) that allows sensitive programs that are not-constant-time to share memory with an attacker while restricting the information leakage to that of non-speculative execution. Although this type of speculative security property is typically challenging to enforce, we show that we can leverage the enclave setup to achieve it. In particular, we use microarchitectural isolation to restrict attacker's observations in conjunction with straightforward hardware mechanisms to limit speculation. This new design point presents a compelling trade-off between security, usability, and performance, making it possible to efficiently enforce RMI for any program. We demonstrate our approach by implementing and evaluating two simple defense mechanisms that satisfy RMI: (1) Safe mode, which disables speculative accesses to shared memory, and (2) Burst mode, a localized performance optimization that requires simple program analysis on small code snippets. Our end-to-end prototype, Citadel, consists of an FPGA-based multicore processor that boots Linux and runs secure applications, including cryptographic libraries and private inference, with less than 5% performance overhead.

Figures (10)

• Figure 1: Citadel's Computing Stack.
• Figure 2: Universal Read Gadget Through Shared Memory
• Figure 3: Security guarantees of secure-speculation mechanisms. Hardware semantics of Citadel' defense modes, Safe (${\color{semanticsred}\{\!\!|}\cdot{\color{semanticsred}|\!\!\}_{safe}^{}}$) and Burst (${\color{semanticsred}\{\!\!|}\cdot{\color{semanticsred}|\!\!\}_{burst}^{sta}}$), both satisfy RMI (${\color{semanticsgreen}\llbracket}\cdot{\color{semanticsgreen}\rrbracket_{shm}^{seq}}$). We also represented other relevant hardware semantics such as ${\color{semanticsred}\{\!\!|}\cdot{\color{semanticsred}|\!\!\}_{burst}^{\top}}$ which represents the hardware mechanisms of Burst without the associated static code analysis (see Section \ref{['sec:burstsecanalysis']}), and some previous works such as ${\color{semanticsred}\{\!\!|}\cdot{\color{semanticsred}|\!\!\}_{pro}^{}}$ for ProSpeCTdaniel2023prospect or ${\color{semanticsred}\{\!\!|}\cdot{\color{semanticsred}|\!\!\}_{tt}^{}}$ for taint-tracking sandboxing schemes such as STT yu2019speculative.
• Figure 4: Resource Partitioning Between Security Domains
• Figure 7: Changes to the Memory Execution Pipeline in Citadel to enable Safe mode. New elements are shown in blue.