10th Workshop on Principles of Secure Compilation

Today’s computer systems are insecure. The semantics of mainstream low-level languages like C provide no security against devastating vulnerabilities like buffer overflows and control-flow hijacking. Even for safer languages, establishing security with respect to the language’s semantics does not prevent low-level attacks. All the abstraction and security guarantees of the source language may be lost when interacting with low-level code, e.g., when using libraries.

Secure compilation is an emerging field that puts together advances in programming languages, security, verification, systems, compilers, and hardware architectures in order to devise secure compiler chains that eliminate many of today’s low-level vulnerabilities. Secure compilation aims to protect high-level language abstractions in compiled code, even against adversarial low-level contexts, and to allow sound reasoning about security in the source language. The emerging secure compilation community aims to achieve this by:

1. identifying and formalizing properties that secure compilers must possess,
2. devising efficient enforcement mechanisms, and
3. developing effective formal verification techniques.

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

The Workshop on Principles of Secure Compilation (PriSC) is an informal 1-day workshop without 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.

The 10th edition of PriSC will be held on January 11, 2025 in Rennes (France) together with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).

Past editions (all collocated with POPL)

• PriSC 2025, Denver, Colorado, USA, January 20, 2025
• PriSC 2024, London, UK, January 20, 2024
• PriSC 2023, Boston, Massachusetts, USA, January 21, 2023
• PriSC 2022, Philadelphia, Pennsylvania, USA, January 22, 2021
• PriSC 2021, Online, January 17, 2021
• PriSC 2020, New Orleans, Louisiana, USA, January 25, 2020
• PriSC 2019, Cascais/Lisbon, Portugal, January 13, 2019
• PriSC 2018, Los Angeles, USA, January 13, 2018
• Secure Compilation Meeting, Paris, France, January 15, 2017

Accepted Papers

Call for Short Talks

PriSC will feature a short-talk session, where participants can pitch intriguing ideas, advertise ongoing work, open positions, etc.

Anyone interested in giving a short 5-minute talk should sign up here: https://tinyurl.com/rnpypp4j

Important Dates

• Short talk proposal submission deadline: January 7th
• PriSC Workshop: Sunday, January 11th

For questions please contact the workshop chairs, Marco Vassena (m.vassena@uu.nl) and Lesly-Ann Daniel (lesly-ann.daniel@eurecom.fr).

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 build compilers that eliminate many of today’s security vulnerabilities.

Anyone interested in presenting at the workshop should submit an extended abstract (up to 2 pages) covering past, ongoing, or future work. Any topic that could be of interest to secure compilation is in scope. Secure compilation should be interpreted broadly to include techniques that span programming languages, architecture, and systems. This includes presentations on new attack vectors whose defenses could benefit from compiler techniques. Presentations that provide a useful outside view or challenge the community are also welcome. Submitting to the workshop does not preclude publication in other venues, as the workshop does not have public proceedings.

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, and property-based testing.

Guidelines for Submitting Extended Abstracts

Extended abstracts should be submitted in PDF format and not exceed 2 pages (excluding references). 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: Lesly-Ann Daniel and Marco Vassena.

Title: The V8 Sandbox From Compiler Correctness to Runtime Containment

Speaker: Samuel Groß, Google Project Zero

Traditional memory-safety approaches (such as memory-safe languages) offer robust protection against implementation vulnerabilities, but they cannot guarantee the safety of Just-In-Time (JIT) compilers, where the compiler itself is a direct attack surface. For example, in a JavaScript engine, the input is attacker-controlled code, and a single logic bug in the optimization pipeline can trick the JIT into emitting unsafe machine code, regardless of the host language’s guarantees.

In this talk, we present the V8 Sandbox, a practical defense mechanism deployed in the Chromium browser engine. Rather than attempting to formally verify the correctness of the entire V8 optimization pipeline, we shift the security goal from compiler correctness to runtime containment. This in essence allows us to decouple the JIT’s complexity from its security properties. We will discuss the design principles and performance characteristics of this lightweight, in-process sandbox, detail the complexities of retrofitting a new security boundary into an existing and complex codebase, and provide an outlook for future hardening of the sandbox such as hardware support or code validation.

About the speaker. Samuel Groß is a Security Researcher at Google Project Zero, where he specializes in browser security and automated vulnerability discovery as part of the Google Big Sleep project. Previously, he led the V8 Security Team (2022–2025), where he directed the architecture and implementation of defensive mitigations within the V8 JavaScript engine, in particular the V8 Sandbox. Before joining Google in 2019, Samuel gained experience as an independent security researcher, participating in contests such as Pwn2Own and publishing articles in Phrack on JavaScript engine exploitation.