PriSC 2026

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 may be 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 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.

Call for Presentations

Secure compilation is an emerging field that puts together advances in security, programming languages, compilers, verification, systems, and hardware architectures in order to build compilers that eliminate many of today’s security vulnerabilities.

Anyone interested in presenting at the workshop should submit an extended abstract (up to 2 pages) covering past, ongoing, or future work. Any topic that could be of interest to secure compilation is in scope. Secure compilation should be interpreted broadly to include techniques that span programming languages, architecture, and systems. This includes presentations on new attack vectors whose defenses could benefit from compiler techniques. Presentations that provide a useful outside view or challenge the community are also welcome. Submitting to the workshop does not preclude publication in other venues, as the workshop does not have public proceedings.

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, and property-based testing.