EN
信标链的核心：Gasper 共识机制的形式化验证
我们很高兴宣布，Runtime Verification 和以太坊基金会长久合作中的另一大里程碑圆满成功：建立了一个用于模拟和验证信标链的形式化框架。我们证明了Gasper中终结性的关键正确性，并用这些结果证明了这些性质也适用于Gasper在信标链中的实现的抽象。模型和验证脚本都可以在网上找到。
在这篇文章中，我们将重点放在成就的第一部分，即验证Gasper的属性。那Gasper是什么？如何对其属性进行正式验证？为什么这很重要？
Gasper
信标链协议是一种新的权益证明协议，它是以太坊即将进行的主要升级（以太坊2.0）的核心。在信标链协议中，参与的节点（或者叫 “验证者”）都在系统中存有保证金（stake，形式为 ETH）。验证者通过向网络提交 “见证消息（attestation）” 来证实区块的有效性并为其多种属性投票。信标链协议本身包含了多种工具，以帮助验证者们对区块链的最新状态达成共识。
Gasper 为信标链协议中的终局性工具（finality gadget）提出了一套抽象但准确的描述，还定义了分叉选择规则；终局性工具用于确定哪些区块应被参与者认定为已经确定的、不可更改的，分叉选择规则则用于在链产生分叉时确定哪个分叉是主链。Gasper 中的终局性（finality）一般化了始创于《Casper Friendly Finality Gadget (Casper FFG)》论文中的概念，让 “终局化（finalization）” 获得了更通用的形式。
合理化与终结性（Justification and Finalization）
终结性仅检查点区块（或时期边界块：对应于时期开始的区块）上运行。见证消息中有一部分叫 “合理化投票”，验证者在合理化投票中将一个来源检查点区块（source checkpoint block）和稍后的一个目标检查点区块（target checkpoint block）关联起来，直观地表明发起该见证消息的验证者认为 “我们可以从来源检查点的状态移动到目标检查点的状态”。实际上，一份合理化投票表明了：（1）发起投票的验证者；（2）来源检查点及其合理化高度（justification height）；（3）目标检查点及其合理化高度（justification height）。
当且仅当条件满足：（1）来源检查点 B0 已得到合理化；（2）大多数人（即至少 2/3 的验证者）同样投票给 B0-B1 来源-目标对；则目标检查点 B1 就经由来源检查点 B0 得到了合理化。
当且仅当大多数验证者将 B0 与其 K 代子孙检查点 Bk 关联起来，则 B0 获得 K 阶终局性（k > 0），且 B0 与 Bk 之间的所有检查点都被终局化。注意，创世区块本身被认为既已得到合理化，又有终局性。下图演示了 Gasper 中的合理性和终结化概念。
罚减条件（Slashing Conditions）
如果验证节点试图偏离协议，并向区块提交冲突的投票，则验证节点将受到惩罚，因为其保证金会被扣除一大部分。Gasper定义了两个条件，称为“削减条件”，用于定义相互冲突的投票：
1. 双重投票：验证者发布两个具有相同目标高度的不同投票。
2. 环绕投票：验证者在另一个投票范围内发布投票。
如下图所示。
双重投票的验证节点违反了第一个削减条件，而环绕投票的验证节点违反了第二个削减条件。无论哪种情况，违规验证者都将因违规而削减其保证金。
正确性（Correctness Properties）
与其他拜占庭式容错（BFT）协议一样，Gasper中的一个关键基本假设是，多数（即至少2/3）验证者是诚实的（以保证金数量定义），并且会遵循该协议。在此假设下，Gasper具有两个基本正确性属性：
· 可追责的安全性（Accountable Safety）：不会有两个属于不同分叉的区块都被终局化，除非有至少 1/3 的验证者（以保证金数量计）被罚没；
· 合理的活性（Plausible Liveness）：无论区块链过往发生了什么事，区块的终局化进程永远不会陷入僵局。
此外，在动态验证者集的情况下，活动验证者集可能会随着时间的推移而发生变化，从中有不同的验证者加入或离开网络，第三个属性量化了违规情况下的可消减保证金：
· 可削减界限（Slashable bound）：只要能够使用协议外条件来控制验证者的激活和退出参数条件，就能证明（在打破安全性时）可被罚没的保证金数量有一个下限。
动态验证节点集（由信标链协议实现）引入了另一个具有挑战性的问题：系统不再那么能够可靠地惩罚恶意验证者，因为他们可能会在作恶之后、保证金被实际罚没之前离开网络。而可罚没下限属性使得调整活跃验证者集合的可变幅度、维持最低水平的可追责性成为可能。
Gasper中验证终结性
Gasper旨在提供一种数学上精确的最终描述，可用于正式证明其正确性，这对于证明信标链协议的安全性至关重要。以太坊平台越来越多地被用作大型金融交易系统的基础平台，突显了确保其安全性的日益重要的意义。
我们与以太坊基金会合作，使用Coq证明助手在动态验证程序集的常规设置中规范了Gasper的终结机制。我们在这一条件下指出并证明了 Gasper 的所有三种关键属性：可追责的安全性、似然活性以及可罚没下限；所有证明都使用了同一个 Coq 模型。
该协议的演绎验证为参数的正确性和完整性提供了最大的信心，从而确保没有未陈述的假设或无效的演绎步骤。它明确了论证所需的所有假设。形式化还反馈到协议的描述中，使其更加精确和完整。
这里我们仅对这一成就给出概要的说明。完整的细节可见：
· 该项目的技术报告
· 该项目的 Github 代码库
建模和验证方法（Modeling and Verification Approach）
第一步是建立协议模型，使我们能够表达我们要正式陈述和证明的所有关键属性。该模型建立在我们先前在Casper FFG中验证安全性和活性的工作的基础上，该工作定义了Gasper终结机制的早期版本。
该模型有三个主要的结构构建基块：
验证者和法定人数（Validators and quorums）。验证者被抽象地表示为一个有限型（finite type）的成员（成员数量有限，而且可以枚举），写为 Validator : finType 。每个验证者都有一份保证金；这一事实我们建模成一个未解释的函数 stake : {fmap Validator -> nat}，保存验证者与其保证金数量（一个自然数）的映射。此外，给定一个验证者集合，其权重 wt 定义为该集合中所有验证者保证金数量的总和：
\sum是求和运算符，stake.[st\u fun v]给出与验证节点v相对应的保证金额（st_fun是保证金函数总计的假设-即每个验证者都必须在系统中拥有保证金）。
wt函数的几个属性来自其定义，例如：空的验证器集合的权重一定为零，两个不相交集合的并集的权重就是它们的权重之和。这些属性在涉及可罚没下限属性中关于权重的推理时会派上用场。
此外，由于我们打算对动态验证器集进行建模，其中验证器的有效集合可能会在不同的块之间变化，因此我们声明了一个抽象（finite）映射vset：{fmap Hash-> {set Validator}}，给出一个区块处的活跃验证者集合。现在使用vset和wt，我们可以定义一个集合成为多数集的含义：
在某个区块处，如果活跃验证者集合的一个子集的权重超过整个集合权重的 2/3，则该子集就是一个绝对多数集合。
区块树。我们通过有限类型的散列哈希Hash：finType来对一个区块进行建模，其创世纪代表Genesis区块。我们使用父二进制关系（使用h1 <〜h2表示法）对检查点区块树进行建模，将其公理化表示h1是h2的父级。
然后使用这个定义将祖先二进制关系h1<~*h2定义为<~的自反传递闭包。因此，如果h1<~*h2，那么h1是h2的祖先，h2是h1的后代（h1和h2可能是同一个区块）。关于祖先关系的属性，例如块的祖先的祖先也是该区块的祖先的属性，由此而来的是父关系的自反传递闭包。
全局状态：状态由一组有限的合理投票来表示，这些投票的形式为（v，s，t，s_h，t_h），其中v是投票验证节点，s和t是该投票用于的源区块和目标区块 ，而s_h和t_h是它们的证明高度。布尔成员谓词可以决定是否进行投票：
示例规范
基于这些定义及其属性，我们定义了模型中的所有其他结构和属性，包括削减条件，仲裁交集属性以及对正和最终确定。还有合理化以及终局化。例如使用抽象成员资格约束来定义由于违反而减少仲裁的属性，如下所示：
一个命题，指出减少定额意味着相对于某些区块bL和bR分别存在两个绝对多数定额vL和vR，这些区块的交点完全由减数的验证者（具有双重投票权或环绕投票的确认者）组成。注意，在活跃验证者集合一直固定的特殊条件下，这些绝对多数集合的交集的权重至少是所有保证金的 1/3。
另一个例子是终结分叉的定义（违反安全）：
这个命题指出两个相互冲突的区块b1和b2（即两个区块都不是另一个区块的祖先）都是最终确定的。这两个区块可以是在任意合理化高度的时候被任意长的链终局化的。
这些定义和结果组中被用来指出和证明可追责的安全性、合理活性以及可消减界限三种定理。为清楚起见，我们还用下式重新定义了可追责安全性定理的表述：
这个定义很简单，只是说：如果安全性被打破（出现了任何被敲定的分叉），那必定意味着某个验证者集合会被罚没。这个证明机械化了 Gasper 给出的非正式论证，并展示了为什么分叉获得终局化就意味一定有两个绝对多数团体违反了其中一条罚没条件，因此其交集可被罚没。
我们的技术报告描述了形式化过程以及这些属性的证明，而我们的项目代码库提供了完整的详述。
进一步说明
在这篇文章中，我们描述了在当前参与阶段，与以太坊基金会合作在Runtime Verification中完成的第一部分。第一部分是关于形式化Gasper并证明它的三个关键属性：可追责的安全性，合理的活性和可消减的界限，假设动态验证节点集。在本文中未讨论的成就的第二部分是展示这些结果如何延续到更细粒度的模型（用K框架编写）中，该模型给出了信标链转换函数的抽象。稍后，我们后面会用另一篇文章来展示这一成果。
这个里程碑的完成标志着朝着实现这项合作的最终目标迈出的重要一步，这是正式证明信标链协议满足所有三个关键特性，并在抽象级别上明确陈述了所需的所有假设，即 非常接近协议的规范。
我们期待在此工作上继续与以太坊基金会合作。对于这次参与，我们非常高兴与以太坊基金会的以下专家合作：Danny Ryan，Carl Beekhuizen，Martin Lundfall，Yan Zhang和Aditya Asgaonkar。
