该论文研究了高保障密码学在现代处理器投机执行（Spectre）下的安全性。传统的高保障密码学通过程序验证和密码工程方法，提供内存安全、功能正确性、可证明安全性和无时序泄露的机器校验证明。然而，这些保证建立在顺序执行语义之上，与利用投机执行提高性能的现代处理器行为不匹配。Spectre式攻击利用投机执行漏洞，对高保障密码学的鲁棒性提出了质疑。论文基于Jasmin验证框架，提出了一种端到端的方法，用于在投机执行下证明密码软件的安全性。该方法扩展了现有验证技术，以覆盖投机执行路径，并保证即使在高性能处理器上也能抵御时序侧信道攻击。实验验证了该方法的有效性：实现了ChaCha20和Poly1305的高效、功能正确的汇编实现，这些实现既抵抗传统时序攻击，也抵抗投机执行攻击，且性能开销适中。主要贡献包括：1) 形式化描述了投机执行下的安全模型；2) 扩展Jasmin框架支持投机执行安全验证；3) 提供经过验证的密码原语实现。该工作对于构建下一代安全关键系统具有重要意义，证明了高保障密码学可以安全地部署在当今主流硬件上。

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 平台的安全架构师阅读。