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

该论文针对密码学软件中的瞬态执行攻击（尤其是Spectre v1）提出了一种基于类型系统的方法，以确保推测性常数时间（Speculative Constant-Time），从而在保持高性能的同时为密码实现提供形式化保证。当前密码库的黄金标准是在高效实现的同时系统性地防御计时攻击，通常借助高保证密码学工具（如Jasmin框架）进行形式化验证。然而，现有工具基于过于简化的执行模型，忽略了瞬态执行产生的微架构泄漏，导致经过验证的实现仍可能受到Spectre等攻击。已有的防御措施往往因性能开销过大而未被实际采用。作者提出了一种值依赖的信息流类型系统，根据执行是否处于错误推测状态动态跟踪安全级别，从而强制实现推测性常数时间属性。该类型系统被集成到Jasmin框架中，并用于保护一个实验密码学库的全部实现，涵盖对称原语、椭圆曲线密码（如X25519）以及Kyber（NIST选定的后量子KEM）。实验结果表明，性能开销极低：Kyber的开销小于1%，X25519几乎为零。这项工作证明了形式化方法可以在不显著牺牲性能的前提下有效缓解瞬态执行攻击。论文的主要贡献包括：提出推测性常数时间的正式定义、设计并实现相应的类型系统、将其集成到Jasmin框架，并通过实际密码库验证其实用性。适合密码学库开发者、系统安全研究员以及形式化验证社区阅读。

本文提出Swivel，一个用于加固WebAssembly（Wasm）免受Spectre攻击的编译器框架。在浏览器之外，Wasm已成为一种流行的轻量级进程内沙箱，常用于边缘云计算和函数即服务（FaaS）平台中隔离不同客户端。然而，Spectre攻击能够绕过Wasm的隔离保证，使恶意代码可能读取沙箱外或其他客户端的数据。Swivel通过确保潜在的恶意代码既不能利用Spectre跳出Wasm沙箱，也不能胁迫受害代码泄露秘密数据，从而加固Wasm。作者设计了两种Swivel方案：一种纯软件方法，可运行于现有CPU；另一种硬件辅助方法，利用Intel第11代CPU的MPK等扩展。两种方案都分别实现了随机化缓解和确定性消除两种模式。随机化模式在SPEC 2006的Wasm兼容子集上开销低于10.3%，而确定性模式开销在3.3%到240.2%之间。尽管某些基准测试开销较高，但Swivel的开销比现有依赖流水线栅栏的防御小9倍到36.3倍。实验表明，Swivel在提供有效防护的同时，性能开销相对较低，为Wasm沙箱环境提供了实用的Spectre防护方案。

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

该论文研究了云边缘计算平台中多租户隔离面临的安全挑战，以 Cloudflare Workers 为例。Cloudflare Workers 为降低冷启动延迟，去除了传统的进程级隔离边界，采用语言级隔离（如 V8 引擎）来承载不同租户的代码。这种架构虽然在性能上具有优势，但被广泛认为会引入 Spectre 等微架构侧信道攻击风险。为此，Cloudflare 此前曾实施一系列防御措施，包括限制高精度计时器、禁止共享内存、禁止多线程，并引入动态进程隔离（DyPrIs）机制来检测可疑行为并对脚本进行进程级隔离。然而，论文作者通过实证分析发现，生产环境中的 DyPrIs 防护并不充分。他们采用微架构放大技术，在 Cloudflare Workers 的生产环境中找到了多种远程计时方法，成功绕过了计时器冻结或粗化策略。基于这些远程计时器，作者端到端地演示了一次远程 Spectre 攻击，能够从同一主机上共存的其他 Worker 中泄漏 JWT 令牌。攻击速率从原先的约 2 比特/分钟大幅提升至最高 12 比特/秒，且准确率达到 99.16%，对客户数据构成直接、实质性的安全威胁。在披露该问题后，Cloudflare 协同实施了多项修复措施：集成 V8 Sandbox 以限制瞬态访问仅能使用 64 位指针；增强 DyPrIs 的检测能力；并部署基于硬件内存保护密钥（MPK）的进程内隔离，为每个租户堆分配独立的内存保护密钥，从而进一步隔离租户数据。该研究揭示了仅依赖语言级隔离与软件计时器限制不足以防御微架构侧信道攻击，凸显了硬件支持的内存隔离机制在边缘计算安全中的必要性。适合云安全研究人员、边缘计算平台开发者和安全防御者阅读。

本文针对硬件侧信道攻击（如Spectre）在真实场景中的检测难题展开研究。尽管机器学习模型在受控环境下能通过硬件性能计数器（HPC）捕捉攻击足迹，但当面对系统背景噪声、多样化攻击变体以及对抗性流量节拍时，静态模型往往失效。为此，作者提出了“方差包络”（variance envelope）的概念，旨在系统刻画攻击签名在不同执行环境中的变化范围。研究覆盖Intel、ARM和AMD三大主流处理器架构，构建了包含三种攻击变体、四种节拍模式和四种背景噪声条件的大规模实验矩阵。实验结果表明，HPC签名极度脆弱，极易受执行环境影响而发生形变；同时，该研究还揭示了AMD Jaguar微架构上一个关键瓶颈：Prime+Probe攻击在该硬件上存在持续性的硬件级失败。最终，作者证明可靠的运行时检测需要架构感知的自适应监控方案，而非依赖静态模型。这一工作为硬件安全监控领域提供了系统性的跨架构实证分析，对设计鲁棒的侧信道检测系统具有重要参考价值。适合安全研究员、硬件架构师以及蓝队检测引擎开发者阅读。

本文提出了一种名为 SpecTaint 的新型 Spectre 漏洞检测技术，旨在解决软件修补过程中难以发现潜在 Spectre 指令窗口（gadget）的问题。当前缓解 Spectre 类攻击的主要手段是在程序中插入序列化指令来禁用潜在 gadget 的投机执行，但缺乏自动化、高效且精确的 gadget 检测方法。SpecTaint 通过在 CPU 模拟器（QEMU 等系统级模拟器）中模拟和探索投机执行路径，将动态污点分析扩展到这些路径上，从而能够追踪数据在投机执行期间如何流动并识别可能被利用的 gadget。作者实现了原型系统 SpecTaint，并在自建的 Spectre 样本数据集和真实世界应用（如 Caffe、Brotli）上进行了评估。实验结果表明，与现有的最先进 Spectre gadget 检测方法相比，SpecTaint 在检测精度和召回率上均有大幅提升，并且能在真实应用中发现新的 Spectre gadget。此外，基于 SpecTaint 检测结果进行的补丁操作，能够显著降低补丁后的性能开销（相比其他检测方法），说明该方法不仅检测能力强，还能辅助生成更精简、性能更好的缓解方案。本文的核心贡献在于：首次将动态污点分析系统性地应用于投机执行路径，实现了系统级模拟下的精确 gadget 发现，并在多个维度上优于已有工作。适合关注微架构侧信道攻击防御、二进制分析、以及 CPU 模拟器开发的蓝队安全研究人员阅读。

Spectre 漏洞利用微架构推测执行机制窃取敏感信息，自 2018 年公开以来给密码库等关键软件带来严重威胁。现有检测方法面临两大挑战：推测路径导致的状态空间爆炸，以及不同编译阶段可能引入新的 Spectre 漏洞。本文提出一种名为 Haunted RelSE 的优化技术，旨在实现二进制级别可扩展的 Spectre 漏洞检测。Haunted RelSE 是一种关系符号执行优化，通过语义等价的变换，将显式的推测探索转化为更高效的隐式关系推理，从而大幅减少需探索的路径数量。作者在符号分析工具中实现了该技术，并在针对 Spectre-PHT（条件分支误预测）和 Spectre-STL（存储到加载转发）的两个 litmus 测试集上进行了全面评估。实验结果表明，Haunted RelSE 相比现有最先进技术和工具，能发现更多违规，且可扩展性更优。此外，将该工具应用于真实世界的密码库时，发现了之前未知的漏洞。特别值得注意的是，研究发现标准防御措施 index-masking（用于阻止 Spectre-PHT）以及 gcc 编译位置无关可执行文件（PIE）的常用选项（如 -fPIE）会引入新的 Spectre-STL 违规。作者提出并验证了 index-masking 的一种修正方案，以消除该问题。本文适合安全研究人员、编译开发者及密码库维护者阅读。

本文提出 Janus，一个基于编译器的安全框架，旨在缓解 ARM64 平台上的瞬态执行攻击（如 Spectre）和控制流劫持。Janus 利用 ARM 的硬件原语——指针认证（PA）和分支目标识别（BTI），通过修改指针认证修饰符（PA modifiers）来整合推测执行和/或控制流依赖，从而防止控制流推测攻击。它通过现有的控制流完整性机制同时保护控制流和推测执行。为了优化性能，Janus 采用修饰符融合（modifier fusion）技术合并不同防御层的操作，以及载体重用（carrier reuse）技术重用受保护变量的寄存器，从而降低开销，同时保持强大的安全保证。在 SPEC CPU2017 基准测试上，平均性能开销仅为 3.85%；实际应用（如 nginx、redis）的开销在 2.97% 到 7.80% 之间。Janus 有效提供了推测执行安全性，且性能和代码大小开销较低，是 ARM 系统的稳健解决方案。本文适合编译器开发者、系统安全研究人员以及 ARM 平台的安全架构师阅读。