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 in New Orleans, together with the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), in January 2020.
Exact dates have not yet been decided, estimates provided below (check back soon for more accurate info).
- Presentation proposal submission deadline: ~ October 2019
- Presentation proposal notification: ~ November 2019
- PriSC Workshop takes place: 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.
The submission site for PriSC will be set up soon.
Contact and More Information
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 Papers
This is a placeholder text.
You can expect more information about the call for papers soon.
This page will soon have information about the submission and selection process and list the important dates.