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.
42