Runtime：Giskard共识协议以极高的安全性与稳定性为PlatON保驾护航

近日，Runtime Verification宣布与PlatON Network合作的Giskard共识协议验证项目圆满完成。本次合作旨在通过COQ证明助手验证手段，验证PlatON的Giskard共识协议安全性。据Runtime Verification发布的技术报告显示，Giskard共识协议在验证过程中展现了极高的安全性与稳定性，为PlatON系统良好运行奠定了有力基础。

据Runtime Verification相关负责人表示，在项目进程中，双方秉持高效、严谨、极细颗粒度的状态与要求，针对Giskard共识进行「高压」验证， Giskard共识是PlatON实现全球隐私计算网络与分布式经济体基础设施的基础与核心，是PlatON区块链生态分布式网络基础设施的中心，应用于验证PlatON网络中进行的交易与运算。

由于分布式系统中情况复杂多变且网络节点存在不良可能性，仅通过单一测试手段来保证共识协议安全性的传统方式已不能满足当下需求。Runtime Verification通过在COQ中建立Giskard的模型，以此演示该协议多条关键安全属性的编码与形式化验证。

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

本次合作意义非常，不仅验证了PlatON作为隐私计算网络与分布式经济体基础设施核心部件的可靠性（该部件很难通过单一的测试和其他类似的方法进行分析）同时，使Runtime Verification能够对Giskard共识协议的技术参数和设想进行阐述。更新后的技术参数为Giskard共识协议以后的实现和验证提供了说明指导，双方对本次合作都给予了很高的评价。

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

针对本次合作，PlatON首席技术官曲俊杰表示：“很荣幸能与Runtime Verification的工程师和科研人员合作，期间的沟通也十分愉快。Runtime Verification团队攻克多个并行复杂问题和边缘案例的能力给我们留下了深刻印象。我很高兴Runtime Verification能成为PlatON的合作伙伴并携手同行。此后，我们在协议建模和智能合约的形式化验证等领域会持续保持深入合作。”

关于Runtime Verification

Runtime Verification是一家位于美国伊利诺伊州厄巴纳的科技公司，专注为区块链领域提供软件测试和验证方面的服务与产品。

关于PlatON

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