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)

• 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 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.