发表机构
Institute of Information Engineering, Chinese Academy of Sciences; University of Illinois Urbana-Champaign（中国科学院信息工程研究所; 伊利诺伊大学厄巴纳-香槟分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出LL-Verifier框架，结合大语言模型自主建模与逻辑模型检查器，自动生成形式逻辑模型并验证，成功在27个物联网访问控制协议中发现多种复杂逻辑漏洞。
AI 中文摘要
逻辑缺陷对现代语义丰富的系统和应用的设计与实现构成重大挑战，影响安全性、隐私性和信任。这些缺陷本质上与业务特定语义和威胁模型相关联，使得其发现和推理困难且难以扩展。现实世界的系统通常展现出多样化的应用特性、复杂的协议逻辑和特定领域的威胁模型，需要大量人力和领域专业知识才能进行有效的安全分析。在本文中，我们介绍了LL-Verifier，一种新颖的自动化框架，用于识别逻辑漏洞，它基于（1）用于自主建模的大型语言模型，以及（2）用于严格推理的逻辑模型检查器。LL-Verifier处理自然语言输入，特别是协议描述和安全目标，以自动生成形式逻辑模型和属性，这些模型和属性用基于通用逻辑语言Maude的新逻辑语言表达，该语言针对任意应用级语义的建模进行了优化。这些形式模型随后被转换为逻辑状态机，通过逻辑级模型检查实现详尽、严格的验证。该方法简化了对现实场景中部署的各种应用级协议的分析，在其逻辑约束内提供自动化、详尽且精确的推理。我们通过将LL-Verifier应用于广泛使用的物联网设备的27个访问控制协议（这些协议具有供应商特定的逻辑流程和语义）来评估其高效性、有效性和实用性。尽管LL-Verifier处理的是应用安全中的一个难题，即自动逻辑缺陷发现，但我们的分析揭示了物联网协议和设备中的一系列复杂逻辑漏洞，这些漏洞具有严重的安全和隐私影响。
英文摘要
Logic flaws pose significant challenges in the design and implementation of modern, semantically rich systems and applications, impacting security, privacy, and trust. These flaws are inherently tied to business-specific semantics and threat models, making their discovery and reasoning difficult and hard to scale. Real-world systems often exhibit diverse application features, complex protocol logic, and domain-specific threat models, necessitating substantial human effort and domain expertise for effective security analysis. In this paper, we introduce LL-Verifier, a novel, automated framework for identifying logic vulnerabilities built on (1) large language models for autonomous modeling, and (2) logic model checkers for rigorous reasoning. LL-Verifier processes natural language inputs, in particular protocol descriptions and security goals, to automatically generate formal logic models and properties expressed in a new logic language built on a generic logic language Maude, optimized for modeling arbitrary application-level semantics. These formal models are then converted into logical state machines, enabling exhaustive, rigorous verification through logic level model checking. This approach streamlines the analysis of diverse, application-level protocols deployed in real-world scenarios, offering automated, exhaustive, and precise reasoning within their logical constraints. We evaluated the high effectiveness, efficiency, and practicality of LL-Verifier by applying it to 27 access control protocols of widely used IoT devices, which come with vendor-specific logic flows and semantics. While LL-verifier tackles a hard problem in application security, i.e., automatic logic flaws discovery, our analysis uncovers a range of sophisticated logic vulnerabilities in IoT protocols and devices with serious security and privacy implications.
Comments13 pages, 3 figures, 3 tables
