PriSC 2022
2022-01-16
Philadelphia, United States
PriSC ·
[PriSC 2020, PriSC 2022, PriSC 2023, PriSC 2024, PriSC 2026]
who it's for
compiler engineers, formal methods engineers, security researchers, programming languages researchers, systems software engineers, hardware security engineers, verification engineers
topics
eBPF speculative execution mitigations; speculative store bypass exploits; type-directed constant-time transformation; Spectre-PHT testing in Rust; Rosette symbolic execution for counterexamples; secure compilation counterexample synthesis; hardware-software codesign validation; robust and fully abstract compilation; data-flow back-translation proofs; instruction-level symbolic encryption (RISC-V); effect-oblivious equivalence for effects; WebAssembly proof-checking kernel in Rust
| title | author | length |
|---|---|---|
| BPF and Spectre: Mitigating transient execution attacks | Daniel Borkmann | 01h 03m |
Shows proof‑of‑concept exploits that use speculative store bypass and memory disambiguation to make unprivileged eBPF read kernel memory, and describes… | ||
| Type-directed Program Transformation for Constant-Time Enforcement | Gautier Raimondi, Floriana Ciaglia | 26m |
Claims a more permissive information‑flow type system that records indirect-of{p} dependencies and rejects only direct flows, then uses those types to drive a… | ||
| Towards Understanding Spectre-PHT in Memory-Safe Languages | Neil Zhao, Floriana Ciaglia | 25m |
A testing framework instruments Rust libraries with SpecFuzz to simulate branch mispredictions (skipping annotated bounds checks), runs four-hour fuzz sessions… | ||
| Synthesizing Evidence of Emergent Computation | Scott Moore, Floriana Ciaglia | 31m |
Tool called seek synthesizes counterexamples to secure compilation from executable language models and uses Rosette symbolic execution to produce concrete… | ||
| Providing evidence for the security properties of hardware/software codesigns | Frank Piessens, Marco Guarnieri | 01h 08m |
Argument: end-to-end proofs need empirical validation for real devices. The team builds an FPGA prototype of VRASED on an MSP430 core, uses F proofs of crypto… | ||
| Composing Secure Compilers | arthur amoren, mattis uh cruz, mata skruzzle, Marco Patrignani | 25m |
Formal results show that composing compilers preserves concrete classes of hyperproperties: sequential and upper composition guarantee that two compilers that… | ||
| SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn | Akram El-Korashy | 26m |
Proposes a concrete back-translation that emits data-flow traces (register moves, loads, stores) so stashing pointers no longer requires traversing the… | ||
| The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How t | Matteo Busi | 22m |
Shows that an identity compiler can be fully abstract yet break a source hyperproperty: a target club symbol context forces termination of a source… | ||
| A CompCert backend with symbolic encryption | paulo torrini, sylvain bulmay | 29m |
A verified C backend called IntrinSec extends CompCert’s RISC-V backend with instruction-level symbolic encryption: new mask registers, four crypto… | ||
| Effect-Oblivious Equivalence | Yao Li, Yishuai Li, Marco Guarnieri | 27m |
Defines effect-oblivious equivalence: two programs are equivalent no matter how effects are implemented, so proofs do not assume concrete IO or handler… | ||
| The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-g | Dominic Mulligan, Marco Guarnieri, Nick Spinale | 26m |
A prototype proof-checking kernel implemented as a Rust implementation running as a WebAssembly host exposes a 75-call syscall interface (about 75 syscalls)… | ||
| nothing matches | ||