paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Robust Constant-Time Cryptography

鲁棒常数时间密码学
PLDI 9(PLDI)2025匹配度 2/10 · 论文关注密码库的鲁棒常数时间安全、操作语义与编译器合成,属于程序语言/安全方向,但与画像核心的 LLM/Agent 静态分析、浮点程序分析、贝叶斯程序分析均无直接交集;仅在形式化与工程实现结合这一偏好上略有共鸣。引用 0 inbox
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
crossref: 2026-09-10

AI 速览

一句话:提出 RoboCop:用参数化攻击者模型定义鲁棒常数时间性质,并按应用上下文编译生成定制密码库防护。

密码库需在脆弱宿主应用中仍不泄漏秘密,但针对某类漏洞硬编码的防护难以适配所有上下文,可能造成额外开销或防护不足。本文提出 RoboCop:先以操作语义刻画库在脆弱应用中执行时不同攻击者可观察的行为;再定义由攻击者模型参数化的鲁棒常数时间(RCT)性质,说明库在给定上下文中应抵御何种攻击者;进而实现编译器,为特定上下文合成定制密码库并保证其满足 RCT。作者在 500 多个密码库原语上评估,覆盖读取 gadget、推测执行读取 gadget 和并发观察三类攻击,防护开销通常低于 2%(读取 gadget)和 4%(推测执行读取 gadget)。

问题
密码库即使链接到存在漏洞的应用中也不能泄漏秘密,但开发者只能选择一组固定的防护,难以同时适配不同攻击者与上下文,导致安全与性能的折衷。
方法
提出 RoboCop:用操作语义刻画库在脆弱应用中的行为,定义由攻击者模型参数化的鲁棒常数时间(RCT)性质,并实现编译器按应用上下文合成并保证满足 RCT 的定制密码库。
评估
在 500 多个密码库原语上自动生成针对读取 gadget、推测执行读取 gadget 和并发观察三类攻击的防护,报告开销通常低于 2% 和 4%。
原文摘要(Abstract)

Cryptographic library developers take care to ensure their library does not leak secrets even when there are (inevitably) exploitable vulnerabilities in the applications the library is linked against. To do so, they choose some class of application vulnerabilities to defend against and hardcode protections against those vulnerabilities in the library code. A single set of choices is a poor fit for all contexts: a chosen protection could impose unnecessary overheads in contexts where those attacks are impossible, and an ignored protection could render the library insecure in contexts where the attack is feasible. We introduce RoboCop , a new methodology and toolchain for building secure and efficient applications from cryptographic libraries, via four contributions. First, we present an operational semantics that describes the behavior of a (cryptographic) library executing in the context of a potentially vulnerable application so that we can precisely specify what different attackers can observe. Second, we use our semantics to define a novel security property, Robust Constant Time (RCT), that defines when a cryptographic library is secure in the context of a vulnerable application. Crucially, our definition is parameterized by an attacker model, allowing us to factor out the classes of attackers that a library may wish to secure against. This refactoring yields our third contribution: a compiler that can synthesize bespoke cryptographic libraries with security tailored to the specific application context against which the library will be linked, guaranteeing that the library is RCT in that context. Finally, we present an empirical evaluation that shows the RoboCop compiler can automatically generate code to efficiently protect a wide range (over 500) of cryptographic library primitives against three classes of attacks: read gadgets (due to application memory safety vulnerabilities), speculative read gadgets (due to application speculative execution vulnerabilities), and concurrent observations (due to application threads), with performance overhead generally under 2% for protections from read gadgets and under 4% for protections from speculative read gadgets, thus freeing library developers from making one-size-fits-all choices between security and performance.

链接与引用

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

BibTeX
@article{paperbot3090,
  title = {Robust Constant-Time Cryptography},
  author = {Matthew Kolosick and Basavesh Ammanaghatta Shivakumar and Sunjay Cauligi and Marco Patrignani and Marco Vassena and Ranjit Jhala and Deian Stefan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  year = {2025},
  doi = {10.1145/3729310}
}