本文针对Spectre微架构安全漏洞的检测问题，提出了一种名为Haunted RelSE的高效关系符号执行优化方法。Spectre漏洞自2018年公开以来，允许攻击者通过利用处理器的推测执行机制窃取秘密信息，其检测对加密库尤为重要。现有软件级防御的正确性验证和漏洞检测面临两大挑战：一是推测路径导致的状态空间爆炸，二是不同编译阶段可能引入新的Spectre变种。作者提出Haunted RelSE优化，在二进制级别实现可扩展的Spectre漏洞检测，并通过语义证明其相对于朴素显式推测探索方法的正确性。该方法基于对推测路径的关系符号执行，有效缩减探索空间。作者在符号分析工具中实现了Haunted RelSE，并在Spectre-PHT的标准 litmus 测试集以及新提出的Spectre-STL litmus 测试集上进行了广泛实验。实验结果表明，该技术相比现有技术能够发现更多违反行为，且扩展性更优。在实际应用中，作者分析了真实世界的加密库，发现了新的违反。特别地，通过该工具，作者发现索引掩码（index-masking）这一Spectre-PHT的标准防御方法以及编译位置无关可执行文件时常用的gcc选项会引入Spectre-STL违反。针对索引掩码的问题，作者提出了修正方案并验证其有效性。本文适合对程序分析、符号执行、侧信道攻击检测感兴趣的安全研究人员阅读。

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