Publications de Thomas Emile Bourgeat

Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet

Edouard Bugnion, Charly Nicolas Lucien Castes, Thomas Emile Bourgeat

Hypervisors are an essential part of our computing infrastructure, yet ensuring their correctness remains a significant challenge for the community. While several hypervisors have been formally verified using traditional methods, they have typically requir ...

ACM2025

RTL Verification for Secure Speculation Using Contract Shadow Logic

Thomas Emile Bourgeat

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 abil ...

Association for Computing Machinery2025

Parendi: Thousand-Way Parallel RTL Simulation

James Richard Larus, Thomas Emile Bourgeat

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 ...

ACM2025

Making Concurrent Hardware Verification Sequential

Thomas Emile Bourgeat

Compared to familiar hardware-description languages like Verilog, rule-based languages like Bluespec offer opportunities to import modularity features from software programming. While Verilog modules are about connecting wires between submodules, Bluespec ...

2025

Verifying Software Emulation of an Unsupported Hardware Instruction

Thomas Emile Bourgeat

Some processors, especially embedded ones, do not implement all instructions in hardware. Instead, if the processor encounters an unimplemented instruction, an unsupported-instruction exception is raised, and an exception handler is run that implements the ...

Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing2024

Formal Verification for Secure Processors: A Guide for Computer Architects

Thomas Emile Bourgeat

As computer architects continually push the limits of microarchitectural performance optimizations, securing hardware against speculative execution attacks feels like a Sisyphean task. This article explores the critical role computer architects can play in ...

IEEE COMPUTER SOC2024

Specification and Verification of Strong Timing Isolation of Hardware Enclaves

Clément Pit-Claudel, Thomas Emile Bourgeat

The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: attacks exploit timing side channels derived from contention on shared microarchitectural resource ...

Association for Computing Machinery, Inc2024