arxiv.orgpaper

Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning

LL-Verifier is a research framework that uses LLMs to autonomously translate natural-language protocol descriptions and security goals into formal logic models (built on the Maude language) and security properties, which are then exhaustively checked by a logic model checker to uncover application logic flaws. The authors applied it to 27 access control protocols from widely used IoT devices and found multiple previously unknown, vendor-specific logic vulnerabilities with real security/privacy impact, demonstrating a scalable alternative to manual expert-driven logic flaw analysis.