-
Automatic ISA analysis for Secure Context Switching
Authors:
Neelu S. Kalani,
Thomas Bourgeat,
Guerney D. H. Hunt,
Wojciech Ozga
Abstract:
Instruction set architectures are complex, with hundreds of registers and instructions that can modify dozens of them during execution, variably on each instance. Prose-style ISA specifications struggle to capture these intricacies of the ISAs, where often the important details about a single register are spread out across hundreds of pages of documentation. Ensuring that all ISA-state is swapped…
▽ More
Instruction set architectures are complex, with hundreds of registers and instructions that can modify dozens of them during execution, variably on each instance. Prose-style ISA specifications struggle to capture these intricacies of the ISAs, where often the important details about a single register are spread out across hundreds of pages of documentation. Ensuring that all ISA-state is swapped in context switch implementations of privileged software requires meticulous examination of these pages. This manual process is tedious and error-prone.
We propose a tool called Sailor that leverages machine-readable ISA specifications written in Sail to automate this task. Sailor determines the ISA-state necessary to swap during the context switch using the data collected from Sail and a novel algorithm to classify ISA-state as security-sensitive. Using Sailor's output, we identify three different classes of mishandled ISA-state across four open-source confidential computing systems. We further reveal five distinct security vulnerabilities that can be exploited using the mishandled ISA-state. This research exposes an often overlooked attack surface that stems from mishandled ISA-state, enabling unprivileged adversaries to exploit system vulnerabilities.
△ Less
Submitted 10 February, 2025;
originally announced February 2025.
-
RTL Verification for Secure Speculation Using Contract Shadow Logic
Authors:
Qinhan Tan,
Yuheng Yang,
Thomas Bourgeat,
Sharad Malik,
Mengjia Yan
Abstract:
Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus, a formal and rigorous evaluation of the ability of hardware designs to deal with speculative execution attacks is urgently desired. This paper proposes a formal verification technique call…
▽ More
Modern out-of-order processors face speculative execution attacks. Despite various proposed software and hardware mitigations to prevent such attacks, new attacks keep arising from unknown vulnerabilities. Thus, a formal and rigorous evaluation of the ability of hardware designs to deal with speculative execution attacks is urgently desired. This paper proposes a formal verification technique called Contract Shadow Logic that can considerably improve RTL verification scalability while being applicable to different defense mechanisms. In this technique, we leverage computer architecture design insights to improve verification performance for checking security properties formulated as software-hardware contracts for secure speculation. Our verification scheme is accessible to computer architects and requires minimal formal-method expertise. We evaluate our technique on multiple RTL designs, including three out-of-order processors. The experimental results demonstrate that our technique exhibits a significant advantage in finding attacks on insecure designs and deriving complete proofs on secure designs, when compared to the baseline and two state-of-the-art verification schemes, LEAVE and UPEC.
△ Less
Submitted 16 July, 2024;
originally announced July 2024.
-
Parendi: Thousand-Way Parallel RTL Simulation
Authors:
Mahyar Emami,
Thomas Bourgeat,
James Larus
Abstract:
Hardware development critically depends on cycle-accurate RTL simulation. However, as chip complexity increases, conventional single-threaded simulation becomes impractical due to stagnant single-core performance.
Parendi is an RTL simulator that addresses this challenge by exploiting the abundant fine-grained parallelism inherent in RTL simulation and efficiently mapping it onto the massively p…
▽ More
Hardware development critically depends on cycle-accurate RTL simulation. However, as chip complexity increases, conventional single-threaded simulation becomes impractical due to stagnant single-core performance.
Parendi is an RTL simulator that addresses this challenge by exploiting the abundant fine-grained parallelism inherent in RTL simulation and efficiently mapping it onto the massively parallel Graphcore IPU (Intelligence Processing Unit) architecture. Parendi scales up to 5888 cores on 4 Graphcore IPU sockets. It allows us to run large RTL designs up to 4$\times$ faster than the most powerful state-of-the-art x64 multicore systems.
To achieve this performance, we developed new partitioning and compilation techniques and carefully quantified the synchronization, communication, and computation costs of parallel RTL simulation: The paper comprehensively analyzes these factors and details the strategies that Parendi uses to optimize them.
△ Less
Submitted 16 March, 2025; v1 submitted 7 March, 2024;
originally announced March 2024.
-
Citadel: Simple Spectre-Safe Isolation For Real-World Programs That Share Memory
Authors:
Jules Drean,
Miguel Gomez-Garcia,
Fisher Jepsen,
Thomas Bourgeat,
Srinivas Devadas
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 sp…
▽ More
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.
△ Less
Submitted 6 February, 2025; v1 submitted 26 June, 2023;
originally announced June 2023.
-
Flexible Instruction-Set Semantics via Type Classes
Authors:
Thomas Bourgeat,
Ian Clester,
Andres Erbsen,
Samuel Gruetter,
Pratap Singh,
Andrew Wright,
Adam Chlipala
Abstract:
Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use semantics in rather different ways. As a result, a central challenge for that community is how semantics should be written and what techniques should be…
▽ More
Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use semantics in rather different ways. As a result, a central challenge for that community is how semantics should be written and what techniques should be used to connect them to new use cases. The best-known work applying single semantics across quite-different tools relies on domain-specific languages like Sail, where the language and its translation tools are specialized to the realm of instruction sets. We decided to explore a different approach, with semantics written in a carefully chosen subset of Haskell. This style does not depend on any new language translators, relying instead on parameterization of semantics over type-class instances. As a result, a semantics can be a first-class object within a logic, and application of a semantics for a new kind of tool can be a first-class operation in the logic, allowing sharing of theorems across applications. Our case study is for the open RISC-V instruction-set family, and we have used a single core semantics to support testing, interactive proof, and model checking of both software and hardware. We especially highlight an application of a first-class semantics within Coq that can be instantiated in different ways within one proof: simulation between variants where multiplication is implemented in hardware or in the machine code of a particular software trap handler.
△ Less
Submitted 16 November, 2022; v1 submitted 1 April, 2021;
originally announced April 2021.
-
MI6: Secure Enclaves in a Speculative Out-of-Order Processor
Authors:
Thomas Bourgeat,
Ilia Lebedev,
Andrew Wright,
Sizhuo Zhang,
Arvind,
Srinivas Devadas
Abstract:
Recent attacks have broken process isolation by exploiting microarchitectural side channels that allow indirect access to shared microarchitectural state. Enclaves strengthen the process abstraction to restore isolation guarantees.
We propose MI6, an aggressive, speculative out-of-order processor capable of providing secure enclaves under a threat model that includes an untrusted OS and an attac…
▽ More
Recent attacks have broken process isolation by exploiting microarchitectural side channels that allow indirect access to shared microarchitectural state. Enclaves strengthen the process abstraction to restore isolation guarantees.
We propose MI6, an aggressive, speculative out-of-order processor capable of providing secure enclaves under a threat model that includes an untrusted OS and an attacker capable of mounting any software attack currently considered practical, including control flow speculation attacks. MI6 is inspired by Sanctum [16] and extends its isolation guarantee to more realistic memory hierarchies. It also introduces a purge instruction, which is used only when a secure process is scheduled, and implements it for a complex processor microarchitecture. We model the performance impact of enclaves in MI6 through FPGA emulation on AWS F1 FPGAs by running SPEC CINT2006 benchmarks on top of an untrusted Linux OS. Security comes at the cost of approximately 16.4% average slowdown for protected programs.
△ Less
Submitted 29 August, 2019; v1 submitted 23 December, 2018;
originally announced December 2018.
-
A probabilistic Hadwiger-Nelson problem
Authors:
Thomas Bourgeat,
Marc Heinrich,
Paul Melotti,
Jean-Marc Robert
Abstract:
If you color a table using k colors, and throw a needle randomly on it, for some proper definition, you get a certain probability that the endpoints will fall on different colors. How can one make this probability maximal? This problem is related to finite graphs having unit-length edges, and some bounds on the optimal probability are deduced.
If you color a table using k colors, and throw a needle randomly on it, for some proper definition, you get a certain probability that the endpoints will fall on different colors. How can one make this probability maximal? This problem is related to finite graphs having unit-length edges, and some bounds on the optimal probability are deduced.
△ Less
Submitted 11 January, 2015;
originally announced January 2015.
-
New Algorithmic Approaches to Point Constellation Recognition
Authors:
Thomas Bourgeat,
Julien Bringer,
Herve Chabanne,
Robin Champenois,
Jeremie Clement,
Houda Ferradi,
Marc Heinrich,
Paul Melotti,
David Naccache,
Antoine Voizard
Abstract:
Point constellation recognition is a common problem with many pattern matching applications. Whilst useful in many contexts, this work is mainly motivated by fingerprint matching. Fingerprints are traditionally modelled as constellations of oriented points called minutiae. The fingerprint verifier's task consists in comparing two point constellations. The compared constellations may differ by rota…
▽ More
Point constellation recognition is a common problem with many pattern matching applications. Whilst useful in many contexts, this work is mainly motivated by fingerprint matching. Fingerprints are traditionally modelled as constellations of oriented points called minutiae. The fingerprint verifier's task consists in comparing two point constellations. The compared constellations may differ by rotation and translation or by much more involved transforms such as distortion or occlusion. This paper presents three new constellation matching algorithms. The first two methods generalize an algorithm by Bringer and Despiegel. Our third proposal creates a very interesting analogy between mechanical system simulation and the constellation recognition problem.
△ Less
Submitted 24 March, 2014;
originally announced May 2014.