論文の概要: Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source
- arxiv url: http://arxiv.org/abs/2606.01794v2
- Date: Tue, 02 Jun 2026 14:01:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-03 18:57:50.469743
- Title: Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source
- Title（参考訳）: 生産展開固体源に対するスマートコントラクト保持の3方向判別パワー形式検証
- Authors: Ray Iskander,
- Abstract要約: OpenZeppelinのReentrancy-guardパターンの最初の正当性証明は、プロダクションデプロイされたSolidityソースのLean 4ステートマシンモデルに対するものだ。
スマートコントラクトの継続は2016年以降、記録された損失として5億ドル以上を突破した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present the first machine-checked correctness proof of the OpenZeppelin reentrancy-guard pattern against a Lean 4 state-machine model of production-deployed Solidity source. All thirteen theorems are machine-checked with zero sorry, zero user-introduced axioms, and an axiom footprint bounded by [propext] (a standard mathlib4 axiom), gated under continuous integration. Smart contract reentrancy has caused over US$500M in documented losses since 2016, with the DAO 2016 attack draining ~3.6M ETH and forcing the hard fork that split Ethereum. The OpenZeppelin ReentrancyGuard pattern is the de facto defense across production DeFi, yet no prior work has established its discriminating power: that the guard blocks attacks on vulnerable instances, preserves correct execution for non-attacking transactions, and distinguishes adjacent safe and vulnerable variants. Prior efforts formalized either guard correctness on toy contracts or attack feasibility on isolated instances - not both directions plus boundary cases against production source. We verify three production instantiations - DAO 2016, Compound v2, and Aave V3 flashLoan - plus a minimal-diff mutant of Aave V3's flashLoan (flashLoanVulnerable) isolating one security-critical difference, via mutation testing. The tridirectional structure pairs (a) attack reproduction of the DAO 2016 pattern, (b) a correctness proof for Compound v2, and (c) a boundary-case proof distinguishing Aave V3's CEI-correct flashLoan from the mutant. A capstone meta-theorem composes the three under a no-retrofit discipline, demonstrated at the first cross-protocol stress test (Compound v2 to Aave V3); broader-family portability is future work. Full Lean 4 source, CI config and reproduction commands are at https://github.com/rayiskander2406/qanary-contracts, reproducible at v1.6-phase7-closure (substrate: v1.3-layer6-closure).
- Abstract（参考訳）: 本稿では,OpenZeppelin Reentrancy-guardパターンのマシンチェックによる最初の正当性証明について述べる。
13の定理はすべて機械チェックされ、ゼロ不注意、ゼロユーザ導入公理、[propext](標準数学のlib4公理)で束縛された公理フットプリントが連続積分の下で公理化される。
2016年以降、スマートコントラクトの維持は5億ドル以上の損失をもたらし、DAO 2016攻撃は3.6M ETHに減少し、Ethereumを分割するハードフォークを強制した。
OpenZeppelin ReentrancyGuardパターンは、プロダクション間での事実上の防御DeFiだが、その識別能力を確立した以前の作業では、ガードが脆弱なインスタンスに対する攻撃をブロックし、非攻撃的なトランザクションに対する正しい実行を保存し、隣接する安全で脆弱な亜種を区別する、というものだった。
以前の取り組みは、おもちゃの契約に対する正当性を守るか、独立したインスタンスに対する実行可能性を攻撃するかのどちらかを形式化した。
DAO 2016 Compound v2 と Aave V3 flashLoan と Aave V3 の flashLoan (flashLoanVulnerable) の最小差のミュータントは、突然変異テストを通じて1つのセキュリティクリティカルな違いを分離する。
三方向構造対
(a)DAO 2016パターンのアタック再生
b) 化合物v2の正当性証明及び
c) Aave V3 の CEI-correct flashLoan を変異体と区別する境界ケース証明。
キャップストーンメタ理論は、最初のクロスプロトコール応力試験(英語版)(v2 to Aave V3)で実証された、不適合な規律の下で3つの理論を構成する。
完全なLean 4ソース、CI設定、再現コマンドはhttps://github.com/rayiskander2406/qanary-contractsで、v1.6-phase7-closureで再現可能である。
関連論文リスト
- Mythos and the Unverified Cage: Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure [0.0]
一部の二次アカウントはサンドボックスネットワークコードにCWE-190算術的脆弱性を仮定している。
本稿では,C/C++ インフラストラクチャにおける CWE-190/191/195 の算術的脆弱性パターンを,Z3 SMT ベースの形式検証エンジンである COBALT について述べる。
提案する: COBALT, VERDICT, DIRECTIVE-4, SENTINEL, 事前デプロイ検証, 事前実行制約, 出力制御, 実行時の監視をMythosインシデントによって公開された障害モードにマッピングする4層封じ込めフレームワーク。
論文 参考訳（メタデータ） (2026-04-22T12:28:23Z) - Harness as an Asset: Enforcing Determinism via the Convergent AI Agent Framework (CAAF) [0.0]
大規模言語モデルは、安全クリティカルエンジニアリングにおける制御可能性のギャップを生み出します。
本稿では,エージェントをオープンループ生成からクローズループフェールセーフ決定性に移行するConvergent AI Agent Framework(CAAF)を紹介する。
CAAFの3つの柱は相補的な故障面に対処し、コモディティコストで制御可能性ギャップを閉じることはない。
論文 参考訳（メタデータ） (2026-04-18T15:15:09Z) - The Defense Trilemma: Why Prompt Injection Defense Wrappers Fail? [0.4563346097310683]
モデルがそれを見る前に入力を前処理する$D: Xto X$は、接続されたプロンプト空間を持つ言語モデルに対して、すべての出力を厳格に安全にする。
論文 参考訳（メタデータ） (2026-04-07T20:20:18Z) - RAGEN-2: Reasoning Collapse in Agentic RL [123.40730283427136]
RAGEN-2では、安定なエントロピーであっても、モデルは多様に見えるが入力に依存しない固定テンプレートに依存することができる。
推論品質をインテリアインプットの多様性(エントロピー)とクロスインプットの区別可能性(Mutual Information, MI)に分解する。
様々なタスクにおいて、相互情報はエントロピーよりも最終的なパフォーマンスと非常に強く関連しているため、推論品質のより信頼性の高いプロキシとなります。
論文 参考訳（メタデータ） (2026-04-07T04:29:41Z) - Burau representation, Squier's form, and non-Abelian anyons [53.92822954974537]
ブレイド群 $B_3$ のブラウ表現から構築した周波数可変2次元非アベリア的演算順序制御を導入する。
Squier 陽性ウィンドウの向こう側にある$Delta(omega)$の符号変更は、因果順序の交互に構成的かつ破壊的干渉を示す。
数値シミュレーションにより、拡張と抑制の両方が確認され、最小の$B_3$ブレイド制御が確立される。
論文 参考訳（メタデータ） (2025-10-21T00:25:21Z) - Building a Foundational Guardrail for General Agentic Systems via Synthetic Data [76.18834864749606]
LLMエージェントは、計画段階で介入するマルチステップタスクを計画できる。
既存のガードレールは主にポスト・エグゼクティブ(英語版)を運用しており、スケーリングが困難であり、計画レベルで制御可能な監督を行う余地がほとんどない。
我々は、良性軌道を合成し、カテゴリーラベル付きリスクを困難に注入し、自動報酬モデルを介して出力をフィルタリングする制御可能なエンジンであるAuraGenを紹介する。
論文 参考訳（メタデータ） (2025-10-10T18:42:32Z) - Sequential Diffusion Language Models [110.06562906987052]
拡散言語モデル(DLM)は理論効率が強いが、固定長の復号化とキー値キャッシュとの非互換性によって制限される。
次点と次点の予測を統一するNext Sequence Prediction (NSP)を導入する。
本稿では,事前学習した自己回帰言語モデル(ALM)を最小限のコストで再現可能な逐次拡散言語モデル(SDLM)を提案する。
論文 参考訳（メタデータ） (2025-09-28T17:59:15Z) - MISLEADER: Defending against Model Extraction with Ensembles of Distilled Models [56.09354775405601]
モデル抽出攻撃は、クエリアクセスを通じてブラックボックスモデルの機能を複製することを目的としている。
既存のディフェンスでは、アタッカークエリにはオフ・オブ・ディストリビューション(OOD)サンプルがあることを前提としており、不審な入力を検出し破壊することができる。
OOD仮定に依存しない新しい防衛戦略であるMISLEADERを提案する。
論文 参考訳（メタデータ） (2025-06-03T01:37:09Z) - Emulated Disalignment: Safety Alignment for Large Language Models May Backfire! [65.06450319194454]
大きな言語モデル(LLM)は、人間との安全な会話を確保するために安全アライメントを行う。
本稿では,安全アライメントの反転が可能なトレーニングフリーアタック手法を提案する。
本手法をエミュレートした脱アライメント (ED) と呼ぶのは, このコントラスト分布からのサンプリングは, 安全報酬を最小限に抑えるため, 微調整の結果を確実にエミュレートするからである。
論文 参考訳（メタデータ） (2024-02-19T18:16:51Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。