LL-Verifier 通过自主形式化建模与自动推理发现 IoT 协议中的业务逻辑漏洞

该论文提出 LL-Verifier 框架，利用大语言模型进行自主建模并结合逻辑模型检查器进行严格推理，以自动识别应用程序中的逻辑漏洞。系统接收自然语言输入（如协议描述和安全目标），生成基于通用逻辑语言 Maude 的新逻辑语言的形式化模型，并将其转换为逻辑状态机进行穷尽式验证。

作者在 27 种广泛使用的 IoT 设备的访问控制协议上进行了评估，这些设备具有厂商特定的逻辑流和语义。实验结果显示，LL-Verifier 能够发现一系列复杂的逻辑漏洞，这些漏洞在安全和隐私方面具有严重的影响。该方法旨在解决应用安全中自动发现逻辑缺陷这一难题，通过自动化、穷尽且精确的推理来简化对现实场景中部署的各种应用级协议的分析。

事实层面，该研究确实构建并测试了 LL-Verifier 框架，并在特定数据集上发现了漏洞。推断层面，这种结合 LLM 与形式化验证的方法可能成为未来应用层安全分析的标准工具之一，特别是在处理复杂业务逻辑时。猜测层面，虽然结果积极，但其在更广泛的非 IoT 场景或不同协议类型中的泛化能力仍需进一步验证，且目前尚未提及该框架是否已开源或集成到现有安全流程中。