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

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.