代码大模型 / AI 编程 - arXivDaily 专题

2601.22978 2026-06-19 cs.CR cs.PL 版本更新 60%

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking

Triosecuris：针对推测控制流劫持的形式化验证防御

Jonathan Baumann, Yonghyun Kim, Yan Farba, Catalin Hritcu, Julay Leatherman-Brooks

专题命中程序修复：形式化验证防御推测控制流劫持

AI总结提出Triosecuris，结合CET风格硬件辅助控制流完整性与编译器插入的推测加载硬化，通过形式化证明实现相对安全性，确保任意程序在推测执行下不泄露比源程序无推测时更多的信息。

Comments To appear at CSF'26; extended version with appendices. W.r.t. first revision: extended with concrete protection against Spectre RSB and renamed to Triosecuris

Journal ref 39th IEEE Computer Security Foundations Symposium (CSF) (2026) 544-559

详情

DOI: 10.1109/CSF68417.2026.00036

AI中文摘要

本文介绍了Triosecuris，一种针对Spectre BTB、RSB和PHT的形式化验证防御，它结合了CET风格的硬件辅助控制流完整性与编译器插入的推测加载硬化（SLH）。Triosecuris基于一个新颖的观察：在CET风格保护存在的情况下，我们可以精确检测间接调用的BTB误推测和返回的RSB误推测，并设置SLH误推测标志。我们在Rocq中将Triosecuris形式化为一种变换，并提供了机器检查的证明，表明它实现了相对安全性：任何经过变换的程序在推测执行下泄露的信息不超过源程序在无推测执行下泄露的信息。这一强安全保证适用于任意程序，即使那些不遵循密码学常数时间编程规范的程序。

英文摘要

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 transformation 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.

URL PDF HTML ☆

赞 0 踩 0