Automated system finds security logic flaws in IoT device protocols
Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
Cryptography and Security
Summary
Logic errors in digital systems can cause serious security and privacy problems, but they are hard to find because they depend on specific business rules and how devices work. The authors created LL-Verifier, a tool that uses AI language models to turn written protocol rules into formal logic expressions, then checks them thoroughly for mistakes. By testing it on 27 different smart device access systems, they found many hidden security weaknesses automatically. This method helps make sure that complex device communication follows safe and correct rules without needing lots of expert time.
logic flawsformal logic modelingautomated reasoningmodel checkinglarge language modelsIoT protocolssecurity analysisaccess controlMaude logic languagevulnerability detection
Authors
Yiwei Fang, Yichen Liu, Ze Jin, Haoqiang Wang, Qixu Liu, Luyi Xing
Abstract
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.