▼更多精彩推荐,请关注我们▼

PlatON 共识协议安全性与稳定性已通过 Runtime 学术级验证

作为分布式系统,区块链由多个节点共同支持运转,尤其是在非许可式的公链中,节点的加入和退出都是自由和开放的,所以节点的「品质」可能千差万别。而节点与节点之间需要通过网络来发送消息进行通信,根据他们所遵循的协议在某个任务消息达成共识并一致执行,以此来保障区块链网络的正常运转。

在这个过程中会出现两种类型的错误:一种是节点崩溃、网络故障、丢包等,因为节点的硬件性能或者运转环境不能得到保障而导致错误情况的出现,另外一种是节点可能是有恶意的、不遵守协议规则的。例如故意延迟或拒绝网络中的消息、提出无效块,或者向不同的对等体发送不同的消息。在最坏的情况下,恶意节点可能会相互协作。

作为一个非许可式的区块链网络,是无法以挑选「合格」的节点的方式来杜绝以上错误发生的,那么这就要求这个区块链系统能够通过共识协议的严密设计和稳定运行,在千变万化的复杂运行环境下,依旧能够保障网络安全稳定地持续运行。

PlatON 一直将 Giskard 共识协议视为网络的基础核心组件来予以高度重视,除了周密设计和高强度测试之外,还邀请全球知名的形式化验证团队 Runtime Verification,以学术研究的规格对该协议进行了形式化验证。在进程中,PlatON 和 Runtime Verification 双方都秉持高效、严谨、极细颗粒度的状态与要求,针对 Giskard 共识进行「高压」验证。 验证结果已经以名为《Verifying Safety of the Giskard Consensus Protocol in Coq》的报告形式发表,并在 Github 上开源。

从验证结果来看,Runtime Verification 通过形式化验证获得的机器验证证据有力地证明了: 即使存在不良节点,Giskard 共识协议的关键安全属性也可以为 PlatON 整个协议的执行保驾护航。 本次项目合作的验证结果为 Giskard 共识协议作为 PlatON 网络基础设施核心组件的可靠性提供了重要证据,并清晰阐述了 Giskard 共识的基础假设。

Runtime Verification CEO、伊利诺伊大学厄巴纳-香槟分校计算机科学教授格里高利·罗素表示:“我们很荣幸与 PlatON 团队合作,通过 COQ 对 Giskard 协议进行建模和多个方面的形式化验证。如今我们对该协议的稳定运行和实现充满信心,同时也证明该协议的安全性已达到期望标准。我们在与 PlatON 团队紧密的沟通下,采用了目前最严谨的形式化验证方法,充分证明了该协议拥有极高的安全性能。而我们建立的验证模型也为未来该协议的实现和变动提供了可靠严谨的参考。非常期待与 PlatON 深化合作,共建技术生态。”

但对于技术进展的追求是永远没有止境的,而且我们一直都深信最强大的智慧一定蕴涵于更为浩瀚广博的社区当中,所以我们在此诚挚地邀请广大社区成员,一起来研究 Runtime Verification 给出的形式化验证报告,深入钻研 Giskard 协议的方方面面,共同将其运转的安全性和稳定性不断推向新的水平。

验证结果报告网址:

https://github.com/runtimeverification/giskard-verification/blob/master/report/report.pdf

欢迎社区成员就验证报告的内容和结果,在论坛展开充分讨论和交流。

### ----关于 Runtime Verification----

Runtime Verification 是一家位于美国伊利诺伊州厄巴纳的科技公司,使用执行期验证技术对公链虚拟机和智能合约进行安全性审计,通过使用自己研发的动态分析验证技术致力于提高区块链领域软件系统的安全性、可靠性和正确性。目前 Runtime Verification 的客户包括 PlatON、 IOHK(Cardano 的开发公司)、以太坊、Algorand、Web3 基金会、Elrond、Casper Labs、Gnosis、MakerDAO 等。

目前区块链安全审计领域多为静态分析(只对源代码内部逻辑进行审计),而动态分析(使用代码编译后执行时产生的数据进行审计)能够涵盖的安全漏洞比静态分析更为广泛。Runtime Verification 拥有世界顶尖的形式化验证团队,能够对编译后的二进制代码直接进行验证。相比对源代码进行形式化验证,可以发现由于编译器的问题而发生的一些很难找到的 bug。

----关于 PlatON----

PlatON 是由万向肖风博士作为创始人发起、致力于成为全球新一代隐私计算和分布式经济体基础设施,也是全球隐私计算领域的开创者与领导者。长期专注于可扩展性和隐私保护的高性能分布式计算网络,通过以可验证计算、安全多方计算、零知识证明、同态加密等密码学算法共同组装的下一代计算架构,为全球人工智能、分布式应用开发者、数据提供方及存有计算需求的各类社区、机构、个人,提供开源架构下的公共基础设施。其元网络 Alaya 于 2020 年 10 月 24 日正式上线。

👇👇👇

在 PlatON 微信公众号后台回复「入群」并加 PlatON 小助手微信,即可加入 PlatON 社群,获得一手活动信息及最新项目进展。

PlatON 共识协议安全性与稳定性已通过 Runtime 学术级验证

了解 PlatON 更多动态

PlatON·GitHub

https://github.com/PlatONnetwork

PlatON·Forum

https://forum.latticex.foundation/c/PlatON-CN

PlatON·Telegram

https://t.me/PlatONNetworkCN

PlatON·Twitter

https://twitter.com/PlatON_Network

PlatON·LinkedIn

https://linkedin.com/company/platonnetwork

PlatON 共识协议安全性与稳定性已通过 Runtime 学术级验证

PlatON 共识协议安全性与稳定性已通过 Runtime 学术级验证

PlatON 共识协议安全性与稳定性已通过 Runtime 学术级验证

阅读原文,访问 PlatON 网站!