論文の概要: Certifying optimal MEV strategies with Lean

• arxiv url: http://arxiv.org/abs/2510.14480v1
• Date: Thu, 16 Oct 2025 09:24:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-17 21:15:14.797746
• Title: Certifying optimal MEV strategies with Lean
• Title（参考訳）: リーンで最適なMEV戦略を認定する
• Authors: Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino,
• Abstract要約: 最大抽出可能値(MEV)の機械的定式化について述べる。 MEVは、ブロックチェーン内のトランザクションの順序付け、インクルージョン、排除を操作することで、敵が利益を得る分散アプリケーションに対する攻撃のクラスを指す。 我々は,MEV境界のマシンチェックによる証明を構築する手法を導入し,既存の技術で可能な以上の正確性を保証する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Maximal Extractable Value (MEV) refers to a class of attacks to decentralized applications where the adversary profits by manipulating the ordering, inclusion, or exclusion of transactions in a blockchain. Decentralized Finance (DeFi) protocols are a primary target of these attacks, as their logic depends critically on transaction sequencing. To date, MEV attacks have already extracted billions of dollars in value, underscoring their systemic impact on blockchain security. Verifying the absence of MEV attacks requires determining suitable upper bounds, i.e. proving that no adversarial strategy can extract more value (if any) than expected by protocol designers. This problem is notoriously difficult: the space of adversarial strategies is extremely vast, making empirical studies and pen-and-paper reasoning insufficiently rigorous. In this paper, we present the first mechanized formalization of MEV in the Lean theorem prover. We introduce a methodology to construct machine-checked proofs of MEV bounds, providing correctness guarantees beyond what is possible with existing techniques. To demonstrate the generality of our approach, we model and analyse the MEV of two paradigmatic DeFi protocols. Notably, we develop the first machine-checked proof of the optimality of sandwich attacks in Automated Market Makers, a fundamental DeFi primitive.
• Abstract（参考訳）: 最大抽出可能な価値(MEV)とは、ブロックチェーン内のトランザクションの順序付け、包摂、排除を操作することで敵が利益を得る分散アプリケーションに対する攻撃のクラスを指す。 分散ファイナンス(DeFi)プロトコルは、トランザクションシーケンシングに重要なロジックに依存するため、これらの攻撃の主要なターゲットである。 これまでのところ、MEV攻撃は何十億ドルもの価値を抽出しており、ブロックチェーンのセキュリティに対する同社のシステム的影響を強調している。 MEV攻撃の欠如を検証するには、適切な上限を決定する必要がある。 敵の戦略の空間は極めて広大であり、実証的研究とペンと紙の推論は十分に厳格である。 本稿では、Lean定理証明器におけるMEVの機械的形式化について述べる。 我々は,MEV境界のマシンチェックによる証明を構築する手法を導入し,既存の技術で可能な以上の正確性を保証する。 提案手法の汎用性を実証するために,2つのパラダイム的DeFiプロトコルのMEVをモデル化し,解析する。 特に,基本的DeFiプリミティブであるAutomated Market Makersにおけるサンドイッチ攻撃の最適性のマシンチェックによる最初の証明を開発した。

関連論文リスト

• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  プロトコルとモニタモデルを知っている信頼できないモデルによるアダプティブアタックについて検討する。 我々は、攻撃者がモデル出力に公知またはゼロショットプロンプトインジェクションを埋め込む単純な適応攻撃ベクトルをインスタンス化する。
  論文  参考訳（メタデータ） (2025-10-10T15:12:44Z)
• Maximal Extractable Value in Decentralized Finance: Taxonomy, Detection, and Mitigation [0.534772724436823]
  最大抽出可能な値(MEV)は、ブロックチェーン上の金融トランザクションから抽出することができる。 MEVは、DeFiエコシステムのセキュリティ、効率、分散化目標を破壊し、金融損失とコンセンサス不安定を引き起こす。 この調査は、研究者、開発者、利害関係者、政策立案者に貴重な洞察を提供する。
  論文  参考訳（メタデータ） (2024-10-22T12:11:41Z)
• Maximal Extractable Value Mitigation Approaches in Ethereum and Layer-2 Chains: A Comprehensive Survey [1.2453219864236247]
  MEVは、採掘者またはバリデーターが追加の値を抽出するためにトランザクションオーダを操作するときに発生する。 これは、予測不可能と潜在的損失を導入することによってユーザエクスペリエンスに影響を与えるだけでなく、分散化と信頼の根底にある原則を脅かす。 本稿では, プロトコルL1と各種L2ソリューションの両方に適用したMEV緩和技術に関する包括的調査を行う。
  論文  参考訳（メタデータ） (2024-07-28T19:51:22Z)
• Avoid Adversarial Adaption in Federated Learning by Multi-Metric Investigations [55.2480439325792]
  Federated Learning(FL)は、分散機械学習モデルのトレーニング、データのプライバシの保護、通信コストの低減、多様化したデータソースによるモデルパフォーマンスの向上を支援する。 FLは、中毒攻撃、標的外のパフォーマンス劣化とターゲットのバックドア攻撃の両方でモデルの整合性を損なうような脆弱性に直面している。 我々は、複数の目的に同時に適応できる、強い適応的敵の概念を新たに定義する。 MESASは、実際のデータシナリオで有効であり、平均オーバーヘッドは24.37秒である。
  論文  参考訳（メタデータ） (2023-06-06T11:44:42Z)
• A theoretical basis for MEV [0.9208007322096532]
  実証的な研究によると、主流のDeFiプロトコルはこれらの攻撃によって非常に標的になっている。 本稿では,ブロックチェーンとスマートコントラクトの一般的な抽象モデルに基づくMEVの形式理論を提案する。 私たちの理論は、MEV攻撃に対するセキュリティの証明の基盤となっている。
  論文  参考訳（メタデータ） (2023-02-04T12:13:29Z)
• Versatile Weight Attack via Flipping Limited Bits [68.45224286690932]
  本研究では,展開段階におけるモデルパラメータを変更する新たな攻撃パラダイムについて検討する。 有効性とステルスネスの目標を考慮し、ビットフリップに基づく重み攻撃を行うための一般的な定式化を提供する。 SSA(Single sample attack)とTSA(Singr sample attack)の2例を報告した。
  論文  参考訳（メタデータ） (2022-07-25T03:24:58Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  垂直ロジスティック回帰(VLR)をミニバッチ降下勾配で訓練した。 我々は、オープンソースのフェデレーション学習フレームワークのクラスにおいて、VLRの包括的で厳密なプライバシー分析を提供する。
  論文  参考訳（メタデータ） (2022-07-19T05:47:30Z)
• Online Adversarial Attacks [57.448101834579624]
  我々は、実世界のユースケースで見られる2つの重要な要素を強調し、オンライン敵攻撃問題を定式化する。 まず、オンライン脅威モデルの決定論的変種を厳格に分析する。 このアルゴリズムは、現在の最良の単一しきい値アルゴリズムよりも、$k=2$の競争率を確実に向上させる。
  論文  参考訳（メタデータ） (2021-03-02T20:36:04Z)
• A Self-supervised Approach for Adversarial Robustness [105.88250594033053]
  敵対的な例は、ディープニューラルネットワーク(DNN)ベースの視覚システムにおいて破滅的な誤りを引き起こす可能性がある。 本稿では,入力空間における自己教師型対向学習機構を提案する。 これは、反逆攻撃に対する強力な堅牢性を提供する。
  論文  参考訳（メタデータ） (2020-06-08T20:42:39Z)

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

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