闪电网络通过首次形式化验证:在数学上和比特币一样安全

转载
25 天前
12886
Coindesk中文站

来源:Coindesk中文站    翻译:王井泰


闪电网络的概念富有创新和实验性,不过可能导致用户资金损失的 bug 仍有待发现。近日,一队科研人员发布了对比特币闪电网络的形式化验证结果。

这篇论文在由爱丁堡大学的安格洛斯·齐亚伊亚斯(Aggelos Kiayias)和奥弗依斯·利托斯(Orfeas Litos)发表。齐亚伊亚斯还是区块链公司 IOHK 的首席科学家,这家公司为新生支付网络的底层安全做出了许多贡献。

迄今为止,闪电网络尚未在数学上进行过正式的安全测试,这一测试可以建立一个计算机系统在数学上的安全程度。这篇题为 “A Composable Security Treatment of the Lightning Network” 的论文认为,如今闪电网络已经被用于保护至少 8500 万美元的真实资金,但其代码规范缺乏形式化验证是一件 “极其严重的事”。

“因此,我们的措施详细地描述了如何基于底层账本上资产实现协议安全保证。” 论文解释道。

他们所做的这个过程被称作 “形式化验证(formal security)”。这一方法在加密货币领域非常流行,而且有助于确定代码的安全性。形式化安全并没有被部署在每个加密项目上,因为部署 “形式化验证” 需要高深的知识,部署成本很高。

01
坚实的规范

研究者结果是积极的,这表明为使支付系统正常工作而堆积在一起的底层加密技术是正确的。“系统所有的重要安全部分都是可靠的,这是意料之中的结果。” 利托斯告诉 CoinDsek。这究竟意味着什么?利托斯和齐亚伊亚斯审查了闪电网络的规范,每一款闪电网络软件都必须满足这些规则,以向网络的其他部分发起支付。

利托斯告诉 CoinDesk:“主要的结论是闪电网络和比特币一样安全。”为了得出这一结论,他们研究了构成闪电网络的密码学。密码学是由数学算法组成的,这些算法提供了网络上的安全和隐私基础。在闪电网络中,密码学是把支付系统黏在一起的胶水,最后的结果是允许一个人把比特币转账给其他人。因此,研究者们研究了闪电网络底层不同的密码学技术,包括数字签名。这一技术对于比特币而言,意味着比特币只能被有着正确私钥的用户产出。

“闪电网络用户只可能在用于比特币的数字签名和哈希函数出错时才可能会丢失资金。”利托斯说,“使用底层的真实账户允许我们精准定位闪电网络运行参数间的安全联系。特别的,我们对 ‘闪电网络用户需要多久检查一次区块链,尤其是进行连续多次交易时’ 这个问题给出了确切的答案。” 


02
规格并非软件

虽然形式化验证是重要的一步,但它只存在于闪电网络的蓝图上,尚未由开发者落实在任何一款软件上。虽然论文声称闪电网络 “和比特币一样安全”,这不意味着软件本身也是安全的。这也许听起来是微不足道的区别,但实际上区别极大。

有 3 款主要闪电网络执行了专家们的意见,分别是 Acinq’s Eclair、Blockstream’s c-lightning 和 Lightning Lab’s lnd。“我们的分析基于形式化验证,而不是实际执行。因此,并不能排除各种实现中的错误,目前仅仅是排除了规范(specification)中的错误而已。” 利托斯表示。利托斯提到,未来的形式化分析可能最终被用于研实际的代码。“理想情况下,通过对代码进行形式化验证来证明其符合规范,会在系统中提升信任程度。但在那之前,我们仍然需要一个机器可读的规范版本。” 他表示。

杨瑶瑶

3174篇

文章总数

37269027

浏览数

新闻排行

为什么美国证券交易委员会再次拒绝了比特币ETF?原因在这里

比特币市场还不够成熟,目前无法支持交易所交易基金(ETF)

英国​数字证券交易所Archax与R3达成合作,以降低交易后摩擦

“目前传统金融市场的交易后流程效率极低,还涉及许多中介机构。这种合作关系,将消除摩擦,精简活动,从而提高效率和降低成本”。

P网“自立”,幕后推手是孙宇晨?

美国当地时间10月18日,加密货币交易所Poloniex(P网)官方宣布,它将从Circle独立出来成为一家新的国际公司Polo Digital Assets,并计划投资超过1亿美元来开发、扩展新的交易平台。

区块链的落地之路

“落地的过程其实就是合规的过程,什么叫做合规?合规就是在规则之内游戏。”

美元的Libra,美元的未来

一时间Libra头顶乌云密布,Libra还有未来么?这么多纷繁芜杂的声音,到底哪个信息才是可信的?

国家互联网信息办公室关于发布第二批境内区块链信息服务备案编号的公告

备案仅是对主体区块链信息服务相关情况的登记,不代表对其机构、产品和服务的认可,任何机构和个人不得用于任何商业目的。

在看不见的协议中寻找未来的加密货币独角兽

当我们谈论「需求主导的周期」时,其实应该最先关注开发者。因为需求首先来自于他们,然后才是终端用户。