PLAS 2026 - Workshop on Programming Languages and Analysis for Security

Accepted Papers

The list of accepted papers at PLAS'2026. The detailed program will be coming soon.

Invited Speaker

Deepak Garg

Max Planck Institute for Software Systems

Accepted Papers

Long talks

LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean
Simon Jeanteur and Lorenzo Veronese (TU Wien), Magdalena Solitro (Fondazione Bruno Kessler), Matteo Maffei (TU Wien)

Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-dependent behavior, inductively defined data structures, unbounded executions, and conditional secrecy requires a level of expressiveness that is difficult to reconcile with effective automation. As a result, protocol verification has largely followed two disjoint paths: fully automated methods with limited expressiveness, or interactive proofs in general-purpose theorem provers that offer flexibility but only limited, non-specialized automation. We present an orthogonal approach that bridges this gap by combining compositional type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols. Guided by the language-and-automation co-design (LAC) principle, our approach delivers protocol-specific automation while retaining high expressiveness. We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*, and combining protocol-specific automation with interactive proofs. Our framework supports, in a unified setting, a broad class of functional and security requirements, including secrecy and authentication for stateful protocols, as well as recursive conditional secrecy for protocols using XOR. We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.

zkTAL: Verifying Memory Safety of Binaries via Type Checking in Zero Knowledge
Luís Pedro Félix Ferreirinha and Klaus v. Gleissenthall (Vrije Universteit Amsterdam)

As proprietary software is deployed widely, it remains the target of memory vulnerabilities. Unlike open-source software, users of proprietary software who want to avoid attacks are left at the mercy of vendors who, in turn, cannot easily convince their clients that their software is benign without revealing its source code. In this paper, we present zkTAL, a method for proving memory safety of RISC-V binaries in zero knowledge. To verify safety at the binary level, zkTAL builds on a new typed assembly language called TAL2O3, which — inspired by Rust — tracks lifetimes and ownership of pointers to ensure memory safety, and control-flow integrity. Given a well-typed TAL2O3 program, zkTAL encodes the type derivation-tree as private witness that we pass to a zero knowledge prover, which can then demonstrate the correctness of the type derivation to a user without leaking anything about the binary or the proof itself. To ensure the proof matches the binary that is shipped to the user, we use a Merkle Tree encoding to match each basic block in the proof to a basic block in the binary. Since type-checking is compositional, we can split the overall proof into component proofs for each basic block. A recursive aggregator circuit then ensures that the proofs combine into the shipped binary. We implement zkTAL and evaluate it against a collection of TAL2O3 programs, including implementations of cryptographic algorithms, together with synthetic benchmarks to measure scalability. Our experiments show that proving time scales linearly with the number of basic blocks of the input program.

Formalizing and Securing Data Memory-Dependent Prefetchers
Jens Sprengers and Marton,Bognar (KU Leuven), Lesly-Ann Daniel (EURECOM), Frank,Piessens (KU Leuven)

Data memory-dependent prefetchers (DMPs) are a microarchitectural optimization introduced in mainstream desktop and server CPUs in recent years. Although DMPs offer performance improvements, they have been shown to enable side-channel leakage of secrets, even from constant-time code that has been hardened against Spectre attacks. Existing defenses either incur significant performance overhead or, as we show, fail to prevent all DMP secret leakage. In this work, we address this gap by designing a defense that is both secure and efficient. First, we propose a classification for DMP leakage, categorizing existing and novel attacks. We demonstrate these leakage classes in practice by implementing the first open-source DMP on a RISC-V processor, and show that the only existing defense that aims to preserve DMP performance fails to protect against entire leakage classes. Next, we propose SecDMP, a provably secure and efficient DMP defense. SecDMP requires secrets to be marked in memory and ensures that the DMP does not encode secret data in the microarchitecture, without compromising performance for public data. We prove the security properties of SecDMP by introducing a formalization of DMPs, which we also use to model several commercial designs. Notably, when combined with speculative-execution defenses, SecDMP restores complete microarchitectural security for constant-time code. Finally, we show in our empirical evaluation that SecDMP prevents all DMP leakage while incurring minimal performance overhead and low hardware cost.

Constant-Gas Programming for Confidential Smart Contracts
Meng Xu (University of Waterloo)

Confidential smart contract execution try to keep calldata and contract state secret while preserving the familiar execution model of Ethereum-like blockchains. This combination, however, unexpectedly creates a side channel that constant-time programming does not close. In the EVM, storage metering distinguishes whether a write sets a zero slot, clears a non-zero slot, writes back the same value, or updates a non-zero value to another. Thus a contract can execute the same bytecode and touch the same storage slots, yet still leak secrets through the semantic class of its storage updates. This paper presents constant-gas programming for confidential smart contracts. We formalize the attacker as a marker-aware write oracle M+ and define constant-gas security as update-oblivious noninterference over EVM-style traces. We then give concrete evidence that Oasis Sapphire localnet is not safe against M+ adversaries. To defend, we build Coga, a proof-carrying toolchain for a subset of Solidity that compiles and executes confidential smart contracts with proof artifacts showing that the execution is M+-safe. Our evaluation shows that Coga is practical for Solidity contracts involving scalars and small and bounded mappings, and can optionally use Path ORAM for contracts involving large mappings.

Data Layout Diversification as a Data-Only Attack Mitigation under Multi-Variant Execution
Anton Schelfhout and Adriaan Jacobs and Stijn Volckaert (KU Leuven)

Memory errors in memory-unsafe software continue to be exploited by malicious actors. Data-only attacks have recently emerged as a potent class of threats that sidesteps popular control-flow defenses like CFI entirely. Existing data-only defenses enforce partial or complete memory safety, incurring runtime overheads that are too high for widespread deployment. Multi-Variant Execution (MVX) offers a low-overhead alternative: by running diversified variants in lock-step on identical inputs, an exploit that succeeds in one variant produces detectable divergence in the others. Applying this approach to data-only attacks requires diversifying each variant’s data layout so that an exploit’s effect differs across variants and is detected as a divergence. In practice, this is impeded by Address-Sensitive Behavior (ASB), in which a program’s control flow depends on concrete address values that differ among variants. In this paper, we introduce a compiler-based unification technique that automatically neutralizes ASB at its source by selectively supplying variant-agnostic values to address-sensitive operations. We show that our approach is effective and incurs low run-time overhead on SPEC CPU2006. Then, we also present initial results from an empirical study of production memory allocators to measure their memory layout diversity, as a starting point for a practical randomizing allocator against data-only attacks in MVX. The preliminary results from this work show promise that data layout diversification can indeed be a practical avenue towards low-overhead data-only attack mitigation in MVX. data-only attack mitigation in MVX.

Bob DyLean: A Framework for the Symbolic Analysis of Cryptographic Protocols in Lean
Théophile Wallez and Cas Cremers (CISPA Helmholtz Center for Information Security)

Over the last decades, symbolic (Dolev-Yao) methods for the analysis of security protocols have proven to be effective to analyze and establish strong guarantees for widely deployed protocols and systems, such as TLS 1.3, E-voting protocols, EMV, and MLS. On the one hand, analysis methods like Tamarin and ProVerif provide automation and support for user-defined equational theories. On the other hand, methods like DY* offer more flexible and modular reasoning, but hardcode threat models and do not support custom equational theories. We present DyLean, a framework for the symbolic analysis of cryptographic protocols in the Lean theorem prover. Our framework comprises both a flexible general-purpose symbolic semantics, as well as a concrete proof methodology. DyLean allows defining protocols and expected security properties; its semantics and equational theories can be customized by the user. Furthermore, the semantics are agnostic of the specific proof methodology: our goal is to provide a generic framework that can be used by the community as a foundation to develop various proof methodologies. Moreover, we provide a concrete proof methodology inspired by DY*, based on trace invariants. Thus, DyLean inherits from the qualities of DY*: it is able to analyze protocols involving unbounded loops or datastructures, and is able to compose security proofs in a variety of scenarios. Our proof methodology improves on DY* by allowing for user-defined equational theories and threat models. We apply our methodology to several case studies, demonstrating that DyLean can effectively be used to analyze a variety of protocols.

Pantomime: Constructive Leakage Proofs via Simulation
Robin Webbers (Vrije Universiteit Amsterdam), Robert Schenck (Northeastern University), Wind Wong and Kristina Sojakova and Klaus v. Gleissenthall (Vrije Universiteit Amsterdam)

Tools for verifying leakage descriptions of hardware aim to ensure that a given hardware design doesn’t leak secrets via its microarchitecture, when executing programs with appropriate countermeasures. However, existing techniques for proving correctness of leakage descriptions are based on non-constructive proofs via non-interference. As a result, they often rely on expensive solvers that offer little help when verification fails or require handwritten invariants, which are difficult to come up with and even harder to debug. In this paper, we present a new approach to leakage verification which we call simulation-based leakage proofs. To show that a leakage description correctly captures a hardware design using a simulation-based proof, the user constructs a simulator—another hardware design that must faithfully replicate all attacker-observable behavior from explicitly leaked secrets. Simulation-based proofs therefore offer a constructive alternative to classic non-interference proofs, exposing a proof object—the simulator, witnessing the correctness claim. As simulators are just programs, we can write, execute and debug them like any other program, making them easy to use. We also show that they can be checked locally, which makes proof checking fast. We implement simulation-based leakage proofs in Pantomime, a tool that supports writing processors and their leakage proofs in Haskell; we report on using Pantomime to write and verify AIMCore, a 5-stage in-order processor, its leakage description, and simulator, as well as a side-channel hardened version of the core. We show that Pantomime verifies them efficiently (it checks AIMCore in under 40s), and use AIMCore’s leakage description to check for leakages in crypto libraries which uncovered two new vulnerabilities in wolfSSL that have both been assigned CVE’s.

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
Jonathan Baumann Yonghyun Kim (MPI-SP), Yan,Farba (MPI-SP and Ruhr University Bochum) Catalin Hritcu (MPI-SP), Julay Leatherman-Brooks (MPI-SP and Portland State University)

This paper introduces Triosecuris, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). Triosecuris is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and RSB misspeculation for returns and set the SLH misspeculation flag. We formalize Triosecuris as a trans formation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline.

Cerisier: a Program Logic for Attestation in a Capability Machine
June Rousseau (Aarhus University), Denis Carnier (KU Leuven), Thomas Van Strydonck (Fortanix), Steven Keuchel and Dominique Devriese (KU Leuven), Lars Birkedal (Aarhus University)

A key feature in trusted computing is attestation, which allows encapsulated components (enclaves) to prove their identity to (local or remote) distrusting components. Reasoning about software that uses the technique requires tracking how trust evolves after successful attestation. This process is security-critical and non-trivial, but no existing formal verification technique supports modular reasoning about attestation of enclaves and their clients, or proving end-to-end properties for systems combining trusted, untrusted and attested code. We contribute Cerisier, the first program logic for modular reasoning about trusted, untrusted and attested code, fully mechanized in the Iris separation logic and the Rocq Prover. We formalize a recent proposal, CHERI-TrEE, to extend capability machines with enclave primitives, as an extension to the Cerise capability machine and program logic. Our program logic comes with a universal contract for untrusted code, which captures both capability safety and local enclave attestation. Like Cerise, this universal contract is phrased in terms of a logical relation defining capabilities’ authority. We demonstrate Cerisier by proving end-to-end properties for three representative applications of trusted computing: secure outsourced computation, mutual attestation and a modeled trusted sensor component.

Short talks

Toward Bridging The Gap Between Black-box Deobfuscation and Program Synthesis
Grégoire Menguy and Vidal Attias and Nicolas Bellec and Sébastien Bardin (Université Paris-Saclay, CEA, List)

Xyntia is a state-of-the-art of black-box deobfuscator, which aims to simplify highly obfuscated code snippets, i.e. code that is artificially complexified to prevent reverse and analysis. Black-box deobfuscation relies on observed input-output behaviors to synthesize a simpler version of the obfuscated code. While there is a clear link with formal program synthesis, the two communities do not really interact, possibly due to mutual ignorance and a lack of common benchmarks and usage scenarios. The goal of this talk is twofold: (i) to start building bridges between the synthesis and the deobfuscation communities; and (ii) to give the first synthetic and comprehensive presentation of Xyntia, along with the first presentation of its sampler. Especially, we provide the necessary material to both run Xyntia on standard synthesis benchmarks, and easily apply synthesis tools on real deobfuscation cases. We believe that Xyntia will benefit both communities, and allow future progress in these fields.

From Cohesive Noninterference to Dynamic Policy Transport
Antonio Zegarelli and Niki Vazou (IMDEA Software Institute)

Dynamic information-flow control (IFC) policies complicate noninterference because policy updates change what an attacker may distinguish. Categorical semantics has explained static noninterference as preservation of attacker indistinguishability, most notably through Kavvos's [POPL'19] classified sets and cohesion. We propose a lax coherent view of dynamic IFC: fixed-policy fibers carry static security structure, while policy updates transport states and induce transformations between attacker observation quotients. The failure of strict preservation is the semantic content of the policy update: the information released, hidden, or restructured by the change in policy.

RoTS: Right-on-Time Memory Safety for GPUs
Jonas Roels Adriaan Jacobs Stijn Volckaert (KU Leuven)

Modern GPU programming frameworks, including CUDA, ROCm, and Triton, expose unchecked pointer arithmetic, leaving GPU kernels vulnerable to the same spatial memory errors as C and C++ programs. Yet, existing GPU memory-safety tools have seen limited adoption as they impose high overhead, require hardware changes, or fail to integrate with production GPU software stacks. Most GPU memory-safety tools enforce bounds by inserting checks near device accesses. We instead introduce Right-on-Time Safety (RoTS): a software-only memory-safety mitigation that validates GPU memory-access ranges at the host-side kernel launch whenever those ranges depend only on launch-time values, and emits device-side checks only for data-dependent accesses. On average, during LLM inference, RoTS incurs 2.1% overhead by placing 97% of bounds checks at kernel launch. At runtime, only 0.005% of executed on-device memory accesses require bounds checks.

Efficient Verification of Fault Injection Attack Protections at Binary Level
Yanis Sellami and Frédéric Recoules and Noémie Bénard and Sébastien Bardin (CEA List & Université Paris-Saclay)

Advanced attackers can exploit targeted physical perturbations on a system to modify the behavior of an otherwise safe program. This is called a fault injection attack. While analysis techniques exist both at source level and microarchitectural level to evaluate whether successful fault injection attacks are possible, those are respectively unadapted to represent accurate microarchitecural fault effects and prohibitively expansive. Program analysis at binary level offers a good compromise. In this work, we extend the adversarial reachability of \binsec to propose a more general and more mature binary-level fault-aware symbolic execution as a \binsec plugin by making use of the recently introduced capability to hook the decoding phase, allowing the full support of the instruction skip fault model. We validate this approach by analyzing the effect of compiler-introduced countermeasures against various fault models in CompCert and CompaSec, and observe that some of them remain efficient for stronger attack models.

Reasoning about Local Capability Revocation Using Logical Memory and Ghost Stacks
Youie Li and Dominique Devriese (KU Leuven)

Safe memory reuse requires revoking earlier authority when interacting with untrusted code. In this paper, we focus on stack revocation on capability machines using local capabilities, a hardware mechanism that supports secure stack-sharing calling conventions and temporal memory safety. Existing work on robust safety with local capability revocation cannot use standard separation logic machinery, such as points-to assertions and invariants, for revocable memory. It instead resorts to step-indexed Kripke logical relations indexed by worlds with public and private transitions. However, worlds and their transitions force users to work at a low level of abstraction, complicating ordinary spatial reasoning even when revocation is not involved. We present \textbf{Amarena}, a program logic and logical relation for robust safety under local capability revocation, as a simpler alternative to the Kripke approach used in prior work. Amarena adapts logical memory to express temporary assertions over revocable stack regions and uses ghost stacks to reason about well-bracketed control flow. The first novelty is support for \emph{component-local} unreachability, which violates the global unreachability the original approach requires for soundness. The second novelty is a ghost operation for reversible revocation, a principle that is unsound in the original garbage-collection setting. We evaluate Amarena on examples using an existing secure calling convention, including the Very Awkward Example, and show that it disentangles revocation reasoning from ordinary spatial reasoning more cleanly than the Kripke approach. The development is mechanized in Rocq on top of Iris.

Compartmentalization of Unmodified Rust Applications
Maxim Ritter von Onciul and Rüdiger Kapitza (Friedrich-Alexander-Universität Erlangen-Nürnberg)

Because of its strong memory safety guarantees, Rust has become an attractive alternative to C/C++ for systems programming. However, despite Rust's strong type support, it is not a silver bullet. Unsafe sections, use of foreign code, and compiler-soundness bugs still pose vulnerabilities. Ideally, compartmentalization limits the impact of such vulnerabilities to the compartments directly affected. However, manual compartmentalization approaches are considered labor-intensive, error-prone, and require deep system expertise. We present zBulk, an automatic compartmentalization system that requires zero retrofitting of application code and paves the way for flexible fine-grained compartmentalization. We achieve this high degree of automation by leveraging Rust's static type and call information as well as its language constructs that declare mutability and ownership. We discuss the overall zBulk approach, which is based on an analysis of rustc's intermediate representation and leads to the automatic generation of compartments based on a function-level deployment policy. Finally, we present preliminary results on the overhead associated with compartmentalizing a standalone base64 decoder application into up to eight compartments.