POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

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)

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

Sat 20 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1PriSC at Turing Lecture
Chair(s): Marco Patrignani University of Trento
09:00
5m
Day opening
Introduction
PriSC
Shweta Shinde ETH Zurich, Marco Patrignani University of Trento
09:05
60m
Keynote
Keynote: Can we reason about the security of concurrent systems code?
PriSC
Peter Sewell University of Cambridge
10:05
25m
Talk
Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
PriSC
Elias Storme KU Leuven, Sander Huyghebaert Vrije Universiteit Brussel, Steven Keuchel Vrije Universiteit Brussel, Thomas Van Strydonck KULeuven, Dominique Devriese KU Leuven
File Attached
10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

10:30 - 11:00
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Session 2PriSC at Turing Lecture
Chair(s): Marco Vassena Utrecht University
11:00
22m
Talk
Microarchitectural Side-Channel Mitigations for Serverless Applications
PriSC
Yayu Wang The University of British Columbia, Aastha Mehta The University of British Columbia
File Attached
11:22
22m
Talk
Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
PriSC
Xaver Fabian Cispa Helmholtz Center for Information Security, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security
File Attached
11:45
22m
Talk
Secure Composition of SPECTRE Mitigations
PriSC
Matthis Kruse CISPA Helmholtz Center for Information Security, Michael Backes Cispa Helmholtz Center for Information Security
File Attached
12:07
22m
Talk
When Obfuscations Preserve Cryptographic Constant-Time
PriSC
Matteo Busi University Ca' Foscari, Venice, Pierpaolo Degano University of Pisa and IMT School for Advanced Studies Lucca, Letterio Galletta IMT School for Advanced Studies Lucca
File Attached
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

12:30 - 14:00
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Session 3PriSC at Turing Lecture
Chair(s): Matteo Busi University Ca' Foscari, Venice
14:00
22m
Talk
Compiler Support for Control-Flow Linearization Using Architectural Mimicry
PriSC
File Attached
14:22
22m
Talk
Modularizing CPU Semantics for Virtualization
PriSC
Paolo G. Giarrusso BedRock Systems, Abhishek Anand BedRock Systems, Gregory Malecha BedRock Systems, František Farka BedRock Systems, Hoang-Hai Dang BedRock Systems
File Attached
14:45
22m
Talk
All the Binaries Together: A Semantic Approach to Application Binary Interfaces
PriSC
Andrew Wagner Northeastern University, Amal Ahmed Northeastern University, USA
File Attached
15:07
22m
Talk
Short Talks
PriSC

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Session 4PriSC at Turing Lecture
Chair(s): Dominique Devriese KU Leuven
16:00
22m
Talk
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
Robert Künnemann CISPA Helmholtz Center for Information Security, Ethan Cecchetti University of Wisconsin-Madison
File Attached
16:22
22m
Talk
Gradual Verification for Smart Contracts
PriSC
Haojia Sun Shanghai Jiao Tong University, Kunal Singh Carnegie Mellon University, Jan-Paul Ramos-Davila Cornell University, Jonathan Aldrich Carnegie Mellon University, Jenna DiVincenzo (Wise) Purdue University
File Attached
16:45
22m
Talk
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
Hoang-Hai Dang BedRock Systems, David Swasey BedRock Systems, Gregory Malecha BedRock Systems
File Attached
17:07
8m
Day closing
Closing Remarks
PriSC
Shweta Shinde ETH Zurich

Accepted Papers

Title
All the Binaries Together: A Semantic Approach to Application Binary Interfaces
PriSC
File Attached
Closing Remarks
PriSC
Compiler Support for Control-Flow Linearization Using Architectural Mimicry
PriSC
File Attached
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
File Attached
Gradual Verification for Smart Contracts
PriSC
File Attached
Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
PriSC
File Attached
Microarchitectural Side-Channel Mitigations for Serverless Applications
PriSC
File Attached
Modularizing CPU Semantics for Virtualization
PriSC
File Attached
Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
PriSC
File Attached
Secure Composition of SPECTRE Mitigations
PriSC
File Attached
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
File Attached
When Obfuscations Preserve Cryptographic Constant-Time
PriSC
File Attached

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.

8th Workshop on Principles of Secure Compilation (PriSC 2024)

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 8th edition of PriSC will be held on January 20, 2024 in London, United Kingdom 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 Shweta Shinde.