POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

Workshop on Principles of Secure Compilation

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, verification, systems, and hardware architectures in order to devise more secure compilation chains that eliminate many of today’s security vulnerabilities and that allow sound reasoning about security properties in the source language. For a concrete example, all modern languages provide a notion of structured control flow and an invoked procedure is expected to return to the right place. However, today’s compilation chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently enforce this abstraction against linked low-level code, which can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction. Other problems arise because today’s languages fail to specify security policies, such as data confidentiality, and the compilation chains thus fail to enforce them, especially against powerful side-channel attacks. The emerging secure compilation community aims to address such problems by identifying precise security goals and attacker models, designing more secure languages, devising efficient enforcement and mitigation mechanisms, and developing effective verification techniques for secure compilation chains.

The goal of this workshop is to identify interesting research directions and open challenges and to bring together researchers interested in working on building secure compilation chains, on developing proof techniques and verification tools, and on designing software or hardware enforcement mechanisms for secure compilation.

Format

PriSC is an informal workshop without any proceedings. Anyone interested in presenting at the workshop will submit an extended abstract (up to 2 pages), and the PC will decide which talks to accept based on a lightweight review process. We will also run a short talks session, where participants get 5 minutes to present intriguing ideas and advertise ongoing work.

Past editions (all collocated with POPL)

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 20 Jan

Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30
Session 1PriSC at Jax
09:00
4m
Day opening
Opening Remarks
PriSC
Marco Patrignani University of Trento, Marco Vassena Utrecht University
09:05
59m
Keynote
Keynote: Bringing Verified Cryptographic Protocols to Practice
PriSC
Bryan Parno Carnegie Mellon University
10:05
25m
Talk
A Semantic Approach to Robust Property Preservation
PriSC
Niklas Mück MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
11:00 - 12:30
Session 2PriSC at Jax
11:00
25m
Talk
ILA: Correctness via Type Checking for Fully Homomorphic Encryption
PriSC
Tarakaram Gollamudi None, Anitha Gollamudi University of Massachusetts Lowell, Joshua Gancher Northeastern University
11:25
24m
Talk
Leveraging Duality for Programming with zkSNARKs
PriSC
Rahul Krishnan University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison
11:50
24m
Talk
Preservation of Speculative Constant-time by Compilation
PriSC
Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria
12:15
15m
Talk
Lightning talks
PriSC

14:00 - 15:30
Session 3PriSC at Jax
14:00
24m
Talk
Auditing Rust Crates Effectively
PriSC
Lydia Zoghbi University of California, San Diego, David Thien University of California, San Diego, Ranjit Jhala UCSD, Deian Stefan University of California at San Diego, Caleb Stanford University of California, Davis
14:25
24m
Talk
Automatic Inference of Enclave Placement in LLVM Compiler
PriSC
Wesley B Nuzzo University of Massachusetts, Lowell (UML), Mohamed Elwakil U.S. Coast Guard Academy, Anitha Gollamudi University of Massachusetts Lowell
14:50
24m
Talk
Counterexamples in Safe Rust
PriSC
Muhammad Hassnain University of California, Davis, Caleb Stanford University of California, Davis
15:15
15m
Talk
Lightning talks
PriSC

16:00 - 17:30
Session 4PriSC at Jax
16:00
24m
Talk
BeePL: Correct-by-compilation kernel extensions
PriSC
Swarn Priya Virginia Tech, Tim Steenvoorden Open Universiteit, Connor Sughrue Virginia Tech, Frédéric Besson Inria, Rennes, Freek Verbeek Open Universiteit & Virginia Tech
16:25
24m
Talk
Non-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
PriSC
Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS
16:50
24m
Talk
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
PriSC
Sören van der Wall PhD Student, Roland Meyer TU Braunschweig
17:15
15m
Day closing
Closing Remarks
PriSC
Marco Patrignani University of Trento, Marco Vassena Utrecht University

Call for Presentations

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, verification, systems, and hardware architectures in order to devise more secure compilation chains that eliminate many of today’s security vulnerabilities and that allow sound reasoning about security properties in the source language. For a concrete example, all modern languages provide a notion of structured control flow and an invoked procedure is expected to return to the right place. However, today’s compilation chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently enforce this abstraction against linked low-level code, which can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction. Other problems arise because today’s languages fail to specify security policies, such as data confidentiality, and the compilation chains thus fail to enforce them, especially against powerful side-channel attacks. The emerging secure compilation community aims to address such problems by identifying precise security goals and attacker models, designing more secure languages, devising efficient enforcement and mitigation mechanisms, and developing effective verification techniques for secure compilation chains.

The goal of this workshop is to identify interesting research directions and open challenges and to bring together researchers interested in working on building secure compilation chains, on developing proof techniques and verification tools, and on designing software or hardware enforcement mechanisms for secure compilation.

9th Workshop on Principles of Secure Compilation (PriSC 2025)

The Workshop on Principles of Secure Compilation (PriSC) is an informal 1-day workshop without any proceedings. The goal is to bring together researchers interested in secure compilation and to identify interesting research directions and open challenges. The 9th edition of PriSC will be held on January 20, 2024 in Denver, Colorado (USA) together with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).

Presentation Proposals and Attending the Workshop

Anyone interested in presenting at the workshop should submit an extended abstract (up to 2 pages, details below) covering past, ongoing, or future work. Any topic that could be of interest to secure compilation is in scope. Secure compilation should be interpreted very broadly to include any work in security, programming languages, architecture, systems or their combination that can be leveraged to preserve security properties of programs when they are compiled or to eliminate low-level vulnerabilities. Presentations that provide a useful outside view or challenge the community are also welcome. This includes presentations on new attack vectors such as microarchitectural side-channels, whose defenses could benefit from compiler techniques.

Specific topics of interest include but are not limited to:

  • Attacker models for secure compiler chains.

  • Secure compiler properties: fully abstract compilation and similar properties, memory safety, control-flow integrity, preservation of safety, information flow and other (hyper-)properties against adversarial contexts, secure multi-language interoperability.

  • Secure interaction between different programming languages: foreign function interfaces, gradual types, securely combining different memory management strategies.

  • Enforcement mechanisms and low-level security primitives: static checking, program verification, typed assembly languages, reference monitoring, program rewriting, software-based isolation/hiding techniques (SFI, crypto-based, randomization-based, OS/hypervisor-based), security-oriented architectural features such as Intel’s SGX, MPX and MPK, capability machines, side-channel defenses, object capabilities.

  • Experimental evaluation and applications of secure compilers.

  • Proof methods relevant to compilation: (bi)simulation, logical relations, game semantics, trace semantics, multi-language semantics, embedded interpreters.

  • Formal verification of secure compilation chains (protection mechanisms, compilers, linkers, loaders), machine-checked proofs, translation validation, property-based testing.

Guidelines for Submitting Extended Abstracts

Extended abstracts should be submitted in PDF format and not exceed 2 pages (references not included). They should be formatted in two-column layout, 10pt font, and be printable on A4 and US Letter sized paper. We recommend using the new acmart LaTeX style in sigplan mode. Submissions are not anonymous and should provide sufficient detail to be assessed by the program committee. Presentation at the workshop does not preclude publication elsewhere.

Contact and More Information

For questions please contact the workshop chairs, Marco Patrignani and Marco Vassena.

Bryan Parno is the Kavčić-Moura Professor of Electrical & Computer Engineering and Computer Science at Carnegie Mellon University, and a Senior Member of ACM and IEEE. After receiving a Bachelor’s degree from Harvard College, he completed his PhD working with Adrian Perrig at Carnegie Mellon University, where his dissertation won the 2010 ACM Doctoral Dissertation Award. He then spent six years as a Researcher in Microsoft Research before returning to CMU, where he was subsequently honored with the Joel and Ruth Spira Excellence in Teaching Award.

Bryan’s research is primarily focused on investigating long-term, fundamental improvements in how to design and build secure systems. In 2011, he was selected for Forbes’ 30-Under-30 Science List. He formalized and worked to optimize cryptographically verifiable computation, receiving a Best Paper Award (and later a Test-of-Time Award) at the IEEE Symposium on Security and Privacy for his advances. He coauthored a book on Bootstrapping Trust in Modern Computers. His work in that area has been incorporated into security enhancements in Intel CPUs, and he received an Intel Test of Time Award for it in 2024. His research into security for new application models was incorporated into Windows and iOS and received two Best Paper Awards. He then extended his interest in bootstrapping trust to the problem of building practical, formally verified secure systems, for which he received four Distinguished Paper Awards. Some of the resulting verified code has found its way into Microsoft, Firefox, Python, the OpenTitan security chip, and the Linux kernel. His other research interests include user authentication, secure network protocols, and security in constrained environments.

Important Dates

  • Short talk proposal submission deadline: January 13th
  • Short talk notification: January 15th
  • PriSC Workshop takes place: Sunday, January 20th

We also have short talks sessions, where participants get 5 minutes to present intriguing ideas, advertise ongoing work, etc. Anyone interested in giving a short 5-minute talk should submit an abstract. Any topic that could be of interest to the emerging secure compilation community is in scope. Presentations that provide a useful outside view or challenge the community are also welcome.

Please sign up here: https://forms.gle/Uy3Rb24YCaA2akBP6.

For questions please contact the workshop chairs, Marco Vassena (m.vassena@uu.nl) and Marco Patrignani (marco.patrignani@unitn.it).