News:

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 2nd 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 does of course not preclude publication elsewhere.

Call for Presentations

https://popl18.sigplan.org/track/prisc-2018#Call-for-Presentations

Participation

PriSC will be held on Saturday, 13 Jan 2018. To participate, please register through the POPL registration system.

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 new 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

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Welcome and Invited TalkPriSC at Hershey
Chair(s): Cătălin Hriţcu Inria Paris
09:00
10m
Talk
PriSC Welcome
PriSC
Cătălin Hriţcu Inria Paris
File Attached
09:10
50m
Talk
Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)
PriSC
Mathias Payer Purdue University
File Attached
13:30 - 15:30
Session 2PriSC at Hershey
Chair(s): David Naumann Stevens Institute of Technology
13:30
30m
Talk
Building Secure SGX Enclaves using F*, C/C++ and X64
PriSC
Anitha Gollamudi , Cédric Fournet Microsoft Research
File Attached
14:00
30m
Talk
Robust Hyperproperty Preservation for Secure Compilation
PriSC
Deepak Garg Max Planck Institute for Software Systems, Cătălin Hriţcu Inria Paris, Marco Patrignani Saarland University, CISPA, Marco Stronati , David Swasey MPI-SWS
Pre-print File Attached
14:30
30m
Talk
Formally Secure Compilation of Unsafe Low-Level Components
PriSC
Guglielmo Fachini Inria Paris, Cătălin Hriţcu Inria Paris, Marco Stronati , Ana Nora Evans University of Virginia, USA, Théo Laurent , Arthur Azevedo de Amorim Carnegie Mellon University, USA, Benjamin C. Pierce University of Pennsylvania, Andrew Tolmach Portland State University
Pre-print File Attached
15:00
30m
Talk
Secure Compilation in a Production Environment
PriSC
File Attached

Presentations

Title
Building Secure SGX Enclaves using F*, C/C++ and X64
PriSC
File Attached
Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)
PriSC
File Attached
Constant-time WebAssembly
PriSC
Pre-print File Attached
Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities
PriSC
File Attached
Formally Secure Compilation of Unsafe Low-Level Components
PriSC
Pre-print File Attached
Foundations of Dependent Interoperability
PriSC
Link to publication File Attached
Linear capabilities for modular fully-abstract compilation of verified code
PriSC
File Attached
On Compositional Compiler Correctness and Fully Abstract Compilation
PriSC
File Attached
Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs
PriSC
File Attached
PriSC Welcome
PriSC
File Attached
Robust Hyperproperty Preservation for Secure Compilation
PriSC
Pre-print File Attached
Secure Compilation in a Production Environment
PriSC
File Attached
Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch?
PriSC
Pre-print File Attached
Short talk: Dependently Typed Assembly for Secure Linking
PriSC
Link to publication File Attached
Short Talk: Secure compilation from F* to WebAssembly
PriSC
File Attached
Short talk: The Meaning of Memory Safety
PriSC
Pre-print File Attached

Call for Short Talks

Important Dates

  • Short talk submission deadline: 14 December 2017, AoE
  • Short talk notification: 18 December 2017, AoE
  • PriSC Workshop takes place: 13 January 2018

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.

Topics of interest include but are not limited to:

  • attacker models for secure compiler chains

  • secure compilation properties: full abstraction, memory safety, control-flow integrity, preserving non-interference or (hyper-)properties against adversarial contexts, secure multi-language interoperability

  • enforcement mechanisms: static checking, program verification, reference monitoring, program rewriting, software fault isolation, system-level protection, secure hardware, crypto, randomization

  • experimental evaluation and applications of secure compilation

  • proof methods: (bi)simulation, logical relations, game 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 submitted in text format and are not anonymous

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

Please submit your abstracts at https://prisc18short.hotcrp.com

Contact and More Information

For questions please contact the Program Chair.

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 Presentations

Important Dates

  • Presentation proposal submission deadline: 25 October 2017, AoE
  • Presentation proposal notification: 15 November 2017
  • PriSC Workshop takes place: 13 January 2018

Scope of the Workshop

Anyone interested in presenting at the workshop should submit an extended abstract (up to 2 pages, details below). This can cover past, ongoing, or future work. 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.

Topics of interest include but are not limited to:

  • attacker models for secure compiler chains

  • secure compilation properties: full abstraction, memory safety, control-flow integrity, preserving non-interference or (hyper-)properties against adversarial contexts, secure multi-language interoperability

  • enforcement mechanisms: static checking, program verification, reference monitoring, program rewriting, software fault isolation, system-level protection, secure hardware, crypto, randomization

  • experimental evaluation and applications of secure compilation

  • proof methods: (bi)simulation, logical relations, game 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://prisc18.hotcrp.com/

Contact and More Information

For questions please contact the Program Chair.

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