智能合约的形式化验证

智能合约的形式化验证是用一个自动的数学证明来验证源代码实现了某种形式的规范(Specif ication)。以太坊的高级编程语言Solidity的主导开发者Christian Reitwiessner正在将形式化证明引擎Why3整合到Solidity中,让用户可以在Solidity程序中插入与某种数学论点有关的证据,并在编译的时候进行验证。此外,还有一个项目在将形式化证明技术Imandra整合到以太坊虚拟机的代码里。

Hyperledger Fabric正在进行一项名为Composer的项目。这个项目可以使得开发人员用模型语言(Modelling Language)编写应用的需求,Composer可以把需求自动生成智能合约。Composer的形式化验证工具将按照模型语言产生的智能合约进行分析。如果是正确的,工具会给出肯定的判断;如果不正确,工具会输出一个反例,解释为什么智能合约不符合需求的规范。这个工具现在还没有,但是做出来以后对Hyperledger Fabric的开发者在安全方面少犯错误会有很大的帮助。

形式化验证在一定程度上能够保护智能合约的安全。比如,The DA0安全问题在发生以前曾经山一些安全专家对代码进行审核,但是在项目众筹(ICO)以前没有发现安全问题,后來一个不知名的黑客利用智能合约的漏洞偷走了相当于7千万美金的代币。这次事件的后果是The DAO项目破产,以太坊币的分叉。如果使用形式化验证,智能合约的漏洞就可以被发现。需要注意的是,形式化验证本身只能帮助我们了解我们设计的规范和区块链智能合约的操作(实际实现)之间的区别。我们仍然需要检查规范是否是我们想要的,这个形式化证明是帮不上忙的。我们需要在整个智能合约的开发过程中,包括需求收集过程中考虑安全的问题。

868区块链学习网为您整理《智能合约的形式化验证》仅供参考。