该论文研究 CHERI 这类基于能力(capability)的处理器架构中的一个关键安全缺口。CHERI 通过在架构层面引入不可伪造的能力指针，为软件组件提供了强隔离与内存安全保证；为了进一步抵御微架构侧信道，软件通常按常量时间(constant-time)风格编写，使执行时间与密钥等机密数据无关。然而现代处理器高度依赖推测执行，推测执行可以在时间维度上绕过架构层面的权限检查，把本应被隔离的机密瞬时(transiently)泄露出去，从而使常量时间编程所提供的机密性保证失效。作者首先论证：在 CHERI 上实现“安全推测”并不平凡，已有的一系列推测执行防护提案无法在保持能力语义的同时维持机密性保证，存在可被形式化刻画的信息泄露路径。为此，论文提出一个统一的形式化框架，能够同时推理三件事：能力安全(capability safety，即能力不可被伪造、不可被越权派生或衰减)、推测执行语义、以及基于信息流的非干扰性(non-interference)安全性质。作者利用该框架形式化地展示了现有设计在 CHERI 语义下的潜在泄露。在此基础上，论文给出新的处理器设计 SCHERI，并在同一框架内给出形式化证明：对于遵循常量时间策略的程序，SCHERI 能够提供端到端的安全推测保证，即推测执行既不会破坏常量时间假设，也不会泄露被架构隔离的机密。其核心贡献是为未来基于能力的处理器建立形式化基础并提供工程指引，使这类处理器对面向常量时间程序的 Spectre 类攻击具备韧性。

该论文关注高性能 CPU 市场从 x86 向 Arm 架构转型的背景，特别是 Apple M 系列芯片在苹果生态系统中完全取代 Intel CPU 的趋势。作者指出，尽管 x86 CPU 已被安全社区广泛分析，但苹果生态系统的安全性仍然缺乏系统性的探索。论文提出了一种基于浏览器的无计时器推测执行攻击方法，命名为 iLeakage，针对 Apple 设备（如搭载 M 系列芯片的 Mac 和 iOS 设备）发起侧信道攻击。传统推测执行攻击通常依赖高精度计时器来测量缓存或微架构状态变化，但浏览器环境往往限制或模糊化计时精度。iLeakage 通过利用不需要显式计时器的机制，在 Safari 等浏览器中实现跨进程或跨站点的敏感信息泄露。论文的核心贡献是首次在苹果自研芯片上展示实用的浏览器端推测执行攻击，弥补了 Arm 架构（特别是 Apple Silicon）安全研究的空白。虽然摘要未提供具体攻击细节和实验数据，但该方法暗示了苹果设备在现代 Web 攻击面中面临新的侧信道风险，也表明需要针对 Apple 芯片的微架构特性重新审视浏览器安全隔离机制。

该论文研究推测执行（speculative execution）与信息流语言中“去分类”（declassify）机制之间的相互作用。在实用的信息流编程语言中，程序员可通过 declassify 构造声明有意泄露的数据，例如从私钥计算出的签名或密文通常被信息流分析视为秘密，而密码库可用 declassify 将其公开。论文发现推测执行会导致去分类点产生非预期的信息泄露：攻击者可利用瞬态执行在错误的时间访问正确的内存位置，从而绕过常规信息流保证。作者给出了一个针对 AES 实现的 PoC，能够从标准实现中恢复密钥，该 PoC 是 Spectre 攻击的一个实例，并且在程序使用广泛使用的编译器级防护手段——推测负载加固（SLH）编译时仍然有效。为应对这些攻击，论文提出了形式化对策，包括对 SLH 的重大改进，称为选择性推测负载加固（selSLH）。这些对策能有效地强制执行相对非干涉（RNI），非正式地说，受保护程序的推测性泄露被限制为原程序已有的顺序泄露。作者在专为高保证密码学设计的 FaCT 语言和编译器中实现了最简单的对策，性能开销最多为 10%；虽然未直接实现 selSLH，但初步评估表明，与传统 SLH 相比，selSLH 能显著降低密码学函数的性能成本。该研究揭示了现有防护（如 SLH）在去分类场景下的盲区，为高保证密码学实现提供了新的形式化安全保证和可落地的加固方向。

本文针对高保证密码学（High-Assurance Cryptography）在现代处理器投机执行（Speculative Execution）时代下的安全保证问题展开研究。传统上，高保证密码学通过程序验证与密码工程方法，为密码软件提供内存安全、功能正确性、可证明安全性以及无时序泄漏等机器可验证的保证，但这些保证通常基于顺序执行语义建立。然而，现代处理器为了提升性能普遍采用投机执行，导致实际执行行为与顺序语义不一致，加之著名的Spectre系列攻击利用投机执行漏洞，使得高保证密码学所承诺的安全属性受到质疑。本文旨在消除这些疑虑，证明高保证密码学的优势在投机执行环境下依然成立，且仅需付出适度的性能开销。作者在Jasmin验证框架之上构建了一种端到端的方法，用于在投机执行语义下证明密码软件的安全属性。该方法扩展了原有验证框架的能力，使其能够建模投机执行带来的微架构侧信道风险。通过在Jasmin中实现ChaCha20和Poly1305两种高效密码算法，作者生成了功能正确且高效的汇编实现，并利用形式化验证证明了这些实现不仅对传统时序攻击安全，而且对投机执行攻击（如Spectre）同样安全。实验结果表明，所提出的方法能够在不显著牺牲性能的前提下，为密码软件提供针对投机执行的高保证安全性。该研究的核心贡献在于：第一，首次将高保证密码学的验证目标扩展到投机执行语义，填补了形式化验证与微架构安全之间的空白；第二，提供了可复用的验证方法论和工具链，使密码工程师能够系统性地设计和验证抗投机执行攻击的密码实现；第三，通过实例验证了该方法的实用性和可扩展性。本文适合密码学与形式化验证领域的研究人员、安全架构师以及需要开发高安全性密码库的工程师阅读，尤其对关注侧信道攻击防御的蓝队人员具有参考价值。

该论文针对现代处理器中推测执行机制的安全分析问题展开研究。现代处理器为提升性能，采用了多种推测执行机制，例如分支预测、内存依赖推测、数据值推测等，这些机制会推测性地执行不同类型的指令。攻击者可能同时利用多种推测机制，在单个瞬态执行窗口内触发对推测访问数据的泄露，从而构造出更复杂的侧信道攻击。然而，现有的形式化安全模型通常只针对固定的、硬编码的推测机制进行建模，无法灵活地扩展以覆盖新增或组合的推测机制，导致对推测性泄露的推理不够完备。论文提出了一种自动检测推测执行组合的方法，旨在解决现有模型缺乏通用性和可扩展性的问题。其核心贡献包括：设计一种能够自动识别和推理多种推测机制组合的形式化框架，使安全分析师能够系统地评估处理器在不同推测策略联合使用下的信息泄露风险。该方法预期能够发现传统单机制模型遗漏的泄露路径，为处理器安全验证提供更全面的理论基础。由于目前仅获得论文摘要，具体技术细节、实验验证和工具实现尚未披露，因此本摘要仅基于摘要信息进行概括。适合处理器架构师、硬件安全研究人员以及形式化验证领域的学者阅读。

该论文研究推测执行攻击对常数时间编程（constant-time programming）安全性的破坏。常数时间编程是密码学等安全敏感软件中防止微架构侧信道攻击的标准技术，但推测执行攻击（如 Spectre）会使其失效。因此，常数时间代码还必须部署针对推测执行攻击的防御措施，以防止存储在内存或处理器寄存器中的秘密数据被泄露。然而，现有的防御手段（如推测加载硬化，Speculative Load Hardening, SLH）虽然能提供强安全保证，但性能开销非常高。针对这一问题，论文提出了一种名为 Declassiflow 的静态分析方法，用于建模非推测知识（non-speculative knowledge），从而在保证安全性的前提下放宽推测执行安全措施的严格性。其核心思想是通过静态分析识别哪些数据在推测执行中不会成为秘密，进而减少不必要的防御加固，降低性能损失。论文的主要贡献包括：形式化非推测知识的概念、设计相应的静态分析算法，并验证该方法能在不牺牲安全语义的前提下提升性能。适合对微架构安全、侧信道防护、编译优化和形式化验证感兴趣的安全研究人员、系统开发者和编译器工程师阅读。由于仅获取了论文摘要，尚无法评估实验细节和具体性能提升幅度，但该研究为缓解推测执行防御的性能瓶颈提供了新思路。

本文提出了一种名为 dfence 的新型 CPU 指令，旨在以硬件-软件协同的方式高效缓解推测执行攻击（如 Spectre-PHT 和 Spectre-STL）。现有的软件缓解方案（如 Speculative Load Hardening, SLH）虽能有效抵御 Spectre-PHT，但需要软件维护推测掩码，既容易出错又带来额外开销；而针对 Spectre-STL 的防御（如 SSBD 位）缺乏细粒度控制且性能损耗明显。dfence 通过极少量的硬件支持，泛化了 SLH 的思想，使开发者能够对敏感寄存器进行注释标注，硬件则确保这些值不会在瞬态执行中被泄露。作者在 Proteus CPU 中实现了 dfence，并进行了安全性和性能评估，实验显示平均性能开销小于 1%。此外，为了便于安全采用，作者设计了一个类型系统，能够静态验证代码中 dfence 指令放置的正确性，从而减少人工标注带来的错误风险。这项工作为处理器微架构安全提供了一种新的硬件-软件协同设计思路，特别适合计算机体系结构、系统安全和编译器方向的研究者与实践者参考。本文为扩展版本，但当前仅基于摘要进行分析，未包含完整实验细节。

本文研究了苹果自研 ARM 架构处理器（Apple Silicon）上 macOS 系统的内核地址空间布局随机化（KASLR）安全性。KASLR 是一种基于随机化的内核加固技术，但历史上容易受到微架构侧信道攻击。现代 macOS 系统通过内核隔离（kernel isolation）将内核页表与用户空间页表分离，试图阻止 KASLR 突破攻击。本文发现，利用系统调用中的 Spectre 型推测执行 gadget，无特权攻击者可以诱导对选定内核地址的转换，使 TLB（转换后备缓冲区）根据地址的有效性发生变化，从而构建绕过内核隔离的 KASLR 突破原语。研究人员通过硬件性能监控单元对多种 M 系列处理器上的 TLB 内部结构进行逆向工程。基于该原语，他们实现了 SysBumps——首个针对 Apple Silicon 上 macOS 的 KASLR 突破攻击。实验评估表明，SysBumps 能够在不同 M 系列处理器和 macOS 版本上有效突破 KASLR。文章还讨论了可能的缓解措施。该研究揭示了即使在内核隔离存在的情况下，推测执行侧信道仍可被利用，对苹果生态系统的安全性构成了严重威胁。

该论文提出 DOLMA，一种基于“瞬态不可观测性”原则的新型微架构安全方案，旨在彻底消除推测执行侧信道攻击（如 Spectre 与 Meltdown）的根源。作者首先分析了现有防御机制（如 lfence、MD 清空、延迟装载等）的局限——它们要么开销过高，要么覆盖不全。基于对瞬态执行中数据流与微架构状态的深度观察，论文定义了“瞬态不可观测性”标准：任何瞬态指令的执行结果不得被后续架构状态或微架构侧信道所观测，即所有瞬态状态的改变必须在提交前完全不可见。DOLMA 通过引入一种新的执行模式，确保只有架构上最终提交的指令才能影响缓存、TLB、分支预测器等共享资源。具体地，DOLMA 在处理器流水线中插入一个“不可观测区”，该区内所有存储操作的结果被暂时阻塞，而加载操作返回的值被标记为“可能不可信”；同时配合一种新型的“瞬态隔离缓冲区”来临时存放写入，直到指令完成提交。实验基于 gem5 模拟器在 x86-64 架构上实现，运行 SPEC CPU2017 与 PARSEC 基准测试。结果表明，与基线相比，DOLMA 的平均性能开销仅 6.7%，远低于现有软件加固方案（30%–100%），也优于大多数硬件方案。论文还从形式化角度论证了 DOLMA 满足瞬态不可观测性，并证明了其能够防御所有已知瞬态执行变种。主要贡献包括：提出瞬态不可观测性原则、设计 DOLMA 微架构、提供完整的形式化安全证明，以及通过模拟评估展示低开销的实用防御。该工作适用于处理器设计团队与微架构安全研究者，为后 Spectre 时代的硬件安全提供了新思路。

本论文提出了一种名为Tiktag的新型攻击方法，旨在通过推测执行绕过ARM架构中的内存标记扩展（MTE）安全机制。MTE是ARM v8.5引入的硬件安全特性，通过为每个内存分配随机标签并检查访问时的标签匹配来防御缓冲区溢出、释放后使用等内存安全漏洞。然而，作者发现推测执行过程中标签检查的时机存在微架构侧信道漏洞：攻击者可以利用分支预测错误或异常，在标签验证实际发生之前，通过推测执行访问具有错误标签的内存，从而泄漏标签信息或绕过保护。论文详细描述了攻击的微架构原理，包括如何触发推测窗口、如何利用缓存侧信道提取标签，以及如何在真实硬件（如Apple M1和ARM固定功能CPU模拟器）上实施攻击。实验表明，Tiktag能够以高成功率提取64位标签中的部分位，并进一步结合其他漏洞实现完整的内存读写。该研究揭示了硬件安全机制与微架构优化之间的新冲突，对依赖MTE的软件安全方案构成威胁。

该论文提出一种名为 GadgetMeter 的框架，用于定量且准确地评估推测执行元素（speculative gadgets）的可利用性。推测执行漏洞（如 Spectre）利用现代处理器中的推测执行机制，通过微架构侧信道泄露敏感信息。现有工作通常关注于发现新的 gadgets 或缓解措施，但缺乏对 gadgets 可利用性的统一量化标准。GadgetMeter 通过分析微架构行为、时序差异和缓存状态，建立了一套自动化的评估指标。该框架首先从二进制代码中识别出潜在的推测执行 gadgets，然后模拟推测执行路径，并测量不同条件下的执行时间差异和缓存访问模式，从而计算每个 gadget 的利用难度评分。实验在多个真实处理器（如 Intel、AMD）上验证，表明 GadgetMeter 能够有效区分高可利用性与低可利用性的 gadgets，并与已知攻击的成功率有良好相关性。该工作为安全研究人员提供了一种系统化的方法论，用于评估推测执行漏洞的威胁程度，并辅助设计更精准的缓解策略。

该论文提出了一种名为μCFI（微架构控制流完整性）的形式化验证方法，旨在解决现有控制流完整性（CFI）机制在微架构层面的安全漏洞。传统的CFI仅在软件或ISA（指令集架构）层面保证控制流安全，但无法抵御利用微架构侧信道或瞬态执行攻击（如Spectre、Meltdown）的控制流劫持。作者通过形式化建模微架构状态（如分支预测器、缓存、乱序执行单元）与控制流之间的关系，定义了微架构层面的安全策略。μCFI基于模型检验技术，能够验证处理器设计是否满足该策略，从而确保即使在微架构优化（如预测执行）下，控制流也不会被恶意操纵。实验在RISC-V处理器核心上实现，验证了多个已知攻击变种（如Spectre v1、v2）的缓解效果，并发现了新的潜在攻击路径。该工作首次将形式化验证应用于微架构CFI，为安全处理器设计提供了理论保证。