Important Update:

The workshop will be held as a hybrid event with full support for remote participation, following the latest update from the main POPL conference. To attend in person, choose “in-person POPL” option from the main registration page, which later will prompt you to select the specific meetings you want to attend. To participate remotely, choose “Virtual POPL” option which is common to all POPL-week events. Note that in both cases, you will automatically get all the benefits of “Virtual POPL” option, namely, remote access to all POPL-week events as well as the POPL Virtual Workshop. If you are already registered, and wish to either update your information or switch between the in-person and virtual options, use “Update Information” option.

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 low-level adversaries, 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

This will be 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 expect the acceptance rate to be high in the initial editions, so another important role of the PC is to spur interesting submissions. We will also run a short talks session, where participants get 5 minutes to present intriguing ideas and advertise ongoing work.

Keynotes

This year’s keynotes will be (1) “BPF and Spectre: Mitigating transient execution attacks”, by Piotr Krysiuk (Symantec, Threat Hunter Team), Benedict Schlüter (Ruhr University Bochum), and Daniel Borkmann (Isovalent, co-maintainer eBPF) and (2) “Providing evidence for the security properties of hardware/software codesigns” by Frank Piessens (KU Leuven).

History

The idea for this workshop emerged in a small informal meeting at INRIA Paris in August 2016 with in-depth talks and long, synergistic discussions. The first edition of the workshop was held at POPL 2017 under the name of “Secure Compilation Meeting” and had 31 registered participants. The second, third, fourth, and fifth editions were organized at POPL 2018–2021, under the new name of “Workshop on Principles of Secure Compilation” reaching between 40 and 54 registered participants. This growing interest from the community has encouraged us to continue the workshop and starting with the fourth edition, we made PriSC a regular feature with a standing steering committee.

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

Sat 22 Jan

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

09:00 - 10:00
Keynote IPriSC at Independence
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
09:00
60m
Keynote
BPF and Spectre: Mitigating transient execution attacksRemote
PriSC
Piotr Krysiuk Symantec, Threat Hunter Team, Benedict Schlüter Ruhr University Bochum, Daniel Borkmann Isovalent
File Attached
10:20 - 11:35
Attacks and defensesPriSC at Independence
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
10:20
25m
Talk
Type-directed Program Transformation for Constant-Time EnforcementRemote
PriSC
File Attached
10:45
25m
Talk
Towards Understanding Spectre-PHT in Memory-Safe LanguagesRemote
PriSC
Zirui Neil Zhao University of Illinois at Urbana-Champaign, Fangfei Liu Intel Corporation, Scott Constable Intel Corporation, Carlos Rozas Intel Corporation
11:10
25m
Talk
Synthesizing Evidence of Emergent ComputationRemote
PriSC
Scott Moore Galois, Inc., Jennifer Paykin Galois, Inc., Olivier Savary Bélanger Galois, Inc.
Media Attached File Attached
11:35 - 12:00
Short talksPriSC at Independence
Chair(s): Marco Guarnieri IMDEA Software Institute
15:05 - 16:20
Secure compilation theoryPriSC at Independence
Chair(s): Arthur Azevedo de Amorim Boston University
15:05
25m
Talk
Composing Secure CompilersRemote
PriSC
Matthis Kruse CISPA Helmholtz Center for Information Security, Marco Patrignani CISPA Helmholtz Center for Information Security / Stanford University
File Attached
15:30
25m
Talk
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking SimulationRemote
PriSC
Akram El-Korashy Max Planck Institute for Software Systems (MPI-SWS), Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Jérémy Thibault MPI-SP, Adrien Durier Max Planck Institute for Security and Privacy (MPI-SP), Cătălin Hriţcu MPI-SP, Deepak Garg MPI-SWS
Pre-print Media Attached File Attached
15:55
25m
Talk
The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, AbstractlyRemote
PriSC
Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8
DOI Pre-print File Attached
16:40 - 17:55
Secure systemsPriSC at Independence
Chair(s): Marco Guarnieri IMDEA Software Institute
16:40
25m
Talk
A CompCert backend with symbolic encryptionRemote
PriSC
Paolo Torrini INRIA, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
File Attached
17:05
25m
Talk
Effect-Oblivious EquivalenceRemote
PriSC
Yao Li University of Pennsylvania, Stephanie Weirich University of Pennsylvania
Pre-print File Attached
17:30
25m
Talk
The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating codeRemote
PriSC
Dominic Mulligan Arm Research, Nick Spinale Arm Research
File Attached

Call for Presentations

The emerging field of secure compilation aims to preserve security properties of programs when they have been compiled to low-level languages such as assembly, where high-level abstractions don’t exist, and unsafe, unexpected interactions with libraries, other programs, the operating system and even the hardware are possible. For unsafe source languages like C, secure compilation requires careful handling of undefined source-language behavior (like buffer overflows and double frees). Formally, secure compilation aims to protect high-level language abstractions in compiled code, even against low-level adversaries, thus enabling sound reasoning about security in the source language. A complementary goal is to keep the compiled code efficient, often leveraging new hardware security features and advances in compiler design. Other necessary components are identifying and formalizing properties that secure compilers must possess, devising efficient security mechanisms (both software and hardware), and developing effective verification and proof techniques. Research in the field thus puts together advances in compiler design, programming languages, systems security, verification, and computer architecture.

6th Workshop on Principles of Secure Compilation (PriSC 2022)

The Workshop on Principles of Secure Compilation (PriSC) is a relatively new, 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 6th edition of PriSC will be held on January 16 in Philadelphia, Pennsylvania, United State together with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2022.

Keynotes

This year’s keynotes will be (1) “BPF and Spectre: Mitigating transient execution attacks”, by Piotr Krysiuk (Symantec, Threat Hunter Team), Benedict Schlüter (Ruhr University Bochum), and Daniel Borkmann (Isovalent, co-maintainer eBPF) and (2) “Providing evidence for the security properties of hardware/software codesigns” by Frank Piessens (KU Leuven).

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, Jonathan Protzenko and Marco Guarnieri. To make sure you receive such announcements in the future please subscribe to the low-traffic mailing list.

Questions? Use the PriSC contact form.