一句话：提出基于模拟的泄漏证明，以可执行模拟器作为构造性证明对象，并实现工具 Pantomime 验证硬件泄漏描述。
硬件泄漏验证工具多依赖非干涉的非构造性证明，需昂贵求解器或手写不变式，失败时难调试。本文提出基于模拟的泄漏证明：用户构造模拟器，即另一硬件设计，须忠实复现攻击者从显式泄漏秘密中可观测的全部行为。模拟器作为证明对象见证正确性；因是程序，可编写、执行和调试，并可局部检查，使检查快速。作者在 Haskell 中实现 Pantomime，用它编写并验证 AIMCore 五级顺序处理器、泄漏描述、模拟器及抗侧信道版本，检查耗时不到 40 秒；并用泄漏描述检查密码库，在 wolfSSL 中发现两个新漏洞，均已分配 CVE。
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.
@article{WebbersSWSG26,
title = {Pantomime: Constructive Leakage Proofs via Simulation},
author = {Robin Webbers and Robert Schenck and Wind Wong and Kristina Sojakova and Klaus von Gleissenthall},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808340}
}