論文の概要: 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モデルチェッカーを用いて検証する。
我々のモデルは、支払いプロトコルの並行性とエラーセマンティクスの両方をキャプチャする。
次に、プロトコルの正しい中間操作をキャプチャし、両方のチャネルピアに対して結果が常に確実であることを保証するいくつかのセキュリティ特性を定義し、それを使用して、文献で以前に報告された既知の攻撃と、ペイアウトレースと呼ばれる新たな攻撃を再発見する。
ペイアウトレースは特定の一連のイベントで構成されており、無実のユーザーが無意識に資金を失うというプロトコルの曖昧さにつながる可能性がある。
ローカルテストベッド環境下での再現により,本攻撃の実用性を確認した。
関連論文リスト
- BlockFound: Customized blockchain foundation model for anomaly detection [47.04595143348698]
BlockFoundは、異常なブロックチェーントランザクション検出のためのカスタマイズされた基盤モデルである。
ブロックチェーントランザクションのユニークなデータ構造をモデル化するための、一連のカスタマイズデザインを紹介します。
BlockFoundは、Solana上の異常なトランザクションを高精度に検出する唯一の方法である。
論文 参考訳（メタデータ） (2024-10-05T05:11:34Z) - FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols [7.413607595641641]
我々は,DeFiプロトコルの深い論理的バグに対して,非常に効果的な攻撃合成フレームワークであるForayを紹介する。
DSLに基づいて、まず指定されたDeFiプロトコルをトークンフローグラフにコンパイルします。
そこで我々は,特定の攻撃目標に対する攻撃スケッチを合成する効率的なスケッチ生成手法を設計した。
論文 参考訳（メタデータ） (2024-07-08T19:35:48Z) - EmInspector: Combating Backdoor Attacks in Federated Self-Supervised Learning Through Embedding Inspection [53.25863925815954]
フェデレートされた自己教師付き学習(FSSL)は、クライアントの膨大な量の未ラベルデータの利用を可能にする、有望なパラダイムとして登場した。
FSSLはアドバンテージを提供するが、バックドア攻撃に対する感受性は調査されていない。
ローカルモデルの埋め込み空間を検査し,悪意のあるクライアントを検知する埋め込み検査器(EmInspector)を提案する。
論文 参考訳（メタデータ） (2024-05-21T06:14:49Z) - 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) - LookAhead: Preventing DeFi Attacks via Unveiling Adversarial Contracts [15.071155232677643]
分散型金融(DeFi)インシデントは、30億ドルを超える経済的損害をもたらした。
現在の検出ツールは、攻撃活動を効果的に識別する上で重大な課題に直面している。
本稿では,敵対的契約の特定に焦点をあてた,DeFi攻撃検出のための新たな方向を提案する。
論文 参考訳（メタデータ） (2024-01-14T11:39:33Z) - Collaborative Learning Framework to Detect Attacks in Transactions and Smart Contracts [26.70294159598272]
本稿では、ブロックチェーントランザクションとスマートコントラクトの攻撃を検出するために設計された、新しい協調学習フレームワークを提案する。
当社のフレームワークは,マシンコードレベルでの複雑な攻撃を含む,さまざまな種類のブロックチェーン攻撃を分類する機能を示している。
我々のフレームワークは、広範囲なシミュレーションによって約94%の精度を達成し、リアルタイム実験では91%のスループットで毎秒2,150トランザクションを処理している。
論文 参考訳（メタデータ） (2023-08-30T07:17:20Z) - One-bit Flip is All You Need: When Bit-flip Attack Meets Model Training [54.622474306336635]
メモリフォールトインジェクション技術を利用したビットフリップ攻撃(BFA)と呼ばれる新たな重み修正攻撃が提案された。
本稿では,高リスクモデルを構築するための訓練段階に敵が関与する,訓練支援ビットフリップ攻撃を提案する。
論文 参考訳（メタデータ） (2023-08-12T09:34:43Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。