PriSC 2026
who it's for
formal verification engineers, compiler engineers, security researchers, programming language designers, systems engineers, hardware verification engineers, runtime and sandbox engineers
topics
type-preserving compilation to WebAssembly; zeroization static detection in GCC; decompiler transparency for constant-time; weakest-precondition preserving compilation; modular probabilistic constant-time proofs; binary-level symbolic execution pipelines; verified F* compilation to ML-like code; blame-aware recomposition for compiler backends; Rust FFI undefined behavior detection; IFC-aware decentralized dependency caching; formal verification of RISC-V with PMP and shadow stack; mechanized speculative load hardening (FSLH)
| title | author | length |
|---|---|---|
| Specifying ABIs with Realizability and Type-Preserving Compilation | Brianna Marshall, Ryan Doenges, Owen Duckham, Ari Prakash, Maxime Legoupil, Elan Semenova, Lars Birkedal, Amal Ahmed | 19m |
Claims a Realizability model for RichWasm that interprets source types as sets of WebAssembly configurations so a type-preserving compiler yields a memory-safe… | ||
| GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses | Pierrick Philippe, Mohamed Sabt, Pierre-Alain Fouque | 17m |
GnuZero is a GCC-integrated static detector that extends the GCC Static Analyzer (GSA) with symbolic execution and region-aware state tracking to find missing… | ||
| Decompiling for Constant-Time Analysis | Sören van der Wall, Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Youcef Bouzid, Zhiyuan Zhang | 19m |
Claims that mainstream decompilers can hide timing leaks by turning branches into conditional moves, tests five popular decompilers and finds unsoundness for… | ||
| WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification | Carmine Abate, Mohamed Elsheikh, Kleio Liotati, František Farka, Sebastian Ertel | 18m |
Claims a compilation chain that preserves weakest preconditions by proving source and compiled programs denote bisimilar interaction trees interpreted in Iris… | ||
| Modular Verification of Probabilistic Constant-Time | Xingyu Xie | 17m |
Proposes a call-by-contract modular proof rule for probabilistic constant-time that replaces each call with three steps: leak public input, invoke an ideal… | ||
| Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of(…) | Yanis Sellami, Frédéric Recoules, Sébastien Bardin | 16m |
Systematic evaluations use BinSec to run binary-level symbolic execution on two benchmarks: a constant/zeroization suite and post-quantum candidates. The… | ||
| Towards formally secure compilation of verified F* programs against unverified ML(…) | Cezar-Constantin Andrici, Danel Ahman, Cătălin Hriţcu, Guido Martínez, Abigail Pribisova, Exequiel Rivas, Théo Winterhalter | 16m |
Framework written and verified in F compiles terminating higher-order IO F programs to a deeply embedded ML-like language with an end-to-end mechanized proof… | ||
| Blame-aware Recomposition for Formally Secure Low-level Compiler Backends | Basile Schlosser, Jérémy Thibault, Cătălin Hriţcu | 18m |
This work extends recomposition with blame-aware recomposition and an overlay semantics that treats cross-compartment observations (like code-size or… | ||
| Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI | Andreea Costea | 21m |
Claims that Rust type assumptions are turned into dynamic checks from Rust types that run at FFI boundaries, a harness that uses MIRI-guided PBT to drive… | ||
| Efficient Dependency Resolution in IFC-aware Decentralized Programming | Steffan Sølvsten, Aslan Askarov | 17m |
Prototype implements an information‑flow aware cache inside the Troupe runtime as a separate trusted thread, using SHA hash keys for dependency references and… | ||
| Modular and automatic formal verification of a RISC-V processor with security mechanisms | Pierre Wilke, Cyprien Jules, Guillaume Hiet | 18m |
A 32‑bit RISC‑V core in Kôika HDL is extended with privilege levels, PMP regions, traps, a hardware shadow stack and landing pads and compiled into an IR that… | ||
| FSLH: Flexible Mechanized Speculative Load Hardening | Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig, Cătălin Hriţcu | 20m |
Presents FSLH, a middle-ground Spectre v1 mitigation that uses a static information‑flow analysis plus selective masking and a semantics that inserts masks (an… | ||
| The V8 Sandbox: From Compiler Correctness to Runtime Containment | Samuel Groß | 01h 07m |
Shifts the security goal from compiler correctness to runtime containment and ships a lightweight, in-process sandbox in Chromium that confines all V8 objects… | ||
| Compiling countermeasures against fault attacks with “Tracing LLVM” | Sébastien Michelland, Christophe Deleuze, Laure Gonnord | 18m |
An open-source LLVM extension called Tracing LLVM adds opacification and tracing primitives that make non-functional security annotations semantically… | ||
| nothing matches | ||