Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要