Marco Guarnieri
where else to find them
bluesky:mguarnieri.bsky.social
what they talk about
where they keep going back
- PriSC2 editions2022–2024
on a stage with
all 11 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks | POPL 2025 | 2025-01-19 |
Paper introduces a lifting framework that upgrades compiler guarantees proved for weaker speculative semantics to stronger ones without redoing full secure… | ||
| Lifting Compiler Security Properties to Stronger Attackers: the Speculation Cas... | PriSC 2024 | 2024-01-20 |
A formal framework proves when a compiler countermeasure for Spectre-style leaks preserves security against stronger attacker models by modelling speculative… | ||
| ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification | PLDI 2022 | 2022-06-13 |
ANOSY verifies attacker-knowledge approximations and synthesizes posterior-update functions using refinement types, then checks them with Liquid Haskell and an… | ||
| Providing evidence for the security properties of hardware/software codesigns | PriSC 2022 | 2022-01-16 |
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… | ||
| Effect-Oblivious Equivalence | PriSC 2022 | 2022-01-16 |
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 | PriSC 2022 | 2022-01-16 |
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 | ||