本研究针对微控制器（MCU）为基础的物联网设备中常用的嵌入式实时操作系统（RTOS）的安全性问题展开分析。初步研究发现，FreeRTOS等流行RTOS缺乏基本的安全保护机制；而Zephyr OS和ThreadX虽已具备基本安全保护，但其系统调用参数过滤机制存在显著差异。具体而言，ThreadX为实现性能优化而采取的一种做法引入了安全漏洞，使得攻击者能够绕过参数过滤过程。基于此，研究者提出了一种名为“内核对象伪装攻击（KOM Attack）”的新型攻击方法——攻击者通过精心选择的系统调用操控一个或多个内核对象，从而访问内核对象中的敏感字段，可能导致数据未授权篡改、权限提升或系统完全沦陷。为系统化挖掘此类漏洞，论文开发了一种基于欠约束符号执行的自动化分析框架，能够识别KOM攻击并理解其影响。实验在搭载ThreadX的平台上验证了KOM攻击的可行性。研究团队已将发现报告给厂商，亚马逊和微软已确认漏洞并在其网站上致谢。该工作揭示了RTOS性能优化与安全性之间的权衡，为嵌入式系统安全设计提供了重要参考。

该论文提出 CryptoBap，一个用于验证加密协议二进制代码安全属性的平台。研究背景是：现实中的加密协议实现可能因编译器优化、平台差异或编程错误而引入安全漏洞，而传统的形式化验证方法通常针对高级语言或协议规范，难以直接分析编译后的机器码。核心问题是如何在二进制层面自动验证协议的弱保密性和认证属性。方法上，CryptoBap 首先将 ARMv8 和 RISC-V 架构的协议二进制代码反编译为中间表示（IR），然后执行密码感知的符号执行，自动提取覆盖所有执行路径的协议模型。符号执行过程支持间接跳转解析和基于循环总结技术的有限循环处理，完全自动化。提取的模型通过第三方工具链转换为 ProVerif 或 CryptoVerif 可接受的输入格式，从而利用这些成熟的自动验证器完成安全属性证明。论文证明了该方法的可靠性（soundness），并通过多个案例验证了平台的有效性，包括玩具示例以及真实协议 TinySSH（SSH 实现）和 WireGuard（现代 VPN 协议）。实验结果表明，CryptoBap 能够成功提取协议模型并验证安全属性，且运行效率可接受。该工作的主要贡献在于：1）首个结合二进制翻译、密码感知符号执行和自动验证器链的集成平台；2）针对 ARMv8 和 RISC-V 指令集的支持；3）对真实世界协议的成功验证。适合的研究读者包括形式化验证、二进制分析、加密协议实现安全性领域的研究人员。

该论文研究通用程序的堆布局操纵（Heap Layout Manipulation, HLM）自动化问题。堆布局操纵是漏洞利用中的关键步骤，攻击者通过控制堆内存的分配和释放顺序，将关键对象放置在可被利用的内存位置。传统方法依赖于专家手动构造，耗时且容易出错，且缺乏通用性。本文提出一种自动且精确的HLM方法，适用于通用程序。核心思路是将HLM问题形式化为一个规划问题，通过符号执行和约束求解来生成满足特定布局所需的输入序列。作者设计了一个框架，包含三个主要组件：堆状态分析器（Heap State Analyzer）用于提取程序对堆操作的行为模型；布局规划器（Layout Planner）基于行为模型和期望布局目标，生成一系列堆操作步骤；输入生成器（Input Generator）将操作步骤转化为具体的程序输入。实验在多个真实世界程序（如Web服务器、数据库）上进行，证明了该方法能够自动生成有效堆布局，成功率超过90%，且生成的布局与手动构造的质量相当。主要贡献包括：首次提出自动化的通用HLM方法、形式化定义HLM问题、实现原型系统并验证有效性。该工作有助于安全研究者理解攻击技术，并为防御方开发堆布局随机化或异常检测提供参考。

符号执行是一种强大的程序分析技术，广泛应用于漏洞检测、安全测试和恶意软件分析等领域。然而，该技术面临可扩展性问题，例如路径爆炸和复杂约束，这些问题往往源于真实程序中常见的特定结构和语义模式。现有方法尝试通过将程序转换为新表示来规避这些模式，从而降低执行开销。但遗憾的是，这些变换通常过于僵化，难以利用多样的局部程序语义，有时甚至依赖为具体执行设计的编译器优化，可能与符号执行的目标不一致。为此，本文提出了Symbolon框架，该框架能够自动学习多样化的代码变换，并以上下文敏感的方式应用这些变换来改进符号执行。其核心思想是将变换发现表述为程序表示上的搜索问题。为了使搜索实用化，Symbolon在离线状态下对小规模程序进行低成本学习，将学到的变换精炼成可重用的智能体技能库，然后利用智能体在仓库级目标上实例化这些技能。评估表明，在32个真实程序上，Symbolon采用16种搜索策略，均显著提升了符号执行引擎KLEE的性能：平均行覆盖率提高了3.69倍，峰值内存降低了29.2倍，每次查询的求解时间降低了123倍。当应用于最新的Linux内核时，Symbolon发现了21个以前未知的漏洞，所有漏洞均已报告给内核维护者。

网络入侵检测系统（NIDS）常因实现层面的差异而被绕过：攻击者精心构造的数据包在NIDS和最终主机上的处理方式不同，导致NIDS无法检测。这些差异源于大量端主机实现及其演化，NIDS通常采用简化实现来近似和泛化，但这种方式存在根本缺陷，因为近似必然与某些端主机实现存在偏差。本文提出轻量级系统Themis，旨在使NIDS能够识别这些差异，并在遇到“歧义”数据包时被动地分叉连接状态。Themis包含离线阶段：利用符号执行从多种流行实现中提取模型；运行时阶段：维护一个非确定有限自动机（NFA）来跟踪每种可能实现的状态。广泛评估表明，Themis极其有效，能够检测所有已知的规避攻击，同时开销极低。在研究过程中，作者还发现了多个此前未知的、可用于绕过当前NIDS的差异。该工作为NIDS防御实现级绕过攻击提供了新思路，适合安全研究员和NIDS开发者阅读。

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发现了新的漏洞。