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 的一种修正方案，以消除该问题。本文适合安全研究人员、编译开发者及密码库维护者阅读。

本文提出了一种名为符号解释器分析（SIA）的新方法，用于解决动态Web应用程序在符号执行中面临的多语言挑战。传统的符号执行工具由于对动态语言（如PHP）的语法支持有限且工程成本高，难以有效分析现代Web应用。SIA的核心思想是：由于Web应用逻辑由解释器（如PHP解释器）执行，因此可以利用现成的符号执行引擎分析解释器的二进制代码，从而间接理解Web应用的行为。这种方法继承了解释器对完整语法的支持，并复用了现有符号执行引擎的成熟工程实现。然而，SIA需要解决若干技术挑战，包括Web应用的探索（如处理超链接、表单等）、数据库交互的符号化建模等。作者基于SIA实现了SymPHP，一个针对PHP应用的混合执行（concolic execution）引擎。实验表明，SymPHP在多种PHP应用上实现了高代码覆盖率，并成功识别了数据集中77.23%的已知漏洞，显著优于此前的方法。此外，基于SymPHP构建的混合模糊测试框架进一步提升了模糊测试效率，并发现了10个新漏洞。该工作适合安全研究人员、Web应用安全工程师以及符号执行领域的开发者阅读，为动态语言Web应用的自动化漏洞发现提供了新的思路。

该论文提出一种结合符号执行与推测性库预加载的静态控制流图（CFG）恢复技术，专门针对依赖动态代码加载来逃避静态分析的加壳软件和现代恶意软件。现有静态分析方法无法处理运行时动态链接引入的间接调用，导致无法恢复完整的CFG。本文方法在符号执行环境中设置自定义软件钩子，拦截动态加载操作（如dlopen、GetProcAddress等），并将实际库加载到分析状态中。系统采用两级架构：底层存储拦截函数，上层跟踪指令，全部在符号执行引擎内完成。通过完全符号执行避免执行潜在恶意代码，从而安全分析恶意软件。实验使用16个合成基准程序，包含加密库名、网络触发加载、环境派生路径、多阶段解密链、无文件执行和手动ELF解析等多种混淆技术。结果表明，与纯静态分析相比，该方法平均多恢复29.8%的CFG节点和26.5%的边，库检测的精确率和召回率均达100%，所有发现均通过Frida动态插桩验证。

符号执行是一种强大的测试生成技术，能够自动探索程序路径并发现漏洞。然而，其可扩展性受限于路径爆炸问题：随着执行深入，需要探索的符号状态数量急剧增加，导致计算资源耗尽。现有符号执行引擎通常依赖手工设计的启发式策略（如随机选择、最近未覆盖分支优先等）来选择下一个要探索的符号状态，但这些策略往往不够高效，难以适应不同程序的结构。本文提出了一种基于学习的方法来自动优化路径探索策略。具体而言，作者将路径选择建模为序列决策问题，利用强化学习或监督学习（摘要未明确，但通常为学习算法）训练一个模型，根据当前程序状态和已探索路径的历史，预测最有希望到达目标分支的符号状态。该方法能够动态调整探索优先级，从而更有效地覆盖关键代码区域。实验在标准基准集（如Coreutils）上进行，结果表明，与传统的启发式策略（如DFS、随机）相比，该方法在相同时间内能覆盖更多的分支，并生成更高的代码覆盖率。此外，该方法还减少了探索过程中内存和时间的消耗。主要贡献包括：1) 形式化了符号执行中的路径选择问题为一个可学习任务；2) 提出了一种基于学习的探索算法；3) 在多个真实程序上验证了其有效性。本文适合安全研究人员和软件测试工程师阅读，有助于理解如何将机器学习与经典符号执行结合以提升自动化漏洞发现效率。

本文针对可信执行环境（TEE）应用中输入验证缺失导致的安全漏洞检测问题展开研究。由于TEE构建和运行环境的配置成本高、复杂性大，且硬件隔离限制了可观测性，现有安全分析方法难以有效应用于TEE应用。为此，作者提出SymTEE，一种新型的大语言模型（LLM）辅助符号执行框架，无需真实TEE环境即可检测输入验证缺失漏洞。SymTEE首先通过抽象语法树（AST）分析提取TEE代码中可能缺乏充分输入验证的代码片段，然后利用LLM（本文使用GPT-5）自动将提取的片段转换为KLEE兼容的驱动程序（harness program），其中包含轻量级的模拟执行环境，以便进行符号分析。在26个漏洞（11个真实漏洞和15个合成漏洞）上的评估显示，SymTEE在检测输入验证缺失漏洞方面达到了100%的精确率和92.3%的召回率，而每次分析的平均成本仅为0.05美元。该结果证明了SymTEE所开创的LLM辅助符号执行范式的有效性和实用性。该范式通过LLM自主生成模拟环境，无需复杂设置即可实现自动化安全分析，为可信计算系统提供了更易访问和可扩展的框架。

本文针对符号执行中的路径爆炸问题，提出了一种基于路径覆盖的有效路径优先级排序技术Empc。符号执行是一种强大的程序分析技术，能够系统地探索被测试程序的执行路径并检测软件缺陷，但路径爆炸严重限制了其可扩展性和性能。以往的路径优先级排序方法使用静态规则或启发式方法，但往往难以泛化到不同程序。本文的核心洞见在于并非所有路径都需要进行符号推理。与传统方法不同，Empc利用最小路径覆盖（MPC）子集，该子集能覆盖被测试程序的所有代码区域。为了鼓励路径优先级排序的多样性，计算多个MPC。然后，将符号执行的搜索引导到这些MPC内部的少量路径上，而非指数级数量的路径。基于KLEE实现了Empc，并进行了全面评估，涵盖代码覆盖率、漏洞发现和运行时开销。评估结果显示，相比KLEE的最佳搜索策略，Empc的基本块覆盖率提高了19.6%，代码行覆盖率相比最新工作cgs提高了24.4%。此外，Empc比KLEE的最佳搜索策略多发现24个安全违规。同时，Empc可将KLEE的内存使用量最高减少93.5%，符号状态数量最高减少88.6%。该研究适用于软件安全测试和符号执行领域的研究人员。

WCDCAnalyzer 是一篇针对 Wi-Fi 认证设备连接协议（WCDC）的可扩展安全分析论文。研究背景是 Wi-Fi 设备连接协议（如 Wi-Fi Easy Connect、Wi-Fi Direct 等）在智能家居、物联网等场景广泛应用，但现有的安全分析工具通常难以应对协议状态空间爆炸和认证流程复杂的问题。核心问题是如何高效、自动化地检测这些协议中的逻辑漏洞、认证绕过或密钥协商缺陷。论文提出的 WCDCAnalyzer 方法采用符号执行与模型检验结合的方式，将协议规范建模为有限状态机，并利用符号执行探索认证握手过程中的所有可能路径。通过引入抽象化技术和并行化搜索策略，实现了对大规模协议状态空间的可扩展分析。主要贡献包括：设计了一种基于协议规范自动生成安全属性的方法；实现了对 Wi-Fi Easy Connect 和 Wi-Fi Direct 协议的完整分析，发现了多个之前未知的漏洞，如未授权设备配对、中间人攻击风险等；实验表明 WCDCAnalyzer 能够在数小时内完成对复杂协议的分析，而传统方法需要数天。该工作为 Wi-Fi 设备互操作性认证中的安全评估提供了高效工具，适合协议开发者、安全测试人员和认证机构参考。

微控制器固件与硬件紧密耦合，导致动态分析工具难以应用。现有最先进的方法通过观察外设访问模式来自动建模未知外设，并利用启发式策略计算访问未知外设寄存器的响应。然而，经验表明该方法及其启发式策略经常不足以成功模拟固件。本文提出了一种名为uEmu的新方法，用于模拟未知外设的固件执行。与现有工作尝试为每个外设构建通用模型不同，uEmu学习如何在单个外设访问点正确模拟固件执行。它接受固件镜像作为输入，通过将未知外设寄存器表示为符号来进行符号执行。在符号执行过程中，uEmu推断响应未知外设访问的规则，这些规则存储在一个知识库中，供动态固件分析时参考。实验表明，uEmu在一组外设驱动单元测试中无需任何手动辅助即达到95%的通过率。此外，使用真实固件样本进行评估时，uEmu发现了新的漏洞。