PriSC 2020
2020-01-25
New Orleans, United States
PriSC ·
[PriSC 2020, PriSC 2022, PriSC 2023, PriSC 2024, PriSC 2026]
who it's for
compiler engineers, formal verification engineers, WebAssembly developers, systems security engineers, runtime engineers, programming language researchers, hardware security architects
topics
AOT WebAssembly runtime; Cranelift code generation; bounds-check elision optimizations; speculative-execution defenses; constant-time select lowering; verified compilers from formats; transient-flow speculative leak detection; universal composability for compilation; memory safety preservation for WebAssembly; capability machine mechanization in Iris; tag-based compartmentalization for C; interruptible enclave security
| title | author | length |
|---|---|---|
| Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing | Tyler McMullen | 54m |
Lucet is an ahead-of-time WebAssembly compiler and runtime that Fastly uses to run user code with Cranelift codegen and an artifact contract that guarantees… | ||
| Reconciling Progress-Intensive Noninterference and Declassification | Aslan Askarov | 22m |
Proposes a concrete security condition that dials between progress-insensitive noninterference and progress-sensitive policies by tagging code regions with TV… | ||
| A CompCert Compiler that Preserves Cryptographic Constant-time | Remi Hutin | 24m |
CompCert gains a verified, branch-free selection primitive that preserves cryptographic constant-time: a new select operation with formal semantics is added to… | ||
| Universal Composability is Secure Compilation | Marco Patrignani | 25m |
Claims a correspondence between universal composability and a robust compilation criterion: UC ↔ RHC equivalence. Argues that for every target attacker a… | ||
| Exploits as Insecure Compilation | Jennifer Paykin | 25m |
Defines an exploit as a target context that makes the compiled program exhibit a behavior impossible in the source and proves this is equivalent to violating a… | ||
| Automatically Eliminating Speculative Leaks with Blade | Marco Vassena | 04m |
Blade is a static detector for speculative leaks that combines a transient-flow type system with an automatic repair pass that inserts a provably minimal set… | ||
| Everparse: A Verifying Compiler from Data Format Specifications to Verified Efficient Parsers | Tahina Ramananandro | 08m |
A verified compiler that takes dependent data-format descriptions and emits F specifications plus Low implementations extracted to high-performance C, with… | ||
| Flexible Tag-based Policies for Compartmentalized C | Sean Anderson | 23m |
A hardware-accelerated tag-monitoring design called PIPE programmable interlocks attaches metadata to registers and memory and enforces C-level policies via… | ||
| Securing Interruptible Enclaves | Matteo Busi | 23m |
Proves that adding interrupts to an enclave can be secure by modeling an ideal interrupt-free language and a realistic low-level language and proving full… | ||
| WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing | Jay Bosamiya | 24m |
A prototype compiler verifies sandboxing properties for WebAssembly by lowering Wasm into an unstructured CFG family early, doing optimizations there, and… | ||
| Memory Safety Preservation for WebAssembly | Marco Vassena | 26m |
Claims a compiler-based way to preserve memory safety when compiling C to WebAssembly by translating checked pointers into capabilities stored in private… | ||
| Implementing a Capability Machine Model into Iris | Aina Linn Georges | 24m |
Mechanization of a core capability-machine model into Iris, with an embedding of a machine language and a mechanized logical relation that solves the world… | ||
| Exorcising Spectres with Secure Compilers | Marco Patrignani | 25m |
Ongoing work builds a formal semantics that pairs a standard non‑speculative semantics with a prediction oracle–driven speculative semantics and an attacker… | ||
| nothing matches | ||