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

• URL: http://arxiv.org/abs/2609.10537v1
• Date: Wed, 09 Sep 2026 17:58:58 GMT
• Title: Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
• Abstract summary: We introduce LL-Verifier, an automated framework for identifying logic vulnerabilities built on large language models for autonomous modeling.<n>We evaluate the high effectiveness, efficiency, and practicality of LL-Verifier by applying it to 27 access control protocols of widely used IoT devices.
• Score: 12.17092289217073
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• ReasoningLens: Hierarchical Visualization and Diagnostic Auditing for Large Reasoning Models [73.59878306788815]
  ReasoningLens is an open-source framework designed for the hierarchical visualization and diagnostic auditing of complex reasoning chains.<n> ReasoningLens addresses information necropsy by: (1) structuring traces into interactive hierarchies that separate high-level strategy from low-level execution; and (2) leveraging an agentic auditor for automated error detection and tool-augmented verification.
  arXiv  Detail & Related papers  (2026-06-22T14:28:35Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• LogicScan: An LLM-driven Framework for Detecting Business Logic Vulnerabilities in Smart Contracts [18.126385773266396]
  We propose LogicScan, an automated contrastive auditing framework for detecting business logic vulnerabilities in smart contracts.<n>The key insight behind LogicScan is that mature, widely deployed on-chain protocols implicitly encode well-tested and consensus-driven business invariants.<n>We evaluate LogicScan on three real-world datasets, including DeFiHacks, Web3Bugs, and a set of top-200 audited contracts.
  arXiv  Detail & Related papers  (2026-02-03T08:56:53Z)
• Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic [23.59512682324697]
  Large Language Models (LLMs) have shown strong performance on code understanding tasks.<n>LLMs lack the ability to perform precise, exhaustive mathematical reasoning about program behavior.<n>We present CodeLogician, a neurosymbolic agent for precise analysis of software logic, integrated with ImandraX.
  arXiv  Detail & Related papers  (2026-01-17T00:16:41Z)
• Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification [0.0]
  This survey presents a comprehensive overview of the role of automated reasoning in cybersecurity.<n>We examine SOTA tools and frameworks, explore integrations with AI for neural-symbolic reasoning, and highlight critical research gaps.<n>The paper concludes with a set of well-grounded future research directions, aiming to foster the development of secure systems.
  arXiv  Detail & Related papers  (2025-03-27T11:41:53Z)
• Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers [4.897782942277061]
  We introduce Semantic Self-Verification (SSV), a novel approach to accurately formulate the reasoning problem from natural language to the formal language of the solver.<n>SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver.<n>We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.
  arXiv  Detail & Related papers  (2025-01-28T14:04:49Z)
• Logic Agent: Enhancing Validity with Logic Rule Invocation [24.815341366820753]
  Chain-of-Thought prompting has emerged as a pivotal technique for augmenting the inferential capabilities of language models during reasoning tasks.<n>This paper introduces the Logic Agent (LA), an agent-based framework aimed at enhancing the validity of reasoning processes in Large Language Models.
  arXiv  Detail & Related papers  (2024-04-28T10:02:28Z)
• A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
  We take a closer look at the self-verification abilities of large language models (LLMs) in the context of logical reasoning. Our main findings suggest that existing LLMs could struggle to identify fallacious reasoning steps accurately and may fall short of guaranteeing the validity of self-verification methods.
  arXiv  Detail & Related papers  (2023-11-14T07:13:10Z)
• Logically Consistent Adversarial Attacks for Soft Theorem Provers [110.17147570572939]
  We propose a generative adversarial framework for probing and improving language models' reasoning capabilities. Our framework successfully generates adversarial attacks and identifies global weaknesses. In addition to effective probing, we show that training on the generated samples improves the target model's performance.
  arXiv  Detail & Related papers  (2022-04-29T19:10:12Z)
• Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
  We present a framework for universal fault-tolerant logic motivated by the need for platform-independent logical gate definitions. We explore novel schemes for universal logic that improve resource overheads. Motivated by the favorable logical error rates for boundaryless computation, we introduce a novel computational scheme.
  arXiv  Detail & Related papers  (2021-12-22T19:00:03Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.