PriSC 2021 - POPL 2021
Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021
Online
Attending
Venue: Online (How to POPL in 2021)
Supporting POPL
Student Volunteers
Code of Conduct
Registration
FAQ
Program
POPL Program
Your Program
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Wed 20 Jan
Thu 21 Jan
Fri 22 Jan
Tracks
POPL 2021
POPL
Artifact Evaluation
Workshops and Co-located Events
TutorialFest
Student Research Competition
Student Volunteers
POPL Meetups
Co-hosted Conferences
CPP
CPP
CPP
Lightning Talks
PLMW
VMCAI
Workshops
CoqPL
LAFI
PEPM
PriSC
Co-hosted Symposia
PADL
Organization
POPL 2021 Committees
Organizing Committee
Track Committees
POPL
Artifact Evaluation
TutorialFest
Student Research Competition
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Organization Committee
Program Committee
Steering Committee
PLMW
Invited Speakers
Panelists
Organizing Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Invited speaker
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PriSC
Program Committee
Steering Committee
Co-hosted Symposia
PADL
Programme Chairs
Programme Committee
Series
Series
POPL 2027
POPL 2026
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
POPL 2021
series
) /
PriSC 2021 (
series
) /
PriSC 2021
About
Program
Accepted Papers
Call for Presentations
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:
identifying and formalizing properties that secure compilers must possess;
devising efficient enforcement mechanisms; and
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.
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
, and
fourth
editions were organized at POPL 2018–2020, 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.
Highlights
Plenary
Program Display Configuration
Close
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
15:30 - 16:00
Social
Workshops and Co-located Events
at
Break
15:30
30m
Social Event
Sunday Breakfast Tables
Workshops and Co-located Events
16:00 - 17:30
Secure compilers & cryptography
PriSC
at
PriSC
Chair(s):
Fraser Brown
Stanford University, USA
Aastha Mehta
MPI-SWS, Germany and University of British Columbia, Canada
16:00
18m
Talk
High-level high-speed high-assurance crypto
PriSC
Jonathan Cogan
Stanford
Fraser Brown
Stanford University, USA
Alex Ozdemir
Stanford
Riad S. Wahby
Stanford University, USA
Media Attached
16:18
18m
Talk
Cross-Architecture Testing for Compiler-Introduced Security Bugs
PriSC
Jianhao Xu
Nanjing University
Kangjie Lu
University of Minnesota
Bing Mao
Nanjing University
Media Attached
File Attached
16:36
18m
Talk
High-Assurance Cryptography in the Spectre Era
PriSC
Gilles Barthe
MPI-SP, Germany / IMDEA Software Institute, Spain
Sunjay Cauligi
University of California at San Diego, USA
Benjamin Gregoire
INRIA
Adrien Koutsos
INRIA Paris
Kevin Liao
Max Planck Institute for Security and Privacy
Tiago Oliveira
University of Porto (FCUP) and INESC TEC
Swarn Priya
Purdue University
Tamara Rezk
Inria, France
Peter Schwabe
Max Planck Institute for Security and Privacy
Media Attached
16:54
18m
Talk
Compilation as Multi-Language Semantics
PriSC
William J. Bowman
University of British Columbia
Pre-print
Media Attached
17:12
18m
Talk
Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
PriSC
Coşku Acay
Cornell University
Rolph Recto
Joshua Gancher
Cornell University
Andrew Myers
Cornell University
Elaine Shi
Cornell University
Media Attached
17:30 - 18:00
Social
Workshops and Co-located Events
at
Break
17:30
30m
Break
Sunday Coffee Break
Workshops and Co-located Events
18:00 - 19:00
Invited talk
PriSC
at
PriSC
Chair(s):
Deian Stefan
University of California at San Diego, USA
18:00
60m
Keynote
Frontiers in Secure Compilation – an Industrial Perspective (invited talk)
PriSC
Hugo Vincent
Arm Research
19:00 - 20:30
Formal analysis & proof techniques
PriSC
at
PriSC
Chair(s):
Marco Patrignani
Stanford University, USA / CISPA, Germany
Jonathan Protzenko
Microsoft Research, Redmond
19:00
18m
Talk
Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs
PriSC
Jérémy Thibault
MPI-SP
Cătălin Hriţcu
MPI-SP
Pre-print
Media Attached
19:18
18m
Talk
Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis
PriSC
Marc Gourjon
Hamburg University of Technology and NXP Semiconductors Germany GmbH
Media Attached
19:36
18m
Talk
Secure Optimization Through Opaque Observations
PriSC
Son Tuan Vu
Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6
Albert Cohen
Google
Karine Heydemann
Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6
Arnaud de Grandmaison
ARM
Christophe Guillon
STMicroelectronics
Pre-print
Media Attached
File Attached
19:54
18m
Talk
The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
PriSC
Carmine Abate
Max Planck Institute for Security and Privacy, Bochum, Germany
Matteo Busi
Università di Pisa - Dipartimento di Informatica
Pre-print
Media Attached
File Attached
20:12
18m
Talk
Toward Complete Stack Safety for Capability Machines
PriSC
Aina Linn Georges
Aarhus University
Armaël Guéneau
Aarhus University
Alix Trieu
Aarhus University
Lars Birkedal
Aarhus University
Media Attached
File Attached
19:30 - 20:00
Social
Workshops and Co-located Events
at
Break
19:30
30m
Social Event
Sunday Hallway Time
Workshops and Co-located Events
21:00 - 21:30
Short talks
PriSC
at
PriSC
Chair(s):
Deian Stefan
University of California at San Diego, USA
21:00
15m
Talk
A Categorical Approach to Secure Compilation (and others things) (short talk)
PriSC
Stelios Tsampas
Andreas Nuyts
KU Leuven, Belgium
Dominique Devriese
Vrije Universiteit Brussel
Frank Piessens
KU Leuven
21:15
15m
Talk
Contract-aware Secure Compilation (short talk)
PriSC
Marco Guarnieri
ETH Zurich, Switzerland
Marco Patrignani
Stanford University, USA / CISPA, Germany
Pre-print
Accepted Papers
Title
Compilation as Multi-Language Semantics
PriSC
William J. Bowman
Pre-print
Media Attached
Cross-Architecture Testing for Compiler-Introduced Security Bugs
PriSC
Jianhao Xu
Kangjie Lu
Bing Mao
Media Attached
File Attached
Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis
PriSC
Marc Gourjon
Media Attached
High-Assurance Cryptography in the Spectre Era
PriSC
Gilles Barthe
Sunjay Cauligi
Benjamin Gregoire
Adrien Koutsos
Kevin Liao
Tiago Oliveira
Swarn Priya
Tamara Rezk
Peter Schwabe
Media Attached
High-level high-speed high-assurance crypto
PriSC
Jonathan Cogan
Fraser Brown
Alex Ozdemir
Riad S. Wahby
Media Attached
Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs
PriSC
Jérémy Thibault
Cătălin Hriţcu
Pre-print
Media Attached
Secure Optimization Through Opaque Observations
PriSC
Son Tuan Vu
Albert Cohen
Karine Heydemann
Arnaud de Grandmaison
Christophe Guillon
Pre-print
Media Attached
File Attached
The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
PriSC
Carmine Abate
Matteo Busi
Pre-print
Media Attached
File Attached
Toward Complete Stack Safety for Capability Machines
PriSC
Aina Linn Georges
Armaël Guéneau
Alix Trieu
Lars Birkedal
Media Attached
File Attached
Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
PriSC
Coşku Acay
Rolph Recto
Joshua Gancher
Andrew Myers
Elaine Shi
Media 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 adversarial low-level contexts, 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.
5th Workshop on Principles of Secure Compilation (PriSC 2021)
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 5th edition of PriSC will be held on January 17 in Copenhagen, Denmark together with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2021.
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 including). 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
Deian Stefan
To make sure you receive such announcements in the future please subscribe to the
low-traffic mailing list
Questions? Use the
PriSC contact form
Publication links
YouTube Playlist
Important Dates
AoE (UTC-12h)
Sun 17 Jan 2021
Workshop
Wed 25 Nov 2020
Notifications
Fri 30 Oct 2020
Submission deadline
Submission Link
Program Committee
Amal Ahmed
Northeastern University, USA
United States
Andrew W.
Appel
Princeton
Fraser Brown
Stanford University, USA
Delphine Demange
Univ Rennes, Inria, CNRS, IRISA
France
Nick Fitzgerald
Marco Gaboardi
Boston University
United States
Marco Guarnieri
IMDEA Software Institute
Spain
Chung-Kil Hur
Seoul National University, South Korea
Xavier Leroy
Collège de France
France
Aastha Mehta
MPI-SWS, Germany and University of British Columbia, Canada
Santosh Nagarakatte
Rutgers University, USA
Zoe Paraskevopoulou
Princeton University
United States
Jennifer Paykin
Galois, Inc.
United States
Jonathan Protzenko
Microsoft Research, Redmond
United States
Tamara Rezk
Inria, France
Andreas Rossberg
Dfinity Stiftung
Germany
Ilya Sergey
Yale-NUS College and National University of Singapore
Singapore
Shweta Shinde
ETH Zurich
Switzerland
Deian Stefan
University of California at San Diego, USA
Conrad Watt
University of Cambridge, UK
Steering Committee
Dominique Devriese
Vrije Universiteit Brussel
Belgium
Deepak Garg
Max Planck Institute for Software Systems
Germany
Michael Hicks
University of Maryland at College Park
Cătălin Hriţcu
MPI-SP
Germany
Santosh Nagarakatte
Rutgers University, USA
Jonathan Protzenko
Microsoft Research, Redmond
United States
Tamara Rezk
Inria, France
Deian Stefan
University of California at San Diego, USA
Fri 24 Apr 15:14