发表机构
Massachusetts Institute of Technology; MPI-SP; DistriNet, KU Leuven; Inria（麻省理工学院; 马克斯·普朗克安全与隐私研究所; 荷语鲁汶大学分布式网络研究中心; 法国国家信息与自动化研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出 SCHERI，一种为 CHERI 架构提供可证明安全的推测执行的处理器设计，通过形式化框架联合推理能力安全与信息流，确保恒定时间策略下的端到端安全，抵御 Spectre 攻击。
AI 中文摘要
基于能力的架构（如 CHERI）为软件组件的架构隔离提供了强有力的支持。为了进一步防止微架构信息泄露，软件可以采用恒定时间风格编写。然而，现代处理器严重依赖推测执行，这可能破坏恒定时间的保证，并瞬时泄露隔离的秘密。在这项工作中，我们表明为 CHERI 提供安全推测并非易事，且现有方案未能保持机密性保证。我们开发了一个形式化框架，用于联合推理能力安全、推测执行和信息流安全，并利用该框架演示潜在泄露。随后，我们提出了 SCHERI，一种在该框架内的新处理器设计，并正式证明其为恒定时间策略提供了端到端的安全推测保证。我们的结果为构建未来能够抵御 Spectre 攻击（针对恒定时间程序）的基于能力的处理器提供了形式化基础和实用指导。
英文摘要
Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leakage, software can be written in a constant-time fashion. Modern processors, however, rely heavily on speculative execution, which can invalidate the constant-time guarantees and leak isolated secrets transiently. In this work, we show that providing secure speculation for CHERI is non-trivial, and that existing proposals fail to preserve the confidentiality guarantees. We develop a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security, and use it to demonstrate potential leaks. We then present SCHERI, a new processor design within this framework, and formally prove that it provides end-to-end secure speculation guarantees for the constant-time policy. Our results provide formal foundations and practical guidance for building future capability-based processors, which are resilient to Spectre attacks for constant-time programs.
