PriSC 2024
2024-01-20
London, United Kingdom
PriSC ·
[PriSC 2020, PriSC 2022, PriSC 2023, PriSC 2024, PriSC 2026]
who it's for
secure compilation researchers, compiler engineers, systems security engineers, formal methods engineers, hypervisor developers, runtime and VM engineers, smart contract engineers
topics
CHERI capability calling conventions; V8 constant-time transformer; speculative execution verification; Spectre mitigation composition; control-flow linearization with AMi; ARM ASL modularization for virtualization; semantic application binary interfaces; translation validation for obfuscation; computationally robust compilation and UC; gradual verification for smart contracts; microarchitectural side-channel mitigation for serverless
| title | author | length |
|---|---|---|
| Introduction | Shweta Shinde, Marco Patrignani | 01m |
PriSC 2024 opens by naming the Principles of Secure Compilation Workshop, noting 11 accepted papers and thanking 22 program committee members who reviewed… | ||
| Keynote: Can we reason about the security of concurrent systems code? | Peter Sewell | 01h 05m |
Goal is to verify Google’s PKVM hypervisor running on ARM, not just papers: ARM semantics is captured in 420,000 lines of ARM spec (Sail/ASL), the hypervisor… | ||
| Secure Calling Conventions for CHERI Capability Machines in Practice (Work in P... | Elias Storme, Sander Huyghebaert, Steven Keuchel, Thomas Van Strydonck, Dominique Devriese | 24m |
Proposes a concrete design that reconciles theoretical secure calling conventions with real CHERI-RISC-V constraints by introducing a reserve stack to avoid… | ||
| Microarchitectural Side-Channel Mitigations for Serverless Applications | Yayu Wang, Aastha Mehta | 22m |
Project claims automatic microarchitectural side‑channel mitigation for serverless JavaScript by modifying V8: Scooti modifies V8 to add a CT transformer, CT… | ||
| Lifting Compiler Security Properties to Stronger Attackers: the Speculation Cas... | Xaver Fabian, Marco Guarnieri, Michael Backes | 20m |
A formal framework proves when a compiler countermeasure for Spectre-style leaks preserves security against stronger attacker models by modelling speculative… | ||
| Secure Composition of SPECTRE Mitigations | Matthis Kruse, Michael Backes | 23m |
Formal framework proves when compiler passes that add Spectre mitigations compose safely and when they do not, using robust preservation and a cross-language… | ||
| When Obfuscations Preserve Cryptographic Constant-Time | Matteo Busi, Pierpaolo Degano, Letterio Galletta | 21m |
Proposes a sufficient condition and a per-program translation validation that statically checks whether an obfuscation preserves cryptographic constant-time… | ||
| Compiler Support for Control-Flow Linearization Using Architectural Mimicry | Daan Vanoverloop, Hans Winderix, Lesly-Ann Daniel, Frank Piessens | 27m |
Implements an LLVM backend pass that automates control‑flow linearization for reducible graphs using Architectural Mimicry (AMi) mimic execution and persistent… | ||
| Modularizing CPU Semantics for Virtualization | Paolo G. Giarrusso, Abhishek Anand, Gregory Malecha, František Farka, Hoang-Hai Dang | 25m |
Proposes a concrete decomposition of ARM ASL into an unprivileged core and a small privileged handler so one common unprivileged semantics can be reused across… | ||
| All the Binaries Together: A Semantic Approach to Application Binary Interfaces | Andrew Wagner, Amal Ahmed | 35m |
Proposes a concrete semantic ABI that maps a functional source language to a C-ish, reference-counted target using realizability models and separation logic to… | ||
| Computational-Bounded Robust Compilation and Universally Composable Security | Robert Künnemann, Ethan Cecchetti | 22m |
Proposes a precise equivalence showing that computationally robust hyper property preservation corresponds to computational UC emulation by adding… | ||
| Gradual Verification for Smart Contracts | Haojia Sun, Kunal Singh, Jan-Paul Ramos-Davila, Jonathan Aldrich, Jenna Wise | 23m |
Gradual verification combines static separation-logic proofs with imprecise specifications (written as question marks) and automatically emits dynamic checks… | ||
| Towards Modular Specification and Verification of Concurrent Hypervisor-based I... | Hoang-Hai Dang, David Swasey, Gregory Malecha | 24m |
NOVA is a microhypervisor of 17K lines and 15 hypercalls whose specification (~100 pages) is decomposed with Iris-based separation logic into WP_Nova_EC and… | ||
| Closing Remarks | Shweta Shinde | 01m |
Workshop concludes with brief thanks, offers Marco (co-chair) and session chairs Marco Mato and Dominique public acknowledgment for running sessions, notes… | ||
| nothing matches | ||