論文の概要: 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論理に基づくスマートコントラクトの形式的検証
• Authors: Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, Vadim Malvone,
• 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を活用して、契約が仕様を尊重するかどうかを判断できます。 我々は、翻訳と検証のステップを統合するツールチェーンにアプローチを実装し、複雑な攻撃シナリオをキャプチャするスマートコントラクトと時間特性のベンチマークで、その有効性と性能を評価した。 提案手法は,スマートコントラクトの非自明な時間特性を効果的に検証し,既存の解析ツールの範囲を超えている違反を検出する。

関連論文リスト

• 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)
• 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)
• 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)

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

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