論文の概要: SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients
- arxiv url: http://arxiv.org/abs/2608.17738v1
- Date: Tue, 18 Aug 2026 13:03:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-19 21:40:53.340585
- Title: SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients
- Title（参考訳）: SpecTrum:Ethereum Consensusクライアントのための仕様ガイド付き差分ファジィ
- Abstract要約: 本稿では,コンセンサスアルゴリズムの機械的仕様であるConsensus-SpecTecを紹介する。
この問題に3段階で対処するフレームワークであるSpecTrumも紹介する。
うち22例は,機械化に挿入された施設がなければ見つからない。
- 参考スコア（独自算出の注目度）: 3.016888279148097
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Ethereum's consensus safety relies on independent consensus client implementations agreeing on every state transition. When they diverge due to implementation errors, the network can fork, finality can stall, and severe attacks are possible. To prevent such consensus divergences, Ethereum provides a Python reference implementation (consensus-spec), which acts as a specification, and a hand-crafted official test suite (spectests). However, as an executable implementation, Ethereum's specification defines validity implicitly through runtime behavior. As a result, it lacks a systematic way to ensure that all validity conditions are thoroughly evaluated. We present SpecTrum, a framework that addresses this problem in three stages. First, we introduce Consensus-SpecTec, a mechanized specification of the Ethereum consensus algorithm, which makes validity conditions explicit as if-premises. Second, we define premise coverage, a metric that measures which if-premises are evaluated to true and false across spectests. Third, we develop a specification-based test generator that extracts constraints on premises not evaluated to false by spectests and generates inputs to evaluate them. Applying SpecTrum to five major Ethereum consensus clients, we identify 27 cross-client divergence cases, 22 of which cannot be found without the premises inserted in our mechanization. All 27 cases reproduce across fork versions, and extending the mechanized specification to a new fork takes modest effort proportional to the specification difference.
- Abstract（参考訳）: Ethereumのコンセンサス安全性は、すべての状態遷移に同意する独立したコンセンサスクライアント実装に依存している。
実装エラーによって分岐した場合、ネットワークはフォークし、最終性は停止し、深刻な攻撃が可能である。
このようなコンセンサスの違いを防ぐため、Ethereumは、仕様として機能するPythonリファレンス実装(consensus-spec)と、手作りの公式テストスイート(spectests)を提供する。
しかし、実行可能実装として、Ethereumの仕様は実行時の振る舞いを通じて暗黙的に妥当性を定義している。
結果として、すべての妥当性条件が徹底的に評価されることを保証する体系的な方法が欠如している。
この問題に対処するフレームワークSpecTrumを3段階に分けて紹介する。
まず,Ethereumコンセンサスアルゴリズムの機械的仕様であるConsensus-SpecTecを紹介する。
第二に、前提カバレッジ、つまり、もし前提がテスト全体で真で偽であると評価されるかどうかを測定する指標を定義します。
第3に,仕様に基づくテストジェネレータを開発し,提案手法を用いて評価されていない前提条件の制約を抽出し,評価するインプットを生成する。
SpecTrumを5つの主要なEthereumコンセンサスクライアントに適用することで、27のクロスクライアント分岐ケースを特定します。
27のケースはすべてフォークバージョン間で再現され、機械化された仕様を新しいフォークに拡張するには、仕様の違いに比例する程度の労力がかかります。
関連論文リスト
- ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。
本稿では,3値の証明カバレッジモデルを用いて,仕様品質を診断するDafny用ツールであるProgrampulseを提案する。
論文 参考訳（メタデータ） (2026-08-31T14:00:31Z) - SpecPath: Testing Coding Agents Across Contract-Equivalent Specification Histories [13.437222222971272]
仕様パスの感度は、最終的な意味において等価な要求履歴が同一のエージェントシステムに振る舞いの異なるプログラムを作成させる障害モードである。
本稿では,契約に至るリビジョンパスのみを変更しつつ,リポジトリ,最終契約,検証,エージェントシステム,実行予算を保持する診断評価であるSpecPathを紹介する。
論文 参考訳（メタデータ） (2026-08-10T16:19:00Z) - Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。
この問題は、事前評価が結果駆動である変換において特に深刻である。
ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。
このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
論文 参考訳（メタデータ） (2026-05-27T19:57:15Z) - Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
論文 参考訳（メタデータ） (2026-04-29T09:57:07Z) - CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。
CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。
リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
論文 参考訳（メタデータ） (2026-04-14T04:31:45Z) - When Specifications Meet Reality: Uncovering API Inconsistencies in Ethereum Infrastructure [16.114947403968326]
APIDifferは、最初の仕様誘導差分テストフレームワークである。
API仕様を包括的なテストスイートに変換する。
APIDifferは72のバグを発見し、90.28%はすでに開発者によって確認または修正されている。
論文 参考訳（メタデータ） (2026-03-06T08:28:44Z) - Proof of Trusted Execution: A Consensus Paradigm for Deterministic Blockchain Finality [0.391985484065646]
本稿では,再実行を再現するのではなく,合意が検証実行から生じる合意パラダイムとして,信頼された実行の証明(PoTE)を提案する。
実行は決定論的であり、プロポーサは公開ランダム性から一意に派生しているため、PoTEはフォークを避け、スロット・タイムのボトルネックを排除し、1ラウンドの検証でブロックをコミットする。
論文 参考訳（メタデータ） (2025-12-10T08:04:38Z) - SConU: Selective Conformal Uncertainty in Large Language Models [59.25881667640868]
SconU(Selective Conformal Uncertainity)と呼ばれる新しいアプローチを提案する。
我々は,特定の管理可能なリスクレベルで設定されたキャリブレーションの不確実性分布から,与えられたサンプルが逸脱するかどうかを決定するのに役立つ2つの共形p値を開発する。
我々のアプローチは、単一ドメインと学際的コンテキストの両方にわたる誤発見率の厳密な管理を促進するだけでなく、予測の効率を高める。
論文 参考訳（メタデータ） (2025-04-19T03:01:45Z) - Conformal Prediction Sets with Improved Conditional Coverage using Trust Scores [52.92618442300405]
有限サンプルにおいて、正確に分布のない条件付きカバレッジを達成することは不可能である。
本稿では,最も重要となる範囲を対象とするコンフォメーション予測アルゴリズムを提案する。
論文 参考訳（メタデータ） (2025-01-17T12:01:56Z) - Short Paper: Accountable Safety Implies Finality [10.589723476970443]
ビザンチン・フォールト耐性(BFT)状態機械複製(SMR)コンセンサスプロトコルについて、2つの重要なデシラタが研究されている。
説明責任の安全性が最終性を意味することを示し、その結果、以前の結果を統一する。
論文 参考訳（メタデータ） (2023-08-31T17:58:38Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳（メタデータ） (2021-09-25T22:53:24Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。