paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Automatically eliminating speculative leaks from cryptographic code with blade

Blade:自动消除密码代码中的推测性泄漏
POPL 5(POPL)2021匹配度 3/10 · 该论文属于静态分析与类型系统在密码代码安全(推测执行泄漏)方向的工作,虽有形式化类型系统和 Cranelift 工程实现,但既不涉及 LLM/Agent 与静态分析的交叉,也不涉及浮点程序分析或贝叶斯程序分析,与画像中正在追的核心问题几乎没有交集。引用 53 inbox
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, Deian Stefan
crossref: 2026-09-10

AI 速览

一句话:提出 Blade,用类型系统与 protect 原语自动切断推测性秘密的数据流,消除密码代码中的推测泄漏。

该论文研究推测执行导致密码代码通过缓存等途径泄漏秘密的问题。现有防护要么完全禁止推测,要么难以自动消除泄漏。Blade 的核心思想是:只需切断可能推测性引入秘密的表达式(source)到泄漏秘密的表达式(sink)之间的数据流,而非禁止所有推测。作者提出静态类型系统,将表达式分为 transient(可能含推测性秘密)与 stable,并要求所有 sink 都是 stable;同时引入抽象原语 protect,以细粒度阻止推测,并由类型系统自动合成最少 protect。Blade 在 Cranelift WebAssembly 编译器中实现,用于修复多个已验证但存在推测泄漏的密码原语实现。评估表明,Blade 能自动修复现有程序,无需用户干预,即使以 fence 实现 protect 也保持高效。

问题
推测执行可绕过常量时间检查,使密码代码通过缓存等 sink 泄漏秘密;现有防护要么完全禁止推测,代价高,要么无法自动消除泄漏。
方法
Blade 提出静态类型系统,将表达式分为 transient 与 stable,要求 sink 稳定;用 protect 原语细粒度阻止推测,并自动合成最少 protect。
评估
在 Cranelift WebAssembly 编译器中实现 Blade,修复多个已验证但存在推测泄漏的密码原语实现。结果显示可无需用户干预自动修复,并且即使 protect 用 fence 实现也高效。
原文摘要(Abstract)

We introduce Blade, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative execution, it suffices to cut the dataflow from expressions that speculatively introduce secrets ( sources ) to those that leak them through the cache ( sinks ), rather than prohibit speculation altogether. We formalize this insight in a static type system that (1) types each expression as either transient , i.e., possibly containing speculative secrets or as being stable , and (2) prohibits speculative leaks by requiring that all sink expressions are stable. Blade relies on a new abstract primitive, protect , to halt speculation at fine granularity. We formalize and implement protect using existing architectural mechanisms, and show how Blade’s type system can automatically synthesize a minimal number of protect s to provably eliminate speculative leaks. We implement Blade in the Cranelift WebAssembly compiler and evaluate our approach by repairing several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. We find that Blade can fix existing programs that leak via speculation automatically , without user intervention, and efficiently even when using fences to implement protect .

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1148,
  title = {Automatically eliminating speculative leaks from cryptographic code with blade},
  author = {Marco Vassena and Craig Disselkoen and Klaus von Gleissenthall and Sunjay Cauligi and Rami Gökhan Kıcı and Ranjit Jhala and Dean Tullsen and Deian Stefan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  year = {2021},
  doi = {10.1145/3434330}
}