区块链 > 技术 > 正文

形式化验证 Gasper 共识机制的终局性

区块链数字货币板块文章「形式化验证 Gasper 共识机制的终局性」,本文约有912个文字,大小约为4KB,预计阅读时间3分钟请您欣赏。樱花区块链门户资讯网荟萃众多优秀文章精选,如果想要浏览更多相关区块链数字货币,可以关注本文结尾推荐的优秀文章内容。本站区块链资讯虽然不乏优秀之作,但仅为大家参考使用,希望能对关注区块链的人有所帮助。

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 中的合理化和终局化概念。

形式化验证 Gasper 共识机制的终局性
「新三板」

罚没条件(Slashing Conditions)

如果验证者尝试偏离协议要求、提交自相矛盾的投票,则该验证者会被惩罚:其保证金会被扣除一大部分。Gasper 定义了两个条件(也称罚没条件)来定义何谓自相矛盾的投票:

1.双重投票(Double-voting):验证者发布了两个截然不同的投票,但两个投票的目标高度是同一个高度。


2.环绕投票(Surround-voting):验证者发布的一个投票所关联的两个检查点恰好在自己所发布的另一个投票的两个检查点高度范围内。


形式化验证 Gasper 共识机制的终局性
「新三板」

以上便是樱花区块链给大家分享的关于「形式化验证 Gasper 共识机制的终局性」http://www.0797jjw.cn/qkljs/jishu_26720.html的相关信息了,希望能帮助到大家,更多区块链相关内容,敬请关注樱花区块链!

猜你喜欢

全球稳定币与金融稳定

郑重声明:本文版权归原作者所有,转载文章仅为传播更多信息之目的,如作者信息标记有误,请第一时间联系我们修改或删除,多谢。

原文地址: