Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

Workshop description

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 are currently 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.

The goal of this informal 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 enforcement mechanisms for secure compilation.

Format

The 3rd Workshop on Principles of Secure Compilation (PriSC) is an informal 1-day workshop without any proceedings. Anyone interested in presenting at the workshop can submit an extended abstract (up to 2 pages). We will also run a short talks session, where participants get 5 minutes to present intriguing ideas and advertise ongoing work. Presentation at the workshop of course does not preclude publication elsewhere.

Call for Presentations

https://popl19.sigplan.org/track/prisc-2019#Call-for-Presentations

Mailing list

For receiving future announcements about PriSC please subscribe to the following low-traffic mailing list: https://lists.gforge.inria.fr/mailman/listinfo/prisc-announce

History

The idea for this workshop emerged in a small highly 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”. This raised significant interest from the community, which convinced us to organize this workshop every year, since 2018 under the name of “Principles of Secure Compilation (PriSC)”.

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

Sun 13 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Session 1PriSC at Sala VI
Chair(s): Deepak Garg Max Planck Institute for Software Systems
09:00
60m
Talk
PriSC Keynote - Jasmin: A Compiler and Framework for High-Assurance and High-Speed Cryptography
PriSC
File Attached
10:00
30m
Talk
Towards Secure Compilation of Power Side-Channel Countermeasures
PriSC
Marc Gourjon Hamburg University of Technology and NXP Semiconductors Germany GmbH
File Attached
11:00 - 12:30
Session 2PriSC at Sala VI
Chair(s): Dominique Devriese Vrije Universiteit Brussel, Belgium
11:00
30m
Talk
Trestle: Bridging the Performance and Safety Divide in WebAssembly
PriSC
Craig Disselkoen University of California San Diego, Tal Garfinkel Stanford University, Deian Stefan University of California San Diego, Conrad Watt University of Cambridge
File Attached
11:30
30m
Talk
Protecting C++ Applications Using CHERI
PriSC
Khilan Gudka University of Cambridge, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge
File Attached
12:00
30m
Talk
Secure Linking in the CheriBSD Operating System
PriSC
Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge
File Attached
14:00 - 15:30
Session 3PriSC at Sala VI
Chair(s): Chung-Kil Hur Seoul National University
14:00
30m
Talk
Translation Validation for Security Properties
PriSC
Matteo Busi Università di Pisa - Dipartimento di Informatica, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Letterio Galletta IMT School for Advanced Studies
Pre-print File Attached
14:30
30m
Talk
Security Witnesses for Compiler Transformations
PriSC
Kedar Namjoshi Bell Labs, Nokia, Lucas M. Tabajara Rice University
File Attached
15:00
30m
Talk
A Data Layout Description Language for Cogent
PriSC
Zilin Chen Data61, CSIRO and UNSW, Matthew Di Meglio UNSW, Liam O'Connor UNSW, Partha Susarla Data61, CSIRO, Christine Rizkallah UNSW, Gabriele Keller Utrecht University
16:00 - 18:00
Session 4PriSC at Sala VI
Chair(s): David Naumann Stevens Institute of Technology, Aslan Askarov Aarhus University
16:00
30m
Other
Short Talks Session
PriSC

16:30
30m
Talk
Modular Security Guarantees for Low-Level Languages with Stack Traversal
PriSC
Mathias Vorreiter Pedersen Aarhus University, Aslan Askarov Aarhus University
File Attached
17:00
30m
Talk
Confidentiality-Preserving Refinement
PriSC
File Attached
17:30
30m
Talk
(Un)Encrypted Computing and Indistinguishability Obfuscation
PriSC
Peter Breuer Hecusys LLC, Jonathan Bowen London South Bank University
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.

3rd Workshop on Principles of Secure Compilation (PriSC 2019)

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 3rd edition of PriSC will be held in Lisbon, together with the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), on January 13th, 2019.

More information is available at https://popl19.sigplan.org/track/prisc-2019

Important Dates

  • Presentation proposal submission deadline: 17 October 2018, AoE
  • Presentation proposal notification: 10 November 2018
  • PriSC Workshop takes place: Sunday, 13 January 2019

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. 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: http://www.sigplan.org/sites/default/files/acmart/current/acmart-sigplanproc.zip

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.

Please submit your extended abstracts at https://prisc19.hotcrp.com/.

Contact and More Information

For questions please contact the workshop chairs, Dominique Devriese (dominique.devriese@cs.kuleuven.be) and Deepak Garg (dg@mpi-sws.org).

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

Call for Short Talks

Important Dates

  • Short talk proposal submission deadline: January 13th 2019
  • Short talk notification: January 13th 2019
  • PriSC Workshop takes place: Sunday, January 13th 2019

Call for Short Talks

We plan to 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 may 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 reviewed by the PC chairs only, non-anonymously.

Giving a short talk at the workshop does not preclude publication elsewhere.

Please submit your extended abstracts at https://prisc2019short.hotcrp.com/.

Contact and More Information

For questions please contact the workshop chairs, Dominique Devriese (dominique.devriese@cs.kuleuven.be) and Deepak Garg (dg@mpi-sws.org).

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