信标链K中的形式模型：以太坊2.0的主要权益证明区块链

随着即将到来的2.0版重大更新（代号为Serenity），以太坊正在过渡到分片的权益证明（PoS）共识机制。它带来了更好的能效，安全性和可扩展性。以太坊2.0的特定PoS协议称为信标链。
我们很高兴地报告Runtime Verification与以太坊基金会之间正在进行的合作中的第一个里程碑，以构建一个用于建模和验证信标链的正式框架。在K框架下完成了信标链的可执行形式化模型K规范和描述这项工作的技术报告都可以在线获得。
那么什么是信标链？K中的模型是如何开发的？为什么这一发展很重要？
Nutshell中的信标链
信标链是即将到来的以太坊2.0的PoS协议层。协议主要负责在参与协议的网络中所有节点之间就系统状态达成共识。
参与节点（在协议中称为验证者）主要根据节点的当前状态，通过提议新的信标区块或对现有的信标区块进行投票来为系统的分布式操作做出贡献。信标区块主要封装了发布到网络的一组投票。该协议管理如何选择验证者来提议和投票给区块，以确保每个验证者都有公平的贡献机会。
投票给一个信标区块叫做证明。证明是共识机制的基本组成部分。通过信标区块的证明：
· 验证者证明该区块是有效的，并且应将其附加到链中；
· 如果链分叉成多个分支（根据分叉选择规则），则验证者通过标识区块应附加到的位置来投票给“规范的块链”；
· 验证者有助于确定区块的确定性，这一过程告诉我们何时可以将信标区块视为最终的，因此不应还原（根据Casper FFG）；

· 如果该区块不属于主链，则验证者将对该区块的分片投票。直观上，分片是链接到信标链的独立链，可以通过系统中的验证者子集与状态中的其他分片并行处理，从而显着提高了系统一次处理更多交易的能力，从而提高了它的可扩展性（请参阅sharding和crosslinks）。

最后，遵循协议并做出明智决策的验证者将获得以太坊奖励，以红利形式分配，以鼓励适当的行为。另一方面，偏离协议或行为不正常的验证者可能会因拒绝或在某些情况下因削减其抵押的以太币而受到处罚。这种奖励惩罚系统有助于使恶意用户在经济上不可行，无法在该系统上发起成功的攻击（请参阅《 Serenity设计原理》注释）。
信标链当前由以太坊基金会开发的Python“以太坊2.0阶段0 –信标链”的参考实现定义。
定义协议操作的实现的主要组件是信标链状态转换函数state_transition。该函数实现的相关部分的摘录如下所示：

处理从创始状态（已处理的创始信标区块的状态）开始。给定要处理的下一个信标区块，并假定该区块有效，信标链状态转换功能将给定的信标链状态（前状态）转换为新状态（后状态）。此后状态反映了以下结果：
· 考虑（可能）丢失的区块； （process_slots）;
· 处理区块的内容（process_block）。
在K中建模信标链
我们在这项工作中的目标是建立一个信标链的形式模型，该模型尽可能与“以太坊2.0阶段0规范”给出的参考实现相对应，从而实现以下功能：
· 模拟或设置信标链状态转换函数的执行。
· 从信标链测试套件运行现有测试。
· 分析现有测试套件的代码覆盖率，并通过新测试进行改进。
K是实现此目标的非常合适的框架，因为它能够开发信标链的形式模型，其特征是：
1. 可通过K工具中的模式重写来执行，因此可以直接从规范中获取信标链状态转换函数的解释器（无需任何额外费用）。
2. 具体而言，其规范直接对应于系统的Python实现（对某些特定的抽象进行模化，例如签名验证）。
K模型也为更复杂的验证任务（例如可达性分析和演绎验证）奠定了基础，但这是正在进行的工作和将来的工作的一部分，将在其他地方进行介绍。
该项目的github存储库中提供了k中模型的完整规范，以及一份更详细地描述这项工作的技术报告。https://github.com/runtimeverification/beacon-chain-spec
信标链是如何用k建模的？
通常信标链在K中建模为状态转换系统，其状态为信标链状态，其转换由主信标链状态转换函数定义。
在K中，信标链状态被指定为由（可能嵌套的）单元组成的配置，其中每个单元代表定义协议所需的配置的语义元素。 例如下面的摘录显示了<beacon-chain />配置的两个单元：<k />单元是用于保存要执行的程序（计算）的一个特殊的单元，而<state />单元是包含信标链状态的所有结构元素（下面仅显示三个，三个点表示省略的单元格）：

信标链状态转换功能由K中的运算符指定，该函数将由当前信标链配置建模的信标链前状态转换为由结果K配置建模的信标链后状态。 运算符声明如下：

如上所述，涉及两个主要的连续步骤：process_slots和process_block。命令在k中的排序自然指定为使用运算符~>，将计算叠加在一个连续项上。例如使用以下k规则定义状态转换函数：

只有当process_slots成功终止时，才会进行由process_block定义的下一次计算，该计算将捕获预期的语义。
在开发转换函数的语义规范时，我们面临的挑战之一是python语义丰富的表达式和大多数命令式编程风格与k语言定义的构造和声明式规范风格之间的不匹配。在这一发展过程中，我们已经确定了一些模式以及如何在k中优雅地指定它们，例如如上所述的用于排序的堆叠计算结构。其他模式更复杂，不匹配更明显，例如列表理解表达式，它们在Beacon链的引用实现中被大量使用。在这些情况下，这种编码通常相当冗长，但如果不用k定义中间语言结构，就无法避免。然而，其优点是，这种编码容易实现更详细的覆盖率分析。
验证模型
以太坊基金会为信标链提供了丰富的测试套件。 除了用作Python实现的调试工具之外，第三方生产客户开发人员还使用测试套件来确保与参考实现一致。 该测试套件包含3,000多种不同的单元测试。
在给定的开发K模型抽象级别，可以在模型中直接执行信标链的标准测试套件中的测试，而无需任何工具。这证明是非常有价值的，因为它提供了一种机制来验证模型，并确保模型符合参考实现，就像验证其他生产实现一样,按照项目资源库中的说明，所有测试都可以自动运行。
扩展测试覆盖范围
标准信标链测试套件的设计使代码覆盖率最大化，可以使用Python的可用代码覆盖率分析工具。 但是Python的覆盖范围通常比较粗略。它不会区分执行语义丰富的Python构造（例如列表理解表达式）的各个分支。
K提供了不同的基于规则的覆盖率分析工具。它检测执行中是否应用了规则（如果适用，则应用了多少次）。 使用这种基于K的工具进行语义覆盖已经证明在其他语言（例如JavaScript）的环境中很有用，我们在所有浏览器中都发现了新的错误（这些结果在PLDI’15论文中进行了描述）。
因此该计划是评价标准的Python代码覆盖率如何确保语义覆盖面，看是否基于规则的覆盖分析可能暴露不是由标准的Python代码覆盖工具检测到任何未覆盖的功能。 确实分析显示测试未涵盖或未充分涵盖的执行路径，而Python覆盖率未检测到这些执行路径 这些检测中的大多数都属于复杂行为的规范，例如列表理解表达式和复杂循环中通常遇到的行为。
以下是K覆盖率工具生成的覆盖率分析报告的快照，显示了未在测试套件的任何测试中应用的规则。

继续向前
信标链的可执行k模型是实现正式验证信标链的基本安全性和活性特性及其参考实现这一最终目标的第一步，但也是至关重要的一步。事实上，如果没有一个可信的、形式化的系统模型来验证，形式化验证的问题是没有意义的。除了能够执行状态转换函数、运行测试和分析测试覆盖率之外，本文提出的k形式化模型还可以用来描述和验证在这种低抽象级别上可表示的低级别不变量。
但是信标链是一个非常复杂的协议。在这种较低的抽象级别上直接验证高级属性（如安全性和活动性）通常是不可行的。相反，通常使用抽象细化技术。因此我们的计划如下：
· 建立此具体模型的抽象，该模型保留协议的核心共识机制；
· 在抽象模型上证明所需的属性；
· 表明这些属性保留在具体模型中；

来源：区块链研究实验室

创业不易，用心坚持，希望您多多支持！

打赏

感谢您的支持，我会继续努力的!

扫码打赏

打开支付宝扫一扫，即可进行扫码打赏哦