論文の概要: Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
- arxiv url: http://arxiv.org/abs/2609.10537v1
- Date: Wed, 09 Sep 2026 17:58:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-10 19:44:09.14296
- Title: Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
- Title（参考訳）: 自律型形式論理モデリングと自動推論によるアプリケーション論理欠陥への対処
- Abstract要約: LL-Verifierは,大規模言語モデル上に構築された自律モデリングのための論理的脆弱性を識別する自動フレームワークである。
広く使用されているIoTデバイスの27個のアクセス制御プロトコルに適用することにより,LL-Verifierの有効性,効率,実用性を評価した。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 論理の欠陥は、現代的でセマンティックにリッチなシステムやアプリケーションの設計と実装において重大な課題を引き起こし、セキュリティ、プライバシ、信頼に影響を与える。
これらの欠陥は本質的に、ビジネス固有のセマンティクスと脅威モデルに結びついているので、発見と推論が難しく、スケールが難しい。
現実世界のシステムは、しばしば多様なアプリケーション機能、複雑なプロトコルロジック、ドメイン固有の脅威モデルを示し、効果的なセキュリティ分析のためにかなりの人的努力とドメインの専門知識を必要とする。
本稿では,1)自律モデリングのための大規模言語モデルと(2)厳密な推論のための論理モデルチェッカーに基づいて構築された論理的脆弱性を識別する,新しい自動フレームワークであるLL-Verifierを紹介する。
LL-Verifierは自然言語入力、特にプロトコル記述とセキュリティ目標を処理し、任意のアプリケーションレベルのセマンティクスのモデリングに最適化されたジェネリックロジック言語上に構築された新しいロジック言語で表現された形式論理モデルとプロパティを自動的に生成する。
これらの形式モデルは論理状態機械に変換され、論理レベルのモデルチェックを通じて徹底的で厳密な検証を可能にする。
このアプローチは、現実世界のシナリオにデプロイされる多様なアプリケーションレベルのプロトコルの分析を合理化し、論理的制約の中で自動化され、徹底的で正確な推論を提供する。
ベンダー固有の論理フローとセマンティクスを備えた,広く使用されているIoTデバイスの27個のアクセス制御プロトコルに適用することにより,LL-Verifierの有効性,効率,実用性を評価した。
LL検証は、アプリケーションセキュリティの難しい問題、すなわち自動ロジック欠陥発見に対処する一方で、我々の分析は、深刻なセキュリティとプライバシに影響を及ぼすIoTプロトコルやデバイスにおいて、さまざまな高度なロジック脆弱性を明らかにする。
関連論文リスト
- ReasoningLens: Hierarchical Visualization and Diagnostic Auditing for Large Reasoning Models [73.59878306788815]
ReasoningLensは、複雑な推論チェーンの階層的な可視化と診断監査のために設計されたオープンソースのフレームワークである。
ReasoningLensは、(1)高レベルの戦略と低レベルの実行を分離する対話的階層にトレースを構造化し、(2)エージェント監査を自動エラー検出とツール拡張検証に活用する。
論文 参考訳（メタデータ） (2026-06-22T14:28:35Z) - Provably Secure Agent Guardrail [89.79561918065122]
既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。
本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
論文 参考訳（メタデータ） (2026-05-28T02:12:41Z) - LogicScan: An LLM-driven Framework for Detecting Business Logic Vulnerabilities in Smart Contracts [18.126385773266396]
スマートコントラクトにおけるビジネスロジックの脆弱性を検出するための,自動化されたコントラスト監査フレームワークであるLogicScanを提案する。
LogicScanの背景にある重要な洞察は、成熟した、広くデプロイされたオンチェーンプロトコルが、十分にテストされた、コンセンサス駆動のビジネス不変性を暗黙的にエンコードしていることです。
DeFiHacks、Web3Bugs、および上位200の監査済み契約を含む3つの実世界のデータセット上でLogicScanを評価する。
論文 参考訳（メタデータ） (2026-02-03T08:56:53Z) - Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic [23.59512682324697]
大きな言語モデル(LLM)は、コード理解タスクに強いパフォーマンスを示しています。
LLMには、プログラムの振る舞いに関する正確で徹底的な数学的推論を行う能力がない。
本稿では,ImandraXと統合されたソフトウェア論理の精密解析のためのニューロシンボリックエージェントであるCodeLogicianについて述べる。
論文 参考訳（メタデータ） (2026-01-17T00:16:41Z) - Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification [0.0]
本調査では,サイバーセキュリティにおける自動推論の役割について概観する。
我々は、SOTAツールとフレームワークを調べ、ニューラルシンボリック推論のためのAIとの統合を調査し、重要な研究ギャップを浮き彫りにする。
本稿は,安全なシステム開発を促進することを目的とした,先進的な研究の方向性の集合をまとめてまとめる。
論文 参考訳（メタデータ） (2025-03-27T11:41:53Z) - Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers [4.897782942277061]
本稿では,SSV(Semantic Self-Verification)を導入し,自然言語から解法の形式言語への推論問題を正確に定式化する手法を提案する。
SSVは一貫性に基づくアプローチを用いて、モデルによって生成され、解決者によって検証される具体的なインスタンス化を用いて、問題の強力な抽象的な形式化を生成する。
このような*ほぼ確実な推論*は、多くの場合、手動検証の必要性を減らすための新しいアプローチとして提案され、より信頼性が高く自律的なAI推論システムに近づきます。
論文 参考訳（メタデータ） (2025-01-28T14:04:49Z) - Logic Agent: Enhancing Validity with Logic Rule Invocation [24.815341366820753]
Chain-of-Thoughtプロンプトは、推論タスク中に言語モデルの推論能力を増強するための重要なテクニックとして現れている。
本稿では,大規模言語モデルにおける推論プロセスの有効性向上を目的としたエージェントベースのフレームワークであるLogic Agent(LA)を紹介する。
論文 参考訳（メタデータ） (2024-04-28T10:02:28Z) - A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
論理的推論の文脈において,大規模言語モデル(LLM)の自己検証能力について詳しく検討する。
本研究の主目的は,既存のLCMが誤った推論手順を正確に識別するのに苦労し,自己検証法の有効性を保証できないことにある。
論文 参考訳（メタデータ） (2023-11-14T07:13:10Z) - Logically Consistent Adversarial Attacks for Soft Theorem Provers [110.17147570572939]
本稿では,言語モデルの推論能力の探索と改善のための生成的逆説フレームワークを提案する。
我々のフレームワークは、敵の攻撃をうまく発生させ、グローバルな弱点を識別する。
有効探索に加えて, 生成したサンプルのトレーニングにより, 対象モデルの性能が向上することを示す。
論文 参考訳（メタデータ） (2022-04-29T19:10:12Z) - Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
本稿では,プラットフォームに依存しない論理ゲート定義の必要性から,普遍的なフォールトトレラント論理の枠組みを提案する。
資源オーバーヘッドを改善するユニバーサル論理の新しいスキームについて検討する。
境界のない計算に好適な論理誤差率を動機として,新しい計算手法を提案する。
論文 参考訳（メタデータ） (2021-12-22T19:00:03Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。