[完整版]Runtime Verification正式地验证了Algorand区块链永远不会分叉
在Algorand，团队是高度重视安全性的，并采取一切可能的措施，以确保我们的区块链系统是安全的。这包括广泛的测试、代码评审和代码的开源，从而使每个人都可以自己独立地检查它。
由于代码的安全性取决于它所实现的协议，所以我们对Algorand协议的正确性进行了仔细的分析和推理。但是我们也知道，分布式系统的协议是出了名的难，这种难度尤其是在不安全的系统上运行的协议，允许任何人在不需要任何权威机构许可的情况下参与。
为了对Algorand和协议实现更大的保证，并使未来的设计和验证新协议更容易，我们选择了用机器可检查的形式验证方法来增强paper上的数学证明。为此，我们采用了运行时验证Runtime Verification，https://runtimeverification.com/ 一家具有深入的验证专业知识的公司，来验证Algorand协议的正确性。我们很高兴地报告这一工作中的一个重要里程碑:使用Coq定理验证器，团队开发了该协议的精确数学模型，并正式验证了其安全性保证(区块链从不分叉)。他们已经写了一篇博客文章来描述这项工作，并提供了到包含模型和证明的存储库的链接。
我们要感谢Grigore Rosu、Musab A. Alturki、Brandon Moore、Karl Palmskog和Lucas Pena的巨大努力和成就。接下来就进入正式的验证内容：
正式验证 Algorand: Reinforcing a Chain of Steel
(建模与安全性)
英文原作者： Musab Alturki
Musab A. Alturki, Brandon Moore, Karl Palmskog 以及 Lucas Pena
今年早些时候，Algorand参与了Runtime验证，以验证其共识协议。我们很高兴地报告，第一部分工作，即对协议进行建模并证明其安全性定理，已经成功完成。具体地说，我们使用了一个证明助手(proof assistant, Coq)系统地识别假设，在这些假设下，协议在数学理论上保证不会分叉。https://coq.inria.fr/
在我们开始对内容进行简要总结之前，让我们先简要介绍一下Algorand。Algorand是由麻省理工学院教授、图灵奖得主Silvio Micali创立，是区块链领域最强大的团队之一。Algorand协议的核心是Algorand consensus协议，这是一个pure Proof-of-Stake ，承诺提供高效、安全和可扩展性的性能，同时保持真正的去中心化。Pure-PoS的基本思想是使系统的安全性只依赖于诚实用户所持有的全部股份的绝大部分，而不必依赖于任何特定的小子集节点，也不必锁定资产并惩罚用户。Algorand的共识协议的三个重点是可扩展性、去中心化性和安全性。读者对Algorand的内部结构感兴趣，可以阅读Algorand团队在Medium、微信官方号以及其他社交媒体上发表的内容丰富的文章。
Engagement Summary
在这里，我们只给出了的High-level的概述。完整的细节可在以下找到：
1. 项目附带的扩展技术报告; https://github.com/runtimeverification/algorand-verification/blob/master/report/report.pdf
2. 项目的Github存储库。https://github.com/runtimeverification/algorand-verification
参与的第一步是建立协议的正式模型，并确定协议设计满足其需求的假设条件。为了达到最高的保证级别，我们选择了演绎验证Deductive Verification，在演绎验证中，系统在表达形式逻辑系统中建模和指定，并以类似于数学家证明定理的方式进行验证。下图描述了系统分析的各种方法，作为所需工作与保证的函数。
Algorand的共识协议模式将进行一些列轮次。每轮，节点验证一个要添加到区块链的块。如果网络是分区的，可能需要多次尝试(称为Periods)来验证一个块。有关更多详细信息，请参见Algorand区块链特性规范和这篇关于Algorand的期刊论文。协议本身包含节点级行为和网络级行为(包括对手的行为)，这意味着必须对相当多的细节进行建模，以便能够表达和验证协议的相关属性。
我们在Coq中开发了Algorand 共识协议的模型，并证明了它的许多属性，然后我们使用这些属性来最终显示异步安全性:没有两个诚实的节点可以证明两个不同的块，即使在网络被分区的情况下(即，消息延迟是任意大的)。模型的核心是全局状态转换关系。这种关系归纳地定义了协议的全局状态如何在一个步骤中转换为另一个状态。
模型中断言发生了某种事件的大多数声明都被指定为Trace的命题，可能满足某些条件。Trace是使用全局转换关系(即，如果状态g(i)是序列中的第i个状态，而g(i+1)是序列中的第(i+1)个状态，则有序对g(i)和g(i+1)属于全局转移关系。通过将path属性指定为trace上的命题，我们可以定义一个通用的属性，而不需要假设一个具体的初始状态(或一组初始状态)。属性所需要的任何条件都可以指定为对正在被考虑的trace状态的约束。
Engagement的一个主要结果是对异步安全定理的严格形式化和证明。定理的描述表明，同一轮的任意两个证书必须是同一块的;也就是说，没有分叉。或者，正式的Coq:
注意前提state_before_round r g0,即trace追溯历史上足够长的时间,还没有用户进入一轮r, is_trace g0 trace,即全球国家的trace在g0开始是一个有效的序列,和每一对连续的状态满足全球过渡关系。定理的证明是由单个的结果构成的，这些结果本身被分解成更小的引理(总共约有170个引理)。
Engagement的第二个主要结果是所需假设的精确说明，并表明这些假设足以使安全特性保持不变。在部署设计的实现以及在实现之上构建的系统时，考虑假设是非常重要的。假设指定为模型参数,如有限的一组节点和一组有限的值用于消息负载,或更复杂的假设(或公理),如假设如何消息延迟是有界和假设的诚实节点上持有的多数stake。
进一步Moving Forward
作为这项工作的一部分，我们开发的模型是通用的，因为它以一种与我们验证的属性正交的方式捕获了Algorand共识协议的动态。这意味着模型可以很容易地用来验证异步安全性之外的系统的其他属性，包括最重要的活跃性(即，即每轮均有一个方块获核证)。事实上，我们预期，许多关于议定书和用于证明安全的较小结果也将构成证明活力的努力的基本组成部分。
在此次合作中，我们很高兴与Algorand公司的以下专家合作: Jing Chen, Nickolai Zeldovich and Victor Luchangco.(陈靖、尼克莱·泽尔多维奇和维克多·卢昌科）。
精选文章更新：
1.[更新]通证经济机制解读
3.Algorand第三方代码审核-Incode We Trust
6.Algorand常见问题Q&A
辅助翻译&讲解公众号
加入Algorand官方群请扫码添加Admin
Algorand官网：
https://www.algorand.com/
Algorand基金会：
https://www.algorand.foundation
Telegram电报群：
https://t.me/algorand
综合白皮书：
https://www.algorand.com/docs/whitepapers/
Medium:
https://medium.com/algorand
Naver Blog:
https://blog.naver.com/algorandmarketing
领英Linkedin:
https://www.linkedin.com/company/algorand/
相关具体的开发者与SDK链接：
GoSDK:
https://github.com/algorand/go-algorand-sdk
JavaScript SDK:
https://github.com/algorand/js-algorand-sdk
测试网申请链接：
https://www.algorand.com/apply-testnet
Github存储库链接：
https://github.com/algorand/js-algorand-sdk
开发者网址：
https://developer.algorand.org/docs/javascript-sdk
联系方式：
https://www.algorand.com/contact