-
Notifications
You must be signed in to change notification settings - Fork 45
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'SIGPLAN:master' into master
- Loading branch information
Showing
1 changed file
with
121 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,121 @@ | ||
--- | ||
title: "PriSC 2024: Call for Presentations" | ||
timestamp: "10/25/2023 15:39:33" | ||
deadline: "11/2/2023" | ||
--- | ||
Short version: PriSC is a fun, welcoming and exciting venue. Share | ||
updates, ideas, thoughts or send students for a friendly gathering | ||
that may lead to future collaborations and ideas. Submit now! | ||
|
||
================================================ | ||
Call for Presentations: PriSC 2024 @ POPL 2024 | ||
================================================ | ||
|
||
Secure compilation is an emerging field that puts together advances in | ||
security, programming languages, compilers, verification, systems, | ||
and hardware architectures in order to devise more secure compilation | ||
chains that eliminate many of today’s security vulnerabilities and | ||
that allow sound reasoning about security properties in the source | ||
language. For a concrete example, all modern languages provide a | ||
notion of structured control flow and an invoked procedure is | ||
expected to return to the right place. However, today’s compilation | ||
chains (compilers, linkers, loaders, runtime systems, hardware) | ||
cannot efficiently enforce this abstraction against linked low-level | ||
code, which can call and return to arbitrary instructions or smash | ||
the stack, blatantly violating the high-level abstraction. Other | ||
problems arise because today’s languages fail to specify security | ||
policies, such as data confidentiality, and the compilation chains | ||
thus fail to enforce them, especially against powerful side-channel | ||
attacks. The emerging secure compilation community aims to address | ||
such problems by identifying precise security goals and attacker | ||
models, designing more secure languages, devising efficient | ||
enforcement and mitigation mechanisms, and developing effective | ||
verification techniques for secure compilation chains. | ||
|
||
The goal of this 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 | ||
software or hardware enforcement mechanisms for secure compilation. | ||
|
||
8th Workshop on Principles of Secure Compilation (PriSC 2024) | ||
============================================================= | ||
|
||
The Workshop on Principles of Secure Compilation (PriSC) is an | ||
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 8th edition | ||
of PriSC will be held on January 20, 2024 in London, United Kingdom | ||
together with the ACM SIGPLAN Symposium on Principles of Programming | ||
Languages (POPL) 2024. | ||
|
||
Important Dates | ||
=============== | ||
|
||
* Thu 02 Nov 2023: Submission Deadline | ||
* Thu 07 Dec 2023: Acceptance Notification | ||
* Sat 20 Jan 2024: Workshop | ||
|
||
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 included). 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 | ||
============================ | ||
|
||
You can find more information on the workshop website: | ||
https://popl24.sigplan.org/home/prisc-2024 | ||
|
||
For questions please contact the workshop chairs, Marco Patrignani and | ||
Shweta Shinde. | ||
|