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