The Coq mailing list

[PriSC PC Chairs <prisc.pc.chairs AT gmail.com>]

Principles of Secure Compilation (PriSC) 2021: Call for Participation
and Short Talks

tl;dr: a new exciting edition of PriSC is in the works! as usual, we've reserved
a few slots for short talks, where speakers can spend a few minutes telling us
about ongoing work and foster informal discussions; please do send us your short
talks proposals!

Principles of Secure Compilation Workshop (PriSC 2021)

  - Registration: https://popl21.sigplan.org/
  - Accepted talks available here:
    https://popl21.sigplan.org/home/prisc-2021#event-overview
  - Invited speaker: Hugo Vincent (ARM)
  - Call for short talks: see below
    Deadline: January 11th 2021

The Workshop on Principles of Secure Compilation (PriSC) is an informal 1-day
workshop without proceedings. The goal is to bring together researchers
interested in secure compilation and to identify interesting research directions
and open challenges.

PriSC 2021 will be held on Saturday January 17th, 2021 online.
It will be co-located with POPL 2021, also online.

For more information about this edition and the PriSC series, please
visit https://popl21.sigplan.org/home/prisc-2021

### Invited Speakers

    Hugo Vincent (ARM)

### Accepted papers

The list of accepted talks is available at

    https://popl21.sigplan.org/track/prisc-2021#event-overview

### Call for Short Talks

We also have a short talks session, where participants get 5 minutes to present
intriguing ideas, advertise ongoing work, etc. If you're interested in giving a
short 5-minute talk, please 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.

  - Deadline: January 11th, 2021
  - More details:
    https://popl21.sigplan.org/home/prisc-2021#Call-for-Short-Talks
  - Submit here:
    https://forms.gle/wkCyK4fN3i11nbyD7

### Workshop summary

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.

### Contact

For any questions please contact the workshop chairs, Jonathan Protzenko
(jonathan.protzenko AT gmail.com) and Deian Stefan (deian AT cs.ucsd.edu).

To make sure you receive PriSC announcements in the future please
subscribe to the following low-traffic mailing list:
https://lists.gforge.inria.fr/mailman/listinfo/prisc-announce