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

区块链资讯区块链研究实验室2019-11-02 12:16:03  阅读 -评论 0

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

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

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

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

处理从创始状态(已处理的创始信标区块的状态)开始。给定要处理的下一个信标区块,并假定该区块有效,信标链状态转换功能将给定的信标链状态(前状态)转换为新状态(后状态)。此后状态反映了以下结果:
· 考虑(可能)丢失的区块; (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中的形式模型:以太坊2.0的主要权益证明区块链

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

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

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

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

只有当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中的形式模型:以太坊2.0的主要权益证明区块链

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

声明:链世界登载此文仅出于分享区块链知识,并不意味着赞同其观点或证实其描述。文章内容仅供参考,不构成投资建议。投资者据此操作,风险自担。此文如侵犯到您的合法权益,请联系我们kefu@lianshijie.com

参与讨论 (0 人参与讨论)

相关推荐

中信银行打造“区块链”信用证结算!

中信银行打造“区块链”信用证结算!

科技不会改变金融的实质,但却能让金融服务更高效,能让资金供、需方信息不对称的问题更好地解决。近期,中信银行首个区块链项目——基于区块链的国内信用证信息传输系统(简称BCLC)(一期)成功上线,这是国内银行业第一次将区块链技术应用于信用证结算领域。 据中信银行国际业务部总经理助理张栩青介绍,将现在流行的区块链技术应用在国内信用证中,改变了银行传统信用证业务模式,信用证的开立、通知、交单、承兑报文

中国信息技术部门成立区块链研究实验室

中国信息技术部门成立区块链研究实验室

暴走时评:本月初,中国政府对国内的ICO和数字货币交易所的打击在世界范围内引起了强大反响,但政府已经多次声明不会将区块链与数字货币划等号,依然非常重视区块链技术在中国的发展。鉴于中国工业和信息化部成立了一个专门研究区块链的实验室,这一论调也得到了进一步的证实。 虽然中国政府最近在大力打击比特币交易所和ICO,但仍然致力于开发区块链在其他领域的潜力。 据财新网报道,中国工业和信息化部已经成立了一

 分布式账本中的生命科学

分布式账本中的生命科学

生物科学是医学领域涉及遗传研究,疾病预防和生活方式治疗(lifestyle treatments)的学科。它已经存在了很长时间,但区块链技术的基础设施应用给该学科提供了重大进步的可能性。 根据Pistoia Alliance进行的2016年6月份高级制药和生命科学领袖调查,83%的受访者表示,他们预计在五年内将全面采用区块链技术。 Pistoia Alliance是一个全球性的非营利组织,致

区块链vs.核能:日本最大电力公司东京电力(TEPCO)寻求使用区块链减轻对核电的依赖

区块链vs.核能:日本最大电力公司东京电力(TEPCO)寻求使用区块链减轻对核电的依赖

东京电力公司 (TEPCO) 对于能源过度中心化的风险可以说绝不陌生。 也许最著名的就是2011年发生的福岛核电站事故,这个日本最大的能源公司如今正在寻求区块链技术来防止这种灾难再次发生。 然而,从使用微型风车的分布式风力发电到用于存储在电力成本低时购买的电力的智能电池,可替代能源项目一直以来都属于个人慈善事业。 然而,TEPCO风险投资部门主管Jeffrey Char认为区块链能够帮助为这

继证监会发表代币发行声明之后,香港交易所Gatecoin将下线部分ICO币

继证监会发表代币发行声明之后,香港交易所Gatecoin将下线部分ICO币

经过一系列监管以及合规审查后,香港交易所Gatecoin将会下线那些被金融监管部门定性为"证券"的代币。 香港加密货币交易所Gatecoin透露,如果在该平台交易的ICO代币在法律上符合"证券"定义,他们就会下线这些代币。据巴比特上月报道,香港主要的金融监管部门证券及期货事务监察委员会(SFC)表达了对ICO这种日渐普及的募资模式的担忧。 尽管ICO中售卖的数字代币通常都被定义为虚拟商品,但

IBM与超级账本共同加入去中心化身份基金会(DIF),推动创建区块链ID行业标准

IBM与超级账本共同加入去中心化身份基金会(DIF),推动创建区块链ID行业标准

IBM与超级账本已经签署协议加入去中心化身份基金会(DIF),这个于今年初成立的联盟旨在帮助推动基于区块链的ID系统的互操作性和标准。 这两个企业区块链大佬加入了这个有各种企业组成的团体,其中包括像微软和埃森哲这样的大企业,还有像Civic和Gem这样的创业公司,以及像uPort和Sovrin这样的开源项目。 DIF执行主管告诉Coindesk说: "这应该是一个信号,表明在这一领域有广泛的

为打击人口贩卖,牙买加警方盯上了犯罪分子的比特币钱包

为打击人口贩卖,牙买加警方盯上了犯罪分子的比特币钱包

作为打击人口贩卖计划的一部分,牙买加警方已经开始行动,锁定了那些试图用比特币和数字支付来掩人耳目的犯罪分子。 越来越多的人口贩卖者都开始转向数字货币来帮助他们进行地下活动并接收非法活动所得,但牙买加警方已经盯上他们了。 牙买加的'大生意' 不幸的是,人口贩卖以及性奴市场规模十分庞大,预计涉资1500亿美元。在牙买加,大约有7000个妇女、儿童以及成年男性被奴役,他们的操控者出售奴役服务的价格

深圳市将发布《深圳市扶持金融业发展若干措施》,奖励区块链、数字货币等金融创新

10月9日,深圳市人民政府向各区人民政府,市政府直属各单位印发《深圳市扶持金融业发展若干措施》(以下简称"《若干措施》")。深圳市政府表示,此举是为进一步完善金融支持政策体系,吸引集聚优质金融资源,推动全市金融业可持续均衡发展,加快建设国际化金融创新中心。 《若干措施》共分五大项,33条。内容包括:坚持服务导向,优化金融政策环境;发展金融总部经济,鼓励金融总部企业做大做强;支持金融企业分支机构

麦妖榜
更新日期 2019-09-03
排名用户贡献值
1牛市来了30910
2BitettFan24187
3等待的宿命23810
4区块大康20369
5六叶树20310
6linjm122719429
7天下无双16192
8lizhen00215280
9让时间淡忘14586
10yelanyi050511349
返回顶部 ↑