支付竞速与通道拥堵：闪电网络安全性的一种形式化分析

闪电网络是一个市值超过1.92亿美元的支付通道网络，旨在通过快速的链下交易解决比特币的可扩展性问题。存在多种闪电网络客户端实现，它们都遵循被称为BOLT的相同文本规范。已有多个漏洞被人工发现，但迄今为止，系统性地分析闪电网络安全性的工作寥寥无几。在这项工作中，我们借助形式化方法，采用基础性的方法来分析闪电网络的安全性。基于BOLT规范，我们构建了闪电网络单跳支付协议的详细形式化模型，并使用Spin模型检测器对其进行验证。我们的模型捕获了支付协议的并发性和错误语义。随后，我们定义了几个安全属性，这些属性捕获了协议正确的中间操作，确保结果对通道双方始终是确定的，并利用它们重新发现了一个先前文献中报道过的已知攻击，以及一个我们称之为“支付竞速”的新型攻击。支付竞速由一系列特定事件组成，可能导致协议出现歧义，使无辜用户无意中损失资金。我们通过在本地测试环境中重现该攻击，证实了其实际可行性。