Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
LL-Verifier combines LLMs with logic model checking to automatically discover logic flaws, uncovering vulnerabilities in 27 IoT access-control protocols.
Researchers present LL-Verifier, a framework that uses LLMs to autonomously convert natural-language protocol descriptions and security goals into formal logic models in a new logic language built on Maude, then applies logic model checking for exhaustive verification. The framework targets application-logic flaws that are tied to business semantics and hard to scale with manual analysis. Evaluation on 27 access-control protocols of widely used IoT devices uncovered a range of sophisticated logic vulnerabilities with security and privacy implications.
- LLMs generate formal logic models from natural-language protocol descriptions.
- Models become logical state machines for exhaustive model checking.
- Evaluated on 27 access-control protocols of widely used IoT devices.
- Analysis uncovered sophisticated logic flaws with security and privacy impact.
Full article245 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.10537