信标链协议|技术贴 | 形式化验证Gasper共识机制的终局性（finalization）机制|技术|验证|

文章图片
免责声明：本文旨在传递更多市场信息，不构成任何投资建议。文章仅代表作者观点，不代表火星财经官方立场。
小编：记得关注哦
来源：以太坊爱好者

文章图片
Gasper 是一个由信标链协议（即将到来的以太坊 2.0网络的底层协议）实现的抽象的权益证明协议层。Gasper 的关键部分就是一套终局性机制（finality mechanism），用于保证交易的持存性（durability）和系统的不间断运作不会被攻击破坏。
我们很高兴宣布，Runtime Verification和以太坊基金会长久合作中的另一大里程碑圆满成功：我们开发了一套形式框架来模拟和验证信标链协议，并成功形式化地证明了 Gasper 终局性的正确性（correctness）；并且，我们还使用这些结果证明了信标链的 Gasper 抽象实现同样具备这些属性。模型和证明脚本都可以在此处找到。
在本文中，我们希望介绍这一成就的第一部分：验证 Gasper 的属性。所以，什么是 Gasper？如何能形式化地验证其属性？这种形式化验证有何意义？
Gasper
信标链协议是一套新的权益证明协议，是以太坊未来的重大升级 “以太坊 2.0” 的核心。在信标链协议中，参与的节点（或者叫 “验证者”）都在系统中存有保证金（stake，形式为 ETH）。验证者通过向网络提交 “见证消息（attestation）” 来证实区块的有效性并为其多种属性投票。信标链协议本身包含了多种工具，以帮助验证者们对区块链的最新状态达成共识。
Gasper为信标链协议中的终局性工具（finality gadget）提出了一套抽象但准确的描述，还定义了分叉选择规则；终局性工具用于确定哪些区块应被参与者认定为已经确定的、不可更改的，分叉选择规则则用于在链产生分叉时确定哪个分叉是主链。Gasper 中的终局性（finality）一般化了始创于《Casper Friendly Finality Gadget (Casper FFG)》论文中的概念，让 “终局化（finalization）” 获得了更通用的形式。
合理化与终局化（Justification and Finalization）终局性概念仅与 “检查点区块”（也叫 “时段边界区块”，就是位于时段（epoch）起点处的区块）有关。见证消息中有一部分叫 “合理化投票”，验证者在合理化投票中将一个来源检查点区块（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 定义了两个条件（也称罚没条件）来定义何谓自相矛盾的投票：

双重投票（Double-voting）：验证者发布了两个截然不同的投票，但两个投票的目标高度是同一个高度。
环绕投票（Surround-voting）：验证者发布的一个投票所关联的两个检查点恰好在自己所发布的另一个投票的两个检查点高度范围内。

信标链协议|技术贴 | 形式化验证Gasper共识机制的终局性（finalization）

文章图片
发起双重投票的验证者被认为违反了第一罚没条件；而发起环绕投票的验证者则违反了第二罚没条件。不论是哪种情况，违反规则的验证者都会被扣除大量保证金。
正确性（Correctness Properties）与其它拜占庭容错型（Byzantine Fault Tolerance，BFT）协议相同，Gasper 协议的一个关键底层假设是绝大多数验证者（超过 2/3，以保证金数量定义）是诚实的、会遵循协议的要求。在此假设下，Gasper 有两大基本属性：