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)

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

Sat 21 Jan

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

09:00 - 10:30
Session 1PriSC at Park
Chair(s): Marco Guarnieri IMDEA Software Institute
09:00
5m
Day opening
Introduction
PriSC

09:05
60m
Keynote
Semantic Intermediate Representations for Sound Language Interoperability
PriSC
Amal Ahmed Northeastern University, USA
Pre-print
10:05
25m
Talk
Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
PriSC
Farzaneh Derakhshan Carnegie Mellon University, Zichao Zhang Carnegie Mellon University, Amit Vasudevan Carnegie Mellon University, Limin Jia Carnegie Mellon University
File Attached
11:00 - 12:30
Session 2PriSC at Park
Chair(s): Cătălin Hriţcu MPI-SP
11:00
25m
Talk
Automated Learning and Verification of Embedded Security Architectures
PriSC
Matteo Busi University Ca' Foscari, Venice, Riccardo Focardi University Ca' Foscari, Venice, Flaminia L. Luccio University Ca' Foscari, Venice
File Attached
11:25
25m
Talk
pi_RA: A pi-calculus for verifying protocols that use remote attestation
PriSC
Emiel Lanckriet KU Leuven, Matteo Busi University Ca' Foscari, Venice, Dominique Devriese KU Leuven
File Attached
11:50
25m
Talk
Robust Constant-Time Cryptography
PriSC
Matthew Kolosick University of California at San Diego, Basavesh Ammanaghatta Shivakumar Max Planck Institute for Security and Privacy (MPI-SP), Sunjay Cauligi University of California at San Diego, USA, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego
Pre-print
12:15
15m
Talk
Short Talk: Generalising secure compilation criteria
PriSC
Emiel Lanckriet KU Leuven
16:00 - 17:30
Session 4PriSC at Park
Chair(s): Matteo Busi University Ca' Foscari, Venice
16:00
25m
Talk
Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
PriSC
Michael Smith UC San Diego, Abhishek Sharma UC San Diego, John Renner University of California at San Diego, USA, David Thien UC San Diego, Sorin Lerner University of California at San Diego, Fraser Brown CMU, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego
File Attached
16:25
25m
Talk
FaJITa: Verifying Optimizations on Just-In-Time Programs
PriSC
David Thien UC San Diego, Michael Smith UC San Diego, Evan Johnson University of California at San Diego; Arm, Sorin Lerner University of California at San Diego, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego, Fraser Brown CMU
Pre-print File Attached
16:50
25m
Talk
Universally Composable Security for Program Partitioning
PriSC
Coşku Acay Cornell University, Joshua Gancher Carnegie Mellon University, Rolph Recto Cornell University, Andrew Myers Cornell University
File Attached

Accepted Papers

Title
Automated Learning and Verification of Embedded Security Architectures
PriSC
File Attached
Blame-Preserving Secure Compilation
PriSC
Pre-print
Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
PriSC
File Attached
FaJITa: Verifying Optimizations on Just-In-Time Programs
PriSC
Pre-print File Attached
pi_RA: A pi-calculus for verifying protocols that use remote attestation
PriSC
File Attached
Robust Constant-Time Cryptography
PriSC
Pre-print
SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
PriSC
Pre-print Media Attached File Attached
Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed InterfacesRecorded
PriSC
Pre-print File Attached
Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
PriSC
File Attached
Universally Composable Security for Program Partitioning
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.

7th Workshop on Principles of Secure Compilation (PriSC 2023)

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 7th edition of PriSC will be held on January 21, 2023 in Boston, Massachusetts, United State 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 Guarnieri and Shweta Shinde.

Questions? Use the PriSC contact form.