PriSC 2020 - Principles of Secure Compilation 2020 - POPL 2020

PriSC 2020 - Principles of Secure Compilation 2020 - POPL 2020
Write a Blog >>
POPL 2020
Sun 19 - Sat 25 January 2020
New Orleans, Louisiana, United States
Attending
Venue: JW Marriott New Orleans
Restaurant: Palace Cafe
Registration
Online Participation
Travel to the USA
Mentoring Events
Information for Students
Code of Conduct
Supporting POPL
SIGPLAN CARES
Program
POPL Program
Your Program
Filter by Day
Sun 19 Jan
Mon 20 Jan
Tue 21 Jan
Wed 22 Jan
Thu 23 Jan
Fri 24 Jan
Sat 25 Jan
Tracks
POPL 2020
Research Papers
Artifact Evaluation
Student Research Competition
Workshops and Co-located Events
TutorialFest
POPLmark 15 Year Retrospective Panel
Ally Skills Session
LGBTQ Lunch
Mentoring Breakfasts
W@POPL Dinner
Student Volunteers
Co-hosted Conferences
CPP
VMCAI
Workshops
ADSL
CoqPL
HASE
LAFI
(né PPS)
PEPM
PLanQC
PLMW
PriSC
PriSC
Principles of Secure Compilation
- Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
WGT
Co-hosted Symposia
PADL
Organization
POPL 2020 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
Artifact Evaluation
Student Research Competition
TutorialFest
POPLmark 15 Year Retrospective Panel
Panel
Organizing Committee
Ally Skills Session
LGBTQ Lunch
Mentoring Breakfasts
W@POPL Dinner
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Artifact-Evaluation Committee
Steering Committee
Workshops
ADSL
Organizing Committee
Program Committee
CoqPL
Invited speakers
Organizing Committee
Program Committee
HASE
Organizing Committee
Program Committee
LAFI
Program Committee
Steering Committee
PEPM
PC Chairs
Program Committee
PLanQC
Organizing Committee
Program Committee
PLMW
Organizing Committee
Invited speakers
Panelists
PriSC
Program Committee
Steering Committee
WGT
Organizing Committee
Program Committee
Co-hosted Symposia
PADL
Program Chairs
Program Committee
Publicity Chair
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 2020
series
) /
PriSC 2020 (
series
) /
Principles of Secure Compilation 2020
PriSC 2020
About
Program
Accepted Talks
Call for Presentations
Call for Short Talks
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: (1) identifying and formalizing properties that secure compilers must possess; (2) devising efficient enforcement mechanisms; and (3) developing effective formal verification techniques.
Format
This will be an informal 1-day 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.
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”
. The second and third edition were organized at
POPL 2018
and
2019
, under the new name of “Workshop on Principles of Secure Compilation”. This increasing interest from the community has encouraged us to continue the workshop and starting with the upcoming edition, we are making PriSC a regular feature with a standing steering committee.
Keynote this year
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
Tyler McMullen
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
Sat 25 Jan
Displayed time zone:
Saskatchewan, Central America
change
09:00 - 10:00
Keynote
PriSC
at
Rosalie
09:00
5m
Day opening
PriSC Introduction
PriSC
Dominique Devriese
Vrije Universiteit Brussel
File Attached
09:05
55m
Industry talk
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
PriSC
K:
Tyler McMullen
Fastly
Media Attached
10:00 - 10:30
Saturday Morning Break
Catering
at
Break
10:30 - 12:30
Foundations and timing channels
PriSC
at
Rosalie
Chair(s):
Marco Vassena
CISPA Helmholtz Center for Information Security
10:30
24m
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco Patrignani
Stanford University & CISPA
Marco Guarnieri
IMDEA Software Institute
Media Attached
File Attached
10:54
24m
Talk
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine Abate
Inria Paris
Roberto Blanco
Inria
Ștefan Ciobâcă
Alexandru Ioan Cuza University of Iasi
Deepak Garg
Max Planck Institute for Software Systems
Cătălin Hriţcu
Inria Paris
Marco Patrignani
Stanford University & CISPA
Éric Tanter
University of Chile
Jérémy Thibault
Inria Paris
Media Attached
File Attached
11:18
24m
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan Bay
Aarhus University
Aslan Askarov
Aarhus University
Media Attached
File Attached
11:42
24m
Talk
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis Larsen
DIKU, University of Copenhagen
Torben Mogensen
DIKU, University of Copenhagen
Michael Kirkedal Thomsen
DIKU, University of Copenhagen
File Attached
12:06
24m
Talk
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine Blazy
Univ Rennes- IRISA
Rémi Hutin
IRISA / ENS Rennes
David Pichardie
Univ Rennes, ENS Rennes, IRISA
Media Attached
12:30 - 14:00
Saturday Lunch
Catering
at
Lunch Room
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:05
New outlooks on secure compilation
PriSC
at
Rosalie
Chair(s):
Cristina Cifuentes
Oracle Labs
14:00
24m
Talk
Exploits as Insecure Compilation
PriSC
Jennifer Paykin
Galois, Inc.
Eric Mertens
Galois, Inc.
Mark Tullsen
Galois, Inc
Luke Maurer
Galois, Inc
Benoit Razet
Galois, Inc
Alexander Bakst
Galois, Inc
Scott Moore
Galois, Inc
Pre-print
Media Attached
File Attached
14:24
24m
Talk
Universal Composability is Secure Compilation
PriSC
Marco Patrignani
Stanford University & CISPA
Riad S. Wahby
Stanford University, USA
Robert Künnemann
CISPA, Saarland University
Media Attached
File Attached
14:48
8m
Talk
Short Talk: Automatically Eliminating Speculative Leaks With Blade
PriSC
Marco Vassena
CISPA Helmholtz Center for Information Security
Klaus v. Gleissenthall
University of California at San Diego, USA
Rami Gökhan Kıcı
University of California at San Diego, USA
Media Attached
File Attached
14:56
8m
Talk
Short Talk: Everparse
PriSC
Tahina Ramananandro
Microsoft Research, n.n.
Media Attached
15:05 - 15:35
Saturday Afternoon Break
Catering
at
Break
15:35 - 17:45
Compartmentalization, memory safety, and isolation
PriSC
at
Rosalie
Chair(s):
Marco Patrignani
Stanford University & CISPA
Jonathan Protzenko
Microsoft Research, Redmond
15:35
24m
Talk
Flexible Tag-based Policies for Compartmentalized C
PriSC
Sean Anderson
Portland State University
Andrew Tolmach
Portland State University
CHR Chhak
Portland State University
Media Attached
File Attached
15:59
24m
Talk
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn Georges
Aarhus University
Alix Trieu
Aarhus University
Lars Birkedal
Aarhus University
Media Attached
16:23
24m
Talk
Securing Interruptible Enclaves
PriSC
Matteo Busi
Università di Pisa - Dipartimento di Informatica
Job Noorman
imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium
Jo Van Bulck
imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium
Letterio Galletta
IMT School for Advanced Studies
Pierpaolo Degano
Università di Pisa - Dipartimento di Informatica
Jan Tobias Mühlberg
imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium
Frank Piessens
KU Leuven
Media Attached
File Attached
16:47
10m
Break
Mini-break
PriSC
16:57
24m
Talk
WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
PriSC
Jay Bosamiya
Carnegie Mellon University
Benjamin Lim
Carnegie Mellon University
Bryan Parno
Carnegie Mellon University
Media Attached
File Attached
17:21
24m
Talk
Memory Safety Preservation for WebAssembly
PriSC
Marco Vassena
CISPA Helmholtz Center for Information Security
Marco Patrignani
Stanford University & CISPA
Link to publication
Media Attached
File Attached
Accepted Talks
Title
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine Blazy
Rémi Hutin
David Pichardie
Media Attached
Exorcising Spectres with Secure Compilers
PriSC
Marco Patrignani
Marco Guarnieri
Media Attached
File Attached
Exploits as Insecure Compilation
PriSC
Jennifer Paykin
Eric Mertens
Mark Tullsen
Luke Maurer
Benoit Razet
Alexander Bakst
Scott Moore
Pre-print
Media Attached
File Attached
Flexible Tag-based Policies for Compartmentalized C
PriSC
Sean Anderson
Andrew Tolmach
CHR Chhak
Media Attached
File Attached
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis Larsen
Torben Mogensen
Michael Kirkedal Thomsen
File Attached
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
PriSC
K:
Tyler McMullen
Media Attached
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn Georges
Alix Trieu
Lars Birkedal
Media Attached
Memory Safety Preservation for WebAssembly
PriSC
Marco Vassena
Marco Patrignani
Link to publication
Media Attached
File Attached
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan Bay
Aslan Askarov
Media Attached
File Attached
Securing Interruptible Enclaves
PriSC
Matteo Busi
Job Noorman
Jo Van Bulck
Letterio Galletta
Pierpaolo Degano
Jan Tobias Mühlberg
Frank Piessens
Media Attached
File Attached
Short Talk: Automatically Eliminating Speculative Leaks With Blade
PriSC
Marco Vassena
Klaus v. Gleissenthall
Rami Gökhan Kıcı
Media Attached
File Attached
Short Talk: Everparse
PriSC
Tahina Ramananandro
Media Attached
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine Abate
Roberto Blanco
Ștefan Ciobâcă
Deepak Garg
Cătălin Hriţcu
Marco Patrignani
Éric Tanter
Jérémy Thibault
Media Attached
File Attached
Universal Composability is Secure Compilation
PriSC
Marco Patrignani
Riad S. Wahby
Robert Künnemann
Media Attached
File Attached
WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
PriSC
Jay Bosamiya
Benjamin Lim
Bryan Parno
Media Attached
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 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.
4th Workshop on Principles of Secure Compilation (PriSC 2020)
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 4th edition of PriSC will be held on January 25 in New Orleans, Louisiana USA together with the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2020.
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,
Dominique Devriese
and
Deian Stefan
To make sure you receive such announcements in the future please subscribe to the
low-traffic mailing list
Call for Short Talks
Important Dates
Short talk proposal submission deadline: January 13th 2020
Short talk notification: January 15th 2020
PriSC Workshop takes place: Sunday, January 25th 2020
Call for Short Talks
We also have a short talks session, where participants get 5 minutes to present intriguing ideas, advertise ongoing work, etc. Anyone interested in giving a short 5-minute talk should submit an abstract. Any topic that could be of interest to the emerging secure compilation community is in scope. Presentations that provide a useful outside view or challenge the community are also welcome.
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 Short Talk Abstracts
Abstracts should be short and in PDF format. A few paragraphs will suffice. They should not exceed 1 page in length. Abstracts are not reviewed anonymously.
Giving a short talk at the workshop does not preclude publication elsewhere.
Please submit your extended abstracts at
Contact and More Information
For questions please contact the workshop chairs, Dominique Devriese (
dominique.devriese@vub.be
) and Deian Stefan (
deian@cs.ucsd.edu
).
To make sure you receive such announcements in the future please subscribe to the following low-traffic mailing list:
Important Dates
AoE (UTC-12h)
Sat 25 Jan 2020
Workshop
Wed 20 Nov 2019
Notification
Fri 1 Nov 2019
Submission deadline
Submission Link
Program Committee
Dominique Devriese
Program Co-Chair
Vrije Universiteit Brussel
Belgium
Deian Stefan
Program Co-Chair
University of California San Diego
Aslan Askarov
Aarhus University
Frédéric Besson
Sandrine Blazy
Univ Rennes- IRISA
France
David Chisnall
University of Cambridge
Stephen Chong
Harvard University
United States
Cristina Cifuentes
Oracle Labs
Australia
Tal Garfinkel
Stanford University
Klaus Gleissenthall
University of California, San Diego
Benjamin Gregoire
INRIA
Limin Jia
Carnegie Mellon University
United States
Daniel Patterson
Northeastern University
United States
Jonathan Protzenko
Microsoft Research, Redmond
United States
Marco Vassena
CISPA Helmholtz Center for Information Security
Germany
Steering Committee
Dominique Devriese
Vrije Universiteit Brussel
Belgium
Deepak Garg
Max Planck Institute for Software Systems
Germany
Michael Hicks
University of Maryland
United States
Cătălin Hriţcu
Chair
Inria Paris
France
Santosh Nagarakatte
Rutgers University, USA
United States
Jonathan Protzenko
Microsoft Research, Redmond
United States
Tamara Rezk
Inria
France
Deian Stefan
University of California San Diego
Fri 24 Apr 15:08