SECOMP: Formally Secure Compilation of Compartmentalized C Programs

v1v2v3v4 (latest)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs

29 January 2024

Jérémy Thibault

Arthur Azevedo de Amorim

Aïna Linn Georges

Cătălin Hriţcu

ArXiv (abs)PDF HTML

Papers citing "SECOMP: Formally Secure Compilation of Compartmentalized C Programs"

8 / 8 papers shown

Title
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs Jérémy Thibault Joseph Lenormand Cătălin Hriţcu LRM 59 0 0 25 Mar 2025
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts Sander Huyghebaert Steven Keuchel Coen De Roover Dominique Devriese 40 5 0 08 Jun 2023
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation Akram El-Korashy Roberto Blanco Jérémy Thibault Adrien Durier Deepak Garg Cătălin Hriţcu LRM 44 8 0 04 Oct 2021
Isolation Without Taxation: Near Zero Cost Transitions for SFI Matthew Kolosick Shravan Narayan Evan Johnson Conrad Watt M. LeMay Deepak Garg Ranjit Jhala D. Stefan 35 16 0 30 Apr 2021
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle Akram El-Korashy Stelios Tsampas Marco Patrignani Dominique Devriese Deepak Garg Frank Piessens ELM LRM 30 14 0 12 May 2020
Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors: Extended Version Matteo Busi Job Noorman Jo Van Bulck Letterio Galletta P. Degano Jan Tobias Muhlberg Frank Piessens 27 22 0 29 Jan 2020
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations J. Almeida M. Barbosa Gilles Barthe B. Grégoire Adrien Koutsos Vincent Laporte Tiago Oliveira Pierre-Yves Strub 37 63 0 09 Apr 2019
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise Carmine Abate Arthur Azevedo de Amorim Roberto Blanco Ana Nora Evans Guglielmo Fachini ... Théo Laurent B. Pierce M. Stronati Jérémy Thibault A. Tolmach 51 41 0 02 Feb 2018