Write a Blog >>

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

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

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00: KeynotePriSC at Rosalie
09:00 - 09:05
Day opening
PriSC Introduction
PriSC
Dominique DevrieseVrije Universiteit Brussel
File Attached
09:05 - 10:00
Industry talk
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
PriSC
Media Attached
10:00 - 10:30: Saturday Morning BreakCatering at Break
10:30 - 12:30: Foundations and timing channelsPriSC at Rosalie
Chair(s): Marco VassenaCISPA Helmholtz Center for Information Security
10:30 - 10:54
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute
Media Attached File Attached
10:54 - 11:18
Talk
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine AbateInria Paris, Roberto BlancoInria, Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniStanford University & CISPA , Éric TanterUniversity of Chile, Jérémy ThibaultInria Paris
Media Attached File Attached
11:18 - 11:42
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan BayAarhus University, Aslan AskarovAarhus University
Media Attached File Attached
11:42 - 12:06
Talk
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis LarsenDIKU, University of Copenhagen, Torben MogensenDIKU, University of Copenhagen, Michael Kirkedal ThomsenDIKU, University of Copenhagen
12:06 - 12:30
Talk
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA
Media Attached
12:30 - 14:00: Saturday LunchCatering at Lunch Room
12:30 - 14:00
Lunch
Lunch
Catering
14:00 - 15:05: New outlooks on secure compilationPriSC at Rosalie
Chair(s): Cristina CifuentesOracle Labs
14:00 - 14:24
Talk
Exploits as Insecure Compilation
PriSC
Jennifer PaykinGalois, Inc., Eric MertensGalois, Inc., Mark TullsenGalois, Inc, Luke MaurerGalois, Inc, Benoit RazetGalois, Inc, Alexander BakstGalois, Inc, Scott MooreGalois, Inc
Pre-print Media Attached File Attached
14:24 - 14:48
Talk
Universal Composability is Secure Compilation
PriSC
Marco PatrignaniStanford University & CISPA , Riad S. WahbyStanford University, USA, Robert KünnemannCISPA, Saarland University
Media Attached File Attached
14:48 - 14:56
Talk
Short Talk: Automatically Eliminating Speculative Leaks With Blade
PriSC
Marco VassenaCISPA Helmholtz Center for Information Security, Klaus v. GleissenthallUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA
Media Attached File Attached
14:56 - 15:04
Talk
Short Talk: Everparse
PriSC
Tahina RamananandroMicrosoft Research, n.n.
Media Attached
15:05 - 15:35: Saturday Afternoon BreakCatering at Break
15:35 - 17:45: Compartmentalization, memory safety, and isolationPriSC at Rosalie
Chair(s): Marco PatrignaniStanford University & CISPA , Jonathan ProtzenkoMicrosoft Research, Redmond
15:35 - 15:59
Talk
Flexible Tag-based Policies for Compartmentalized C
PriSC
Sean AndersonPortland State University, Andrew TolmachPortland State University, CHR ChhakPortland State University
Media Attached File Attached
15:59 - 16:23
Talk
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn GeorgesAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached
16:23 - 16:47
Talk
Securing Interruptible Enclaves
PriSC
Matteo BusiUniversità di Pisa - Dipartimento di Informatica, Job Noormanimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulckimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio GallettaIMT School for Advanced Studies, Pierpaolo DeganoUniversità di Pisa - Dipartimento di Informatica, Jan Tobias Mühlbergimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank PiessensKU Leuven
Media Attached File Attached
16:47 - 16:57
Break
Mini-break
PriSC
16:57 - 17:21
Talk
WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
PriSC
Jay BosamiyaCarnegie Mellon University, Benjamin LimCarnegie Mellon University, Bryan ParnoCarnegie Mellon University
Media Attached File Attached
17:21 - 17:45
Talk
Memory Safety Preservation for WebAssembly
PriSC
Marco VassenaCISPA Helmholtz Center for Information Security, Marco PatrignaniStanford University & CISPA
Link to publication 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 https://prisc2020short.hotcrp.com/.

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: https://lists.gforge.inria.fr/mailman/listinfo/prisc-announce

Accepted Talks

Title
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
PriSC
Media Attached
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Media Attached
Exorcising Spectres with Secure Compilers
PriSC
Media Attached File Attached
Exploits as Insecure Compilation
PriSC
Pre-print Media Attached File Attached
Flexible Tag-based Policies for Compartmentalized C
PriSC
Media Attached File Attached
Hermes: Implementing Cryptography without Side-channels
PriSC
Mechanized Reasoning about a Capability Machine
PriSC
Media Attached
Memory Safety Preservation for WebAssembly
PriSC
Link to publication Media Attached File Attached
Reconciling progress-insensitive noninterference and declassification
PriSC
Media Attached File Attached
Securing Interruptible Enclaves
PriSC
Media Attached File Attached
Short Talk: Automatically Eliminating Speculative Leaks With Blade
PriSC
Media Attached File Attached
Short Talk: Everparse
PriSC
Media Attached
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Media Attached File Attached
Universal Composability is Secure Compilation
PriSC
Media Attached File Attached
WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
PriSC
Media Attached File Attached