PriSC 2025 (with POPL 2025)
who it's for
compiler engineers, language designers, security engineers, formal methods engineers, cryptography engineers, Rust developers, software auditors
topics
Rust crate effect auditing; speculative non-interference; verified eBPF compilation; semantic backtranslation for compilers; verified cryptographic protocol toolchain; unsafe Rust exploit patterns; hyperproperty simulation proofs; automatic enclave placement; speculative constant-time preservation; noise-typed homomorphic circuits; programming for zkSNARKs
| title | author | length |
|---|---|---|
| Auditing Rust Crates Effectively | Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford | 18m |
Cargo Scan is an interactive analysis tool that inspects Rust crates, models side-effecting APIs, and propagates color-checked propagation across call sites so… | ||
| SNIP: Speculative Execution and Non-Interference Preservation for Compiler(…) | Sören van der Wall, Roland Meyer | 24m |
Proposes a new directive-based simulation that models attacker-controlled microarchitectural choices and proves dead‑code elimination preserves speculative… | ||
| BeePL: Correct-by-compilation kernel extensions | Swarn Priya, Tim Steenvoorden, Connor Sughrue, Frédéric Besson, Freek Verbeek | 20m |
BeePL is a new source language whose type system encodes eBPF specs (effects, substructural and refinement types) and whose goal is a Coq-verified compiler… | ||
| A Semantic Approach to Robust Property Preservation | Niklas Mück, Michael Sammler, Aina Linn Georges, Derek Dreyer, Deepak Garg | 25m |
Proposes a semantic reduction of robust property preservation: replace hard syntactic backtranslation with a backtranslation between semantic domains, so… | ||
| Keynote: Bringing Verified Cryptographic Protocols to Practice | Bryan Parno | 01h 00m |
A toolchain produces provably secure, interoperable protocol implementations: a type-based verifier Owl yields computationally sound proofs, an SMT-backed… | ||
| Counterexamples in Safe Rust | Muhammad Hassnain, Caleb Stanford | 19m |
Shows concrete safe Rust breaks: using proc/self/mem memory patching to flip const pointers and enlarge vector capacity for out‑of‑bounds reads/writes… | ||
| Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations | Julian Rosemann, Sebastian Hack, Deepak Garg | 26m |
Presents a formal framework that generalizes compiler simulation proofs to arbitrary k‑trace hyperproperties and claims preservation of… | ||
| Automatic Inference of Enclave Placement in LLVM Compiler | Wesley B Nuzzo, Mohamed Elwakil, Anitha Gollamudi | 25m |
Claims a practical LLVM-based pipeline that infers which functions and pointers must live inside enclaves and lowers them to Intel SGX using OpenEnclave… | ||
| Preservation of Speculative Constant-time by Compilation | Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, Vincent Laporte | 18m |
Shows that common compilers (GCC -O0 and -O1 and Jasmin) produce speculatively insecure binaries from speculatively constant-time sources, then builds a… | ||
| ILA: Correctness via Type Checking for Fully Homomorphic Encryption | Tarakaram Gollamudi, Anitha Gollamudi, Joshua Gancher | 26m |
ILA is an intermediate language that attaches quantitative bounds (plaintext range and ciphertext noise) as types and proves that well-typed ILA circuits… | ||
| Leveraging Duality for Programming with zkSNARKs | Rahul Krishnan, Ethan Cecchetti | 26m |
Language adds a single combined block that is annotated at variable declarations with C/P/CP labels, then a compiler projects that block into two low-level… | ||
| nothing matches | ||