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

转载
249 天前
13126
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)中的错误而已。” 利托斯表示。利托斯提到,未来的形式化分析可能最终被用于研实际的代码。“理想情况下,通过对代码进行形式化验证来证明其符合规范,会在系统中提升信任程度。但在那之前,我们仍然需要一个机器可读的规范版本。” 他表示。

杨瑶瑶

4863篇

文章总数

49436546

浏览数

新闻排行

OKEx期权课堂【期权与现货/杠杆有啥不一样?】

随着您交易现货和杠杆现货,以及您现在接触的期权这种衍生品,您一定会问这些有什么不一样的地方。

OKEX永续合约的资金费

OKEx永续合约的资金费率是什么意思?为什么有正有负?是平台收取的吗?

揭秘Filecoin二测矿商刷榜套路(内附避坑指南)

“看排名买矿机,先了解下套路”

火讯财经助力国内首个区块链人才库“鸾翔计划”发布

来自国家部委、知名企业、学术机构、主流协会等不同领域的重磅嘉宾出席了此次发布会,通过视频直播连线方式,就区块链人才、新基建等诸多话题进行了精彩讨论。

ChainsMap周报:链上数据全面下降,三大所比特币去向揭秘

在比特币减半之后的一周,链上数据并未出现剧烈变化,但是相关核心数据整体呈现普降的态势。

未来矿场百城巡演——昆山疯牛社区站

社区工作室坐落于昆山万达广场,5月22日于昆城一品举办百人客户答谢会暨昆山疯牛社区开业仪式,本次开业仪式由未来矿场领袖、创世团队共同见证。

严明辉:未来要投资区块链不止是投趋势,更是个技术活儿;

这个是个从“事情”到“势能”转化的一个过程;但我们同时也看到很多创新能力和运营能力比较强的精作类项目,目前我们也有跟进好看好,但这类项目的甄别还需要一定的方法......