简析:智能合约和形式化验证 | 火星技术贴

DegameLabs链游实验室·热度: 22957
本文主要对智能和形式化验证进行介绍。

本文主要对智能和形式化验证进行介绍。

什么是智能合约

It's a Title Here

一个智能合约是一套以数字形式定义的承诺(commitment),包括合约参与方可以在上面执行这些承诺的协议。在区块链技术领域就是一段运行在区块链上的有多方参与的代码。最经典的例子是公开拍卖。

智能合约可以看做一个解决某个问题的程序,但是因为运行在区块链上,因为区块链的不可逆转特性,所以需要较一般程序更高的安全性要求,需要更严格的方法确保安全。


 

举个利用智能合约进行游戏的例子,现在有两个人A,B在玩游戏,两人先分别抵押2比特币,然后再下注一比特币,然后AB分别在01里面进行选择一个数字,分别退回他们的押金,然后如果他们两个人选的数字相同,则A得到两个比特币,如果数字不同,则B得到两个比特币。

现在我们只考虑AA要么在一定时间内向全网广播一个他选择的value的哈希值,然后广播他的value,要么在过了一段时间t之后,没有反应而因为超时受到惩罚,即其押金会转移给B

 我们可以利用智能合约完成这样的一个有着明确规则的过程。 

软件测试

软件测试的标准定义:在规定的条件下对程序进行操作,以发现程序错误,衡量软件质量,并对其是否能满足设计要求进行评估的过程。

 主要过程包括静态分析测试、动态分析测试、黑盒测试和白盒测试

 黑盒测试不用考虑内部结构,是从使用者的角度进行的测试


 白盒测试需要对程序内部考虑,程序执行流程图内的每一条路径都要考虑到,每个分支语句,每个判断语句都要分别进行测试

 一个软件测试的进行分为制定测试计划->进行测试设计->测试开发->执行测试->测试评估等过程

 如果要正确的进行黑盒测试,软件规格说明书一定要正确,但是但很难完全正确,同时不可能对程序进行毫无遗漏的测试

 如果要正确的进行白盒测试,测试用例要全面,但是代价昂贵,容易遗漏

 以上所说的黑盒测试和白盒测试会占用大量的人力物力财力,庞大的工作量产出繁杂的报告,但是正确性得不到完全保证。

 一般的软件开发,项目经常延误,预算经常超支。开发的后续阶段会发现很多前期错误,代价高昂,更可怕的是,如果是运行了很久的智能合约,很有可能会发生类似于DAO漏洞的重入攻击。

 

 DAO漏洞的原因:在以太坊上运行的智能合约在涉及到以太币的转移时,如果合约内部没有处理以太币转移的函数,则会自动调用fallback函数,当恶意用户在智能合约的fallback函数再次转移以太币时,会形成转移以太币然后调用fallback函数的循环,导致合约内的以太币不断转入用户地址。

 形式化验证

目前形式化方法的主要研究对象是计算机系统的设计和验证,其主要目的是帮助工程师构造正确可靠的计算机系统,形式化方法最基本的特点是利用数学的概念、方法和工具来解决设计的正确性问题,作为形式化方法的主要数学基础包括各种逻辑学、集合论、代数理论、图论。

 我们举coq的例子为例,如果要证明对于任意布尔变量,not(not b)=b,如果b是布尔变量,我们可以先destruct,将b分解为0,1,对两个值分别求结果进行验证。(coq就是一个数学证明的过程)

继续举刚才的游戏例子。   

 比特币对智能合约的支持并不是很好,一般是通过比特币脚本在比特币系统加入智能合约。所以,《BitML: A Calculus for Bitcoin Smart Contracts》论文即是对于比特币系统上的智能合约(或者比特币脚本)建立的形式化验证语言。

 下面是《BitML: A Calculus for Bitcoin Smart Contracts》论文中形式化验证的例子:

 

在其特定编译器里,上述代码的意思是PayOrRefund函数有两种结果,要么在A的允许下,B将合约中的比特币拿走,要么,在B的准许下,A将合约中的比特币拿走。

 

上述代码的意思是:当AB都因超时而违规时,需要管理人员的介入,在上述例子中,0.1比特币将转入管理人员M的账户中,余下的0.9比特币将在M的授权下,进入AB的账户。

 

上述代码的意思是我们上述合约的形式化:

 首先,如果B没有违规,在规定时间内向全网广播了其value的哈希值和value值,那么B可以收回押金。同理,A也一样。当AB都广播了其哈希值和value值时,如果value值相同,则A可以获得2比特币,如果value值不同,则B可以获得2比特币。

 对于上述的形式化语言,论文中自行设计了一个编译器,用来专门编译上述的语言。

 形式化验证对智能合约的意义

 形式化验证并不能完全确保系统的性能正确无误,但是可以从逻辑上最大限度地理解和分析系统,并尽可能地发现其中不一致性、模糊性、不完备性等错误。形式化验证可用来消除高风险代码漏洞。

 形式化验证对软件测试的意义

 减轻人力物力的使用

相比于其他测试,形式化验证更加可靠

 

公众号:DegameLabs链游实验室,专注于区块链游戏新玩法,行业解读,游戏咨询,技术分享,更多精彩内容请关注公众号。

声明:本文为入驻“火星号”作者作品,不代表火星财经官方立场。
转载请联系网页底部:内容合作栏目,邮件进行授权。授权后转载时请注明出处、作者和本文链接。 未经许可擅自转载本站文章,将追究相关法律责任,侵权必究。
提示:投资有风险,入市须谨慎,本资讯不作为投资理财建议。
免责声明:作为区块链信息平台,本站所提供的资讯信息不代表任何投资暗示,本站所发布文章仅代表个人观点,与火星财经官方立场无关。鉴于中国尚未出台数字资产相关政策及法规,请中国大陆用户谨慎进行数字货币投资。
语音技术由科大讯飞提供
最近更新
本文来源:DegameLabs链游实验室
原文标题:
24H热门新闻
暂无内容

评论0