Gasper是一个抽象的权利证明协议层，它由信标链协议实现，信标链协议是即将到来的以太网2.0网络的底层协议。Gasper的一个关键组成部分是终结机制，它可以确保事务的持久性和系统在受到攻击时的持续运行。

我们很高兴地宣布运行时验证和以太网基金会之间长期合作的另一个里程碑的成功：建立一个模拟和验证信标链的正式框架。我们证明了Gasper中终止的关键正确性，并利用这些结果证明了这些性质也适用于Gasper在信标链中实现的抽象。模型和验证脚本都可以在网上找到。

在本文中，我们将重点关注成果的第一部分，即验证Gasper的属性。加斯伯是什么？如何正式验证其属性？为什么这很重要？

廉价香烟

信标链协议是一种新的权利证明协议，是以太网2.0的核心。在信标链协议中，所有参与节点(或“验证者”)在系统中都有存款(以ETH的形式)。验证者验证块的有效性，并通过向网络提交“证明”来对其多个属性进行投票。信标链协议本身包含各种工具，帮助验证者就区块链的最新状态达成共识。

Gasper对信标链协议中的终结小工具提出了一套抽象但准确的描述，并定义了分叉选择规则。终结性工具用于确定哪些块应该被参与者确认和不可改变，分叉选择规则用于确定当链产生分叉时哪个分叉是主链。最后定稿Gasper概括了起源于《Casper Friendly Finality Gadget (Casper FFG)》论文的概念，并使“最终性”获得了更一般的形式。

合理化和定稿(理由和定稿)

终结仅在检查点块(或周期边界块：对应于周期开始的块)上运行。见证消息的一部分被称为“理性投票”，验证者在理性投票中将源检查点块与后面的目标检查点块相关联，这直观地表明发起见证消息的验证者认为“我们可以从源检查点的状态移动到目标检查点的状态。”事实上，合理的投票表明：(1)发起投票的验证者；(2)源检查点及其对正高度；(3)目标检查点及其对正高度。

当且仅当满足以下条件：(1)源检查点B0已被合理化；(2)大多数人(即至少三分之二的验证者)也投票支持B0-B1源-目标对；然后目标检查点B1通过源检查点B0合理化。

当且仅当大多数验证器将B0与其K代后代检查点Bk相关联时，B0获得K阶终结性(k 0)，并且B0和Bk之间的所有检查点被终结。请注意，创新板块本身被认为是理性的和最终的。下图展示了Gasper中的合理性和终止概念。

惩罚条件(斜线条件)

如果验证节点试图偏离协议并向块提交冲突的投票，验证节点将受到惩罚，因为它的大部分余量将被扣除。Gasper定义了两个条件，称为“切割条件”，用于定义冲突投票：

1.双重投票：验证者以相同的目标高度发出两个不同的投票。

2.轮投票：验证者在另一个投票范围内投票。

如下图所示。

双重投票的验证节点违反第一个约简条件，而圆形投票的验证节点违反第二个约简条件。在这两种情况下，违规者都将削减自己的违规保证金。

准确性属性(正确性属性)

像其他拜占庭容错(BFT)协议一样，Gasper中的一个关键基本假设是，大多数(即至少2/3)验证者是诚实的(由裕量定义)，并且将遵循该协议。在这个假设下，Gasper有两个基本的正确性属性：

可问责的安全性：除非至少三分之一的验证者(就保证金金额而言)被没收，否则属于不同分支的两个区块不会被最终确定；

合理的活跃度：不管区块链过去发生了什么，该区块的最终确定过程永远不会陷入僵局。

此外，在动态验证者集的情况下，活动验证者集可以随着时间而改变，不同的验证者从该验证者集加入或离开网络。第三个属性量化了违规情况下的可还原边距：

可削减的界限：只要协议之外的条件可以用来控制验证者的激活和退出参数，就可以证明可以没收的证券数量有一个下限(当证券被破坏时)。

节点集的动态验证(通过信标链协议实现)引入了另一个具有挑战性的问题：系统不再能够可靠地惩罚恶意验证者，因为他们可能在犯罪之后并且在保证金被实际没收之前离开网络。惩罚下限的属性使得可以调整主动验证者集的可变范围并保持最低的责任。

在Gasper中验证终结性

Gasper旨在提供一个数学上精确的最终描述，可以用来正式证明其正确性，这对于证明信标链协议的安全性非常重要。以太网平台越来越多地被用作大型金融交易系统的基础平台，这凸显了保证其安全性的日益重要的意义。

我们与以太网基金会合作，通过使用Coq认证助手，在动态验证组件的一般设置中标准化Gasper的终止机制。在此条件下，我们指出并证明了Gasper的三个关键属性：责任安全性、可能性活动和惩罚下限；所有的证明都使用相同的Coq模型。

协议的演绎验证为参数的正确性和完整性提供了最大的可信度，从而确保不存在未声明的假设或无效的演绎步骤。它澄清了争论所需的所有假设。形式化也被反馈到协议的描述中，以使其更加准确和完整。

这里我们只对这一成就做一个简单的描述。可以看到完整的细节：

项目技术报告

项目的Github代码库

建模和验证方法(建模和验证方法)

第一步是建立一个协议模型，这样我们就可以表达我们想要正式陈述和证明的所有关键属性。该模型基于我们之前在卡斯珀FFG验证安全性和活动的工作，它定义了早期版本的加斯伯终止机制。

该模型有三个主要的结构构件：

验证者和法定人数(验证者和法定人数)。验证器被抽象地表示为一个有限类型的成员(成员的数量是有限的并且可以被枚举)，并且被写成验证器： finType。每个验证者都有押金；这一事实被建模为一个无法解释的函数，stack : { fmap Validator-NAT }，它存储验证器与其存款金额(一个自然数)之间的映射。此外，给定一个验证者集合，其权重wt被定义为该集合中所有验证者余量的总和：

\sum是sum运算符，而stake。[st\u fun v]给出对应于验证节点v的保证量(假设st_fun是裕量函数的和，即每个验证者在系统中必须有裕量)。

权函数的几个属性来自于它的定义。例如，空验证器集的权重必须为零，并且两个不相交集的并集的权重是它们的权重之和。当涉及到对惩罚下限属性中的权重进行推理时，这些属性就派上了用场。

此外，因为我们打算对动态验证器集进行建模，其中有效的验证器集可能在不同的块之间变化，所以我们声明了一个抽象映射vset: {fmap hash-{set validator}}，它在一个块上给出了一个活动的验证器集。现在使用vset和wt，我们可以定义集合成为多数集合的含义：

在某个块，如果活动验证集的子集的权重超过整个集的权重的2/3，则该子集是绝对多数集。

积木树。我们通过一个有限类型的散列来模拟一个块：fin类型，它的genesis代表Genesis块。我们使用父二元关系(h1h2符号)来建模检查点块树，并将其公理化以表明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，证明其三个关键属性：责任安全性、合理活动和可约边界，并假设节点集的动态验证。本文未讨论的成果的第二部分是展示如何将这些结果扩展到更细粒度的模型(用K框架编写)，该模型给出了信标链转换函数的抽象。稍后，我们将使用另一篇文章来展示这一成就。

这一里程碑的完成标志着实现这一合作最终目标的重要一步。它是信标链协议满足所有三个关键特征的正式证明，并且在抽象层次上清楚地陈述了所有必需的假设，也就是说，它非常接近协议的规范。

我们期待着在这项工作中继续与埃瑟伦基金会合作。我们很高兴能与以太博物馆基金会的下列专家合作：丹尼瑞恩、卡尔比凯岑、马丁伦德福尔、严章和阿迪雅阿斯高恩卡。