論文の概要: KindHML: formal verification of smart contracts based on Hennessy-Milner logic

• arxiv url: http://arxiv.org/abs/2604.14038v1
• Date: Wed, 15 Apr 2026 16:18:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-16 20:38:32.632638
• Title: KindHML: formal verification of smart contracts based on Hennessy-Milner logic
• Title（参考訳）: KindHML:Hennessy-Milner論理に基づくスマートコントラクトの形式的検証
• Abstract要約: 現実世界の攻撃は、スマートコントラクトのビジネスロジックの欠陥を悪用することが多い。 スマートコントラクトの形式的検証に対する自動的なアプローチを提案する。 提案手法は,スマートコントラクトの非自明な時間特性を効果的に検証できることを示す。
• 参考スコア（独自算出の注目度）: 1.8594711725515678
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks often exploit flaws in the business logic of contracts that unfold across multiple transactions, such as liquidity or front-running attacks. Detecting these attacks requires reasoning about expressive temporal properties beyond the capabilities of existing analysis tools. In this paper, we present an automated approach to the formal verification of smart contracts, enabling the specification and verification of complex temporal properties. Our approach provides a fully automated encoding into Lustre -- the specification language supported by the Kind 2 model checker -- of an expressive subset of Solidity contracts and temporal specifications based on first-order Hennessy-Milner Logic. This encoding allows us to leverage Kind 2 to determine whether the contract respects the specification or not. We implement our approach in a toolchain that integrates the translation and verification steps, and we evaluate its effectiveness and performance on a benchmark of smart contracts and temporal properties capturing complex attack scenarios. Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts and detect violations that are beyond the reach of existing analysis tools.
• Abstract（参考訳）: Ethereumのようなブロックチェーン上にデプロイされたスマートコントラクトは、大量のアセットを日常的に管理する。 実世界の攻撃は、流動性やフロントランニング攻撃など、複数のトランザクションにまたがる契約のビジネスロジックの欠陥をしばしば悪用している。 これらの攻撃を検出するには、既存の分析ツールの能力を超えた表現力のある時間特性の推論が必要である。 本稿では,スマートコントラクトの形式的検証を自動化し,複雑な時間特性の仕様と検証を可能にする。 私たちのアプローチは、Solidityコントラクトの表現力豊かなサブセットと、一階のHennessy-Milner Logicに基づいた一時的な仕様のLustre – Kind 2モデルチェッカーでサポートされている仕様言語に、完全に自動化されたエンコーディングを提供します。 このエンコーディングにより、Kind 2を活用して、契約が仕様を尊重するかどうかを判断できます。 我々は、翻訳と検証のステップを統合するツールチェーンにアプローチを実装し、複雑な攻撃シナリオをキャプチャするスマートコントラクトと時間特性のベンチマークで、その有効性と性能を評価した。 提案手法は,スマートコントラクトの非自明な時間特性を効果的に検証し,既存の解析ツールの範囲を超えている違反を検出する。

関連論文リスト

• Provably Secure Agent Guardrail [89.79561918065122]
  既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。 本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
  論文  参考訳（メタデータ） (2026-05-28T02:12:41Z)
• GoAT-X: A Graph of Auditing Thoughts for Securing Token Transactions in Cross-Chain Contracts [52.51342355102833]
  マルチチェーンエコシステムの重要な基盤であるクロスチェーンブリッジは、攻撃者にとって主要なターゲットとなっている。 バイトコードレベルの静的解析のような既存の防御は、チェーン間の相互作用のセマンティックな複雑さを扱うには不十分である。 パターンマッチングから体系的な第一原理検証へ自動的なクロスチェーンスマートコントラクト監査を移行するフレームワークであるGoAT-Xを提案する。
  論文  参考訳（メタデータ） (2026-04-27T11:34:21Z)
• SmartGraphical: A Human-in-the-Loop Framework for Detecting Smart Contract Logical Vulnerabilities via Pattern-Driven Static Analysis and Visual Abstraction [0.30586855806896046]
  本稿では,論理攻撃面の識別に特化して設計された新しいセキュリティフレームワークであるSmartGraphicalを紹介する。 論理的バグのコンテキスト依存の性質を合成することによって、SmartGraphicalは、視覚化された構造的コンテキスト内で警告を解釈することが可能になる。 このハイブリッド手法は,スマートコントラクトにおける非自明な論理的セキュリティ脅威の解釈可能性と検出率を大幅に向上させることが示唆された。
  論文  参考訳（メタデータ） (2026-03-09T16:35:17Z)
• One Signature, Multiple Payments: Demystifying and Detecting Signature Replay Vulnerabilities in Smart Contracts [56.94148977064169]
  署名の使用状況のチェックが不足すると、繰り返し検証が行われ、許可の不正使用のリスクが増大し、契約資産が脅かされる可能性がある。 我々はこの問題をSignature Replay Vulnerability (SRV) として定義する。 37のブロックチェーンセキュリティ企業を対象とした1,419の監査報告から、詳細なSRV記述と5種類のSRVを分類した108を識別しました。
  論文  参考訳（メタデータ） (2025-11-12T09:17:13Z)
• ContractTrace: Retracing Smart Contract Versions for Security Analyses [4.126275271359132]
  ContractTraceは、スマートコントラクトのバージョンを正確に識別し、コヒーレントなラインにリンクする自動化インフラストラクチャです。 この機能は、脆弱性の伝播パターンを理解し、ブロックチェーン環境におけるセキュリティパッチの有効性を評価するために不可欠である。
  論文  参考訳（メタデータ） (2024-12-30T11:10:22Z)
• Soley: Identification and Automated Detection of Logic Vulnerabilities in Ethereum Smart Contracts Using Large Language Models [1.081463830315253]
  GitHubのコード変更から抽出された実世界のスマートコントラクトのロジック脆弱性を実証的に調査する。 本稿では,スマートコントラクトにおける論理的脆弱性の自動検出手法であるSoleyを紹介する。 スマートコントラクト開発者が実際のシナリオでこれらの脆弱性に対処するために使用する緩和戦略について検討する。
  論文  参考訳（メタデータ） (2024-06-24T00:15:18Z)
• Solvent: liquidity verification of smart contracts [2.680854115314008]
  スマートコントラクト検証ツールの現在の制限は、暗号資産の交換に関する流動性特性の表現と検証に効果がないことである。 我々は,これらの特性の検証を目的とした溶剤について提案する。これは,Solidityの既存の検証ツールの範囲を超えている。
  論文  参考訳（メタデータ） (2024-04-27T10:54:50Z)
• LookAhead: Preventing DeFi Attacks via Unveiling Adversarial Contracts [15.071155232677643]
  DeFi(Decentralized Finance)は、30億ドルを超える損失を計上している。 現在の検出ツールは、攻撃活動を効果的に識別する上で重大な課題に直面している。 敵契約を公開することでDeFi攻撃を検出する新しいフレームワークであるLookAheadを提案する。
  論文  参考訳（メタデータ） (2024-01-14T11:39:33Z)
• Token-Level Adversarial Prompt Detection Based on Perplexity Measures and Contextual Information [67.78183175605761]
  大規模言語モデルは、敵の迅速な攻撃に影響を受けやすい。 この脆弱性は、LLMの堅牢性と信頼性に関する重要な懸念を浮き彫りにしている。 トークンレベルで敵のプロンプトを検出するための新しい手法を提案する。
  論文  参考訳（メタデータ） (2023-11-20T03:17:21Z)
• Enhancing Smart Contract Security Analysis with Execution Property Graphs [48.31617821205042]
  ランタイム仮想マシン用に特別に設計された動的解析フレームワークであるClueを紹介する。 Clueは契約実行中に重要な情報をキャプチャし、新しいグラフベースの表現であるExecution Property Graphを使用する。 評価結果から, クリューの真正率, 偽正率の低い優れた性能が, 最先端のツールよりも優れていた。
  論文  参考訳（メタデータ） (2023-05-23T13:16:42Z)
• Safety Verification of Declarative Smart Contracts [4.303272418564008]
  本稿では,DeCon で記述された宣言型スマートコントラクトを対象とした自動安全検証ツール DCV を提案する。 20のベンチマークコントラクトに対する評価は,DCVがパブリックリポジトリから適応したスマートコントラクトの検証に有効であることを示し,他のツールがサポートしていないコントラクトの検証が可能であることを示唆している。
  論文  参考訳（メタデータ） (2022-11-26T15:02:37Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  既存の機械学習ベースの脆弱性検出方法は制限され、スマートコントラクトが脆弱かどうかのみ検査される。 スマートコントラクトのための初のDeep Neural Network(DNN)ベースの脆弱性検出フレームワークであるESCORTを提案する。 ESCORTは6種類の脆弱性に対して平均95%のF1スコアを達成し,検出時間は契約あたり0.02秒であることを示す。
  論文  参考訳（メタデータ） (2021-03-23T15:04:44Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。