通过 LLM 辅助符号执行查找 TEE 中丢失的输入验证

可信执行环境 (TEE) 提供硬件强制隔离，保护敏感代码和数据免受不可信软件的侵害。尽管具有强大的安全保证，但由于配置完整的 TEE 构建和运行时环境的高成本和复杂性，以及硬件隔离带来的可观察性有限，分析 TEE 应用程序仍然具有挑战性。本文介绍了 SymTEE，这是一种新颖的 大语言模型 (LLM) 辅助符号执行框架，用于检测 TEE 应用程序中丢失的输入验证问题，而无需真正的 TEE 设置。 SymTEE 首先利用抽象语法树 (AST) 分析来提取可能缺乏足够输入验证的 TEE 代码切片，然后使用 LLM（在我们的示例中为 GPT-5）将提取的切片自动转换为 KLEE 兼容的工具程序，其中包含用于符号分析的轻量级模拟执行环境。对 26 个漏洞（11 个真实漏洞和 15 个合成漏洞）的评估表明，SymTEE 在检测缺失输入验证漏洞方面实现了 100% 的精确度和 92.3% 的召回率，而平均分析成本仅为 0.05 美元。这些结果证明了 SymTEE LLM 辅助符号执行的开创性范例的有效性和实用性，其中 LLM 自主生成模拟环境，无需复杂的设置即可实现自动化安全分析，为可信计算系统提供更易于访问和扩展的框架。