Fugu-MT 論文翻訳(概要): Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network

論文の概要: Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network

arxiv url: http://arxiv.org/abs/2405.02147v1
Date: Fri, 3 May 2024 14:52:47 GMT
ステータス: 処理完了
システム内更新日: 2024-05-06 12:36:11.030730
Title: Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network
Title（参考訳）: ペイアウトレースと混雑チャネル: 雷ネットワークにおけるセキュリティの形式的分析
Authors: Ben Weintraub, Satwik Prabhu Kumble, Cristina Nita-Rotaru, Stefanie Roos,
Abstract要約: Lightning Networkは、Bitcoinのスケーラビリティ問題を解決するために設計された支払いチャネルネットワークである。いくつかの脆弱性が手作業で発見されたが、これまでLightning Networkのセキュリティを体系的に分析する作業はほとんど行われていない。我々は、正式な手法を用いて、Lightning Networkのセキュリティを分析するための基礎的なアプローチを採っている。
参考スコア（独自算出の注目度）: 8.397189036839956
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: The Lightning Network, a payment channel network with a market cap of over 192M USD, is designed to resolve Bitcoin's scalability issues through fast off-chain transactions. There are multiple Lightning Network client implementations, all of which conform to the same textual specifications known as BOLTs. Several vulnerabilities have been manually discovered, but to-date there have been few works systematically analyzing the security of the Lightning Network. In this work, we take a foundational approach to analyzing the security of the Lightning Network with the help of formal methods. Based on the BOLTs' specifications, we build a detailed formal model of the Lightning Network's single-hop payment protocol and verify it using the Spin model checker. Our model captures both concurrency and error semantics of the payment protocol. We then define several security properties which capture the correct intermediate operation of the protocol, ensuring that the outcome is always certain to both channel peers, and using them we re-discover a known attack previously reported in the literature along with a novel attack, referred to as a Payout Race. A Payout Race consists of a particular sequence of events that can lead to an ambiguity in the protocol in which innocent users can unwittingly lose funds. We confirm the practicality of this attack by reproducing it in a local testbed environment.
Abstract（参考訳）: Lightning Networkは1億2000万USドル以上の時価総額を持つ支払いチャネルネットワークであり、高速なオフチェーントランザクションを通じてBitcoinのスケーラビリティ問題を解決するように設計されている。複数のLightning Networkクライアント実装があり、すべてBOLTsとして知られる同じテキスト仕様に準拠している。いくつかの脆弱性が手作業で発見されたが、これまでLightning Networkのセキュリティを体系的に分析する作業はほとんど行われていない。本研究では,Lightning Networkのセキュリティを形式的手法の助けを借りて解析するための基礎的なアプローチを採る。 BOLTの仕様に基づいて、Lightning Networkのシングルホップ支払いプロトコルの詳細な形式モデルを構築し、Spinモデルチェッカーを用いて検証する。我々のモデルは、支払いプロトコルの並行性とエラーセマンティクスの両方をキャプチャする。次に、プロトコルの正しい中間操作をキャプチャし、両方のチャネルピアに対して結果が常に確実であることを保証するいくつかのセキュリティ特性を定義し、それを使用して、文献で以前に報告された既知の攻撃と、ペイアウトレースと呼ばれる新たな攻撃を再発見する。ペイアウトレースは特定の一連のイベントで構成されており、無実のユーザーが無意識に資金を失うというプロトコルの曖昧さにつながる可能性がある。ローカルテストベッド環境下での再現により,本攻撃の実用性を確認した。

関連論文リスト

Atomic Transfer Graphs: Secure-by-design Protocols for Heterogeneous Blockchain Ecosystems [7.312229214872541]
本稿では,共通セキュリティと機能目標を実現するセキュア・バイ・デザインプロトコルを生成するフレームワークを提案する。その結果生まれたプロトコルは、新しい最小限のスマートコントラクト機能であるTimelock Contracts (CTLC)上に構築される。私たちのフレームワークは、既存のユースケース固有のプロトコルのパフォーマンスをマッチングまたは改善しながら、これらすべてのユースケースに対して、汎用的で証明可能なセキュアなプロトコルを初めて提供します。
論文参考訳（メタデータ） (2025-01-29T17:25:53Z)
CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文参考訳（メタデータ） (2024-11-20T14:16:55Z)
BlockFound: Customized blockchain foundation model for anomaly detection [47.04595143348698]
BlockFoundは、異常なブロックチェーントランザクション検出のためのカスタマイズされた基盤モデルである。ブロックチェーントランザクションのユニークなデータ構造をモデル化するための、一連のカスタマイズデザインを紹介します。 BlockFoundは、Solana上の異常なトランザクションを高精度に検出する唯一の方法である。
論文参考訳（メタデータ） (2024-10-05T05:11:34Z)
Blockchain Amplification Attack [13.13413794919346]
攻撃者は修正ノードのネットワークトラフィックを3,600倍に増幅し,攻撃を行うために必要な約13,800倍の経済的損害を与えることを示す。これらのリスクにもかかわらず、アグレッシブなレイテンシ削減は、修正ノードの存在を正当化するために、さまざまなプロバイダに十分な利益をもたらす可能性がある。
論文参考訳（メタデータ） (2024-08-02T18:06:33Z)
FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols [7.413607595641641]
我々は,DeFiプロトコルの深い論理的バグに対して,非常に効果的な攻撃合成フレームワークであるForayを紹介する。 DSLに基づいて、まず指定されたDeFiプロトコルをトークンフローグラフにコンパイルします。そこで我々は,特定の攻撃目標に対する攻撃スケッチを合成する効率的なスケッチ生成手法を設計した。
論文参考訳（メタデータ） (2024-07-08T19:35:48Z)
Sequencer Level Security [2.756899615600916]
本稿では,ロールアップのシークエンシングプロトコルであるSequencer Level Security (SLS)プロトコルを紹介する。本稿では、ロールアップメムプールに送信されたトランザクションと、レイヤ1から派生したトランザクションの両方に対するプロトコルの仕組みについて述べる。我々は,GethとOPスタック上に構築されたSLSプロトコルであるZircuitのプロトタイプを実装した。
論文参考訳（メタデータ） (2024-05-03T02:47:40Z)
A Formal Analysis of SCTP: Attack Synthesis and Patch Verification [7.331862211069559]
SCTP設計の安全性について検討し,厳密なアプローチを形式的手法に根ざして検討した。攻撃者は仲間のポートとIPを隠蔽できる外部者であり、攻撃者は悪意のあるピアであるEvil-Server、攻撃者が捕獲して再生できるReplay、パケットを変更できないOn-Path、攻撃者がピア間のチャネルを制御するOn-Pathの4つのモデルを定義します。
論文参考訳（メタデータ） (2024-03-08T20:38:56Z)
Combining Graph Neural Networks with Expert Knowledge for Smart Contract Vulnerability Detection [37.7763374870026]
既存の契約のセキュリティ分析の取り組みは、労働集約的でスケーリング不能な専門家によって定義された厳格なルールに依存している。本稿では,正規化グラフからグラフ特徴を抽出する新たな時間的メッセージ伝達ネットワークを提案する。
論文参考訳（メタデータ） (2021-07-24T13:16:30Z)
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)
Online Adversarial Attacks [57.448101834579624]
我々は、実世界のユースケースで見られる2つの重要な要素を強調し、オンライン敵攻撃問題を定式化する。まず、オンライン脅威モデルの決定論的変種を厳格に分析する。このアルゴリズムは、現在の最良の単一しきい値アルゴリズムよりも、$k=2$の競争率を確実に向上させる。
論文参考訳（メタデータ） (2021-03-02T20:36:04Z)
Quantum Multi-Solution Bernoulli Search with Applications to Bitcoin's Post-Quantum Security [67.06003361150228]
作業の証明(英: proof of work、PoW)は、当事者が計算タスクの解決にいくらかの労力を費やしたことを他人に納得させることができる重要な暗号構造である。本研究では、量子戦略に対してそのようなPoWの連鎖を見つけることの難しさについて検討する。我々は、PoWs問題の連鎖が、マルチソリューションBernoulliサーチと呼ばれる問題に還元されることを証明し、量子クエリの複雑さを確立する。
論文参考訳（メタデータ） (2020-12-30T18:03:56Z)

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

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