20th Workshop on Programming Languages and Analysis for Security (PLAS 2025)

Overview

PLAS explores the use of programming language and program analysis techniques to improve software security across compilers, machine learning models, and smart contracts. It promotes speculative, forward-looking ideas and insightful discussions at the intersection of programming languages and security.

Invited Speakers

Limin Jia
(Carnegie Mellon University)

Automatically synthesizing exploits for code injection attacks in Node.js packages using types

Abstract. JavaScript is widely used in applications, via the Node.js runtime. Unfortunately, code-injection vulnerabilities, such as those that allow arbitrary code execution, are frequently found in Node.js packages. Most existing vulnerability-detection tools don’t construct proof-of-concept (PoC) exploits to help developers investigate potential vulnerabilities. In this talk, I will present our work on automatically generating exploits to help developers understand code-injection vulnerabilities. Node.js packages do not come with type specifications, which makes it challenging to generate appropriate inputs to APIs. Our novel exploit synthesis algorithms use output from program analysis to generate inputs of a specific type or with a specific structure and non-trivial interactions with the package API under test. Our evaluations show that we can synthesize PoC for a large fraction of the reported code injection vulnerabilities.

Jan Reineke
(Saarland University)

Verification and Synthesis of Hardware-Software Leakage Contracts

Abstract. Microarchitectural attacks undermine security by exploiting software-visible side effects of hardware optimizations such as caching and speculative execution. To use modern processors securely, programmers must understand the security consequences of these optimizations. Yet, instruction set architectures (ISAs), the traditional interface between hardware and software, are ill-suited for this purpose: they abstract away microarchitectural details entirely and therefore fail to reflect their security impact. To enable the construction of secure software systems on top of modern hardware, we have recently proposed leakage contracts as a new security abstraction at the ISA level. However, leakage contracts are only useful once processors are available that are known to satisfy them.
In this talk, I will introduce 1. LeaVe, a tool for the verification of register-transfer-level (RTL) processor designs against ISA-level leakage contracts, and 2. LeaSyn, a tool and methodology for the synthesis of precise and sound leakage contracts. To scale to realistic processor designs, LeaVe exploits a decoupling theorem that allows to separate security and functional correctness concerns. LeaVe employs inductive reasoning on relational abstractions to obtain unbounded contract satisfaction proofs and invariant synthesis to automate the process. Using LeaVe and LeaSyn, we precisely characterize the side-channel leakage of three open-source RISC-V processors at the ISA level.

Tentative Program

Scope

• Side-channel vulnerability detection and elimination
• Verification techniques applied to adversarial learning and smart contracts
• Software isolation (e.g., SFI, sandboxing)
• Compiler/runtime-based hardening and monitoring
• Program analysis, binary analysis, and fuzzing
• Security enforcement mechanisms
• Cryptographic protocol verification
• Information flow and access control
• Security in web, IoT, and cloud programming languages

Submission Guidelines

We invite both short papers and long papers. For short papers, we especially encourage the submission of position papers that are likely to generate lively discussion as well as short papers covering ongoing and future work.

• Full papers: There is no page limit on long papers. Papers in this category are expected to have relatively mature content. Papers that present promising preliminary and exploratory work, or recently published work are particularly welcome in this category. Long papers may receive longer talk slots at the workshop than short papers, depending on the number of accepted submissions.
• Short papers: should be at most 2 pages long, plus as many pages as needed for references. Papers that present radical, open-ended and forward-looking ideas are particularly welcome in this category. Authors submitting papers in this category must prepend the phrase "Short Paper:" to the title of the submitted paper.

The workshop has no published workshop proceedings and there is no restriction on paper format other than the page limits stated above. Presenting a paper (either short or long) at the workshop does not preclude submission to or publication in other venues that are before, concurrent, or after the workshop. Papers presented at the workshop will be made available to workshop participants only.

Please submit your submissions (in PDF format) via the following website: https://plas25.hotcrp.com. We follow a single-blind reviewing process, so you do not need to anonymize your submissions.

Important Dates

Paper submission: June 20 July 4, 2025 AoE

Author notification: August 8, 2025

Workshop date: October 13, 2025

Program Committee

• Amir Ahmadian (KTH, Sweden)
• Sebastien Bardin (CEA, France)
• Abhishek Bichhawat (IIT Gandhinagar, India) (co-chair)
• Ferhat Erata (Yale, USA)
• Jana Hofmann (MPI-SP, Germany) (co-chair)
• Adrien Koutsos (Inria, France)
• McKenna McCall (Carnegie Mellon University, USA)
• Toby Murray (University of Melbourne, Australia)
• Sabine Oechsner (VU Amsterdam, Netherlands)

Previous Editions

• PLAS 2024: Salt Lake City, USA
• PLAS 2023: Copenhagen, Denmark
• PLAS 2022: Virtual
• PLAS 2021: Virtual
• PLAS 2020: Virtual
• PLAS 2019: London, UK
• PLAS 2018: Toronto, CA
• PLAS 2017: Dallas, TX, USA
• PLAS 2016: Vienna, Austria