PriSC 2023
who it's for
secure compilation researchers, compiler engineers, formal verification engineers, cryptography engineers, trusted execution environment developers, browser engine engineers, language designers
topics
semantic intermediate representations; interface-preserving compilation; verified trusted execution environments; automata learning for enclaves; remote attestation calculus; robust constant-time implementations; blame-preserving compilation; F* secure compilation with IO; CompCert compartments to CHERI; DSL for JIT verification; translation validation for JITs; universally composable program partitioning
| title | author | length |
|---|---|---|
| Semantic Intermediate Representations for Sound Language Interoperability | Amal Ahmed | 01h 05m |
Claim: build semantic IRs — logical relations that map each source type to a set of target terms — to prove interoperability after compilation. Implementation… | ||
| Towards End-to-End Verified TEEs via Verified Interface Conformance and Interfa... | Farzaneh Derakhshan, Zichao Zhang, Amit Vasudevan, Limin Jia | 29m |
Framework formalizes TEEs as isolated compartments (Uber objects) with exclusive memory and verified pre/post interfaces, verified in isolation and compiled… | ||
| Automated Learning and Verification of Embedded Security Architectures | Matteo Busi, Riccardo Focardi, Flaminia L. Luccio | 27m |
Proposes reducing the model/implementation gap by extracting concrete behavioral models with automata learning and checking preservation of robust… | ||
| pi_RA: A pi-calculus for verifying protocols that use remote attestation | Emiel Lanckriet, Matteo Busi, Dominique Devriese | 23m |
pi_RA is an applied pi-calculus variant that treats remote attestation as a first‑class cryptographic primitive and compiles an actor-style source language… | ||
| Robust Constant-Time Cryptography | Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan | 23m |
Constant-time is insufficient: code that avoids secret-dependent branches still leaks when keys live in memory or the application misbehaves. The work defines… | ||
| Short Talk: Generalising secure compilation criteria | Emiel Lanckriet | 08m |
Proposes a concrete framework that extends robust property preservation (RHP) and reduction/backtranslation (RHC) to cover probabilistic behaviors… | ||
| Blame-Preserving Secure Compilation | Marco Patrignani, Matthis Kruse | 31m |
Proposes a new secure-compilation criterion, Blame-Preserving Compilation, that refuses trivial proofs when the source language (e.g., C) cannot robustly… | ||
| Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ... | Cezar-Constantin Andrici, Cătălin Hriţcu, Théo Winterhalter | 21m |
Secure compilation chain for an F subset with IO converts static specs into runtime checks and adds a linking-time reference monitor that blocks forbidden… | ||
| SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M... | Jérémy Thibault, Arthur Azevedo de Amorim, Roberto Blanco, Aina Linn Georges, Cătălin Hriţcu, Andrew Tolmach | 28m |
Extension of CompCert implements CompCert with compartments that enforces interfaces, disables cross-compartment inlining/tailcalls, and updates Coq… | ||
| Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers | Michael Smith, Abhishek Sharma, John Renner, David Thien, Sorin Lerner, Fraser Brown, Hovav Shacham, Deian Stefan | 27m |
Cachet is a DSL that compiles Cachet to Boogie and C++ and encodes JIT invariants so the verifier proves generated code never violates them. The toolchain uses… | ||
| FaJITa: Verifying Optimizations on Just-In-Time Programs | David Thien, Michael Smith, Evan Johnson, Sorin Lerner, Hovav Shacham, Deian Stefan, Fraser Brown | 27m |
FaJITa is a translation validator that checks semantic equivalence of JavaScript functions after Firefox JIT optimizations by combining symbolic execution with… | ||
| Universally Composable Security for Program Partitioning | Coşku Acay, Joshua Gancher, Rolph Recto, Andrew C. Myers | 27m |
An implemented compiler called Viaduct compiler takes a single-threaded program with tuple information-flow labels (confidentiality, integrity) and… | ||
| nothing matches | ||