Skip to main content

Showing 1–8 of 8 results for author: Bourgeat, T

.
  1. arXiv:2502.06609  [pdf, other

    cs.OS cs.CR

    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

    Submitted 10 February, 2025; originally announced February 2025.

    Comments: 15 pages, 6 figures, 2 tables, 4 listings

  2. arXiv:2407.12232  [pdf, other

    cs.AR

    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

    Submitted 16 July, 2024; originally announced July 2024.

    Comments: This paper has been accepted to ASPLOS 2025

  3. arXiv:2403.04714  [pdf, other

    cs.DC cs.AR

    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

    Submitted 16 March, 2025; v1 submitted 7 March, 2024; originally announced March 2024.

  4. arXiv:2306.14882  [pdf, other

    cs.CR cs.AR

    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

    Submitted 6 February, 2025; v1 submitted 26 June, 2023; originally announced June 2023.

  5. arXiv:2104.00762  [pdf, other

    cs.LO

    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

    Submitted 16 November, 2022; v1 submitted 1 April, 2021; originally announced April 2021.

  6. arXiv:1812.09822  [pdf, other

    cs.CR cs.OS

    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

    Submitted 29 August, 2019; v1 submitted 23 December, 2018; originally announced December 2018.

    Comments: 15 pages

  7. arXiv:1501.02441  [pdf, other

    math.CO

    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.

    Submitted 11 January, 2015; originally announced January 2015.

    Comments: 11 pages, 5 figures

  8. arXiv:1405.1402  [pdf, ps, other

    cs.CV

    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

    Submitted 24 March, 2014; originally announced May 2014.

    Comments: 14 pages, short version submitted to SEC 2014