DEVCON2: Solidity的形式化验证

记者：Lydia

Dr. Christian Reitwiessner 和Dr. Yoichi Hirai为大家做了较为详细的演讲关于Solidity的形式化验证。并表示区块链是形式化验证的天堂。形式化验证来临了！

Christian Reitwiessner：编写100%正确的代码是非常困难的，不论是智能合约上的还是其他上面的，因为我们对正确的定义很含糊。如果合约代码做的事和我们想做的事情一致就是正确的，如果和我们的意图冲突就不是一个正确的代码。我希望我们的意图和用户的意图是一样的。

有一些办法可以实现这些意图

我们可以进行一些简单的测试，进行一些输入，做出适当的预期，然后看真正发生的是否和我们的预期相符合。可是实现本身和预期不一样时，因此需要我们用不同的方法对合约进行调用，测试可以通过许多方法进行。

形式化验证的例子

非常简单的代码合约，有余额、映射。

余额可以从一个账户转移到另一个账户，这里有一个非常小的错误。可能测试会查到这个错误，大多数代币合约都会正常运转，这里可能会有溢出的现象，如果核超过256，这个机制就不是正常运转的。

形式化验证运作原理

提供关于合约行为的函数，证明代码可以满足这样的声明，因此我们有自动化声明的算法，这不能解决所有问题，源代码或编程语言就是程序的形式化描述，用另外一种语言添加形式化声明没有太大帮助，最重要的是人心里的模型，形式化验证是为了降低合约的复杂性，它做了什么比怎么做更容易理解，最重要的是是余额总额是固定的吗？有方法修改余额吗？或智能合约是否卡住了？是否能调用函数？形式化验证的时代已经来临了，有很多研究论文，因为区块链是形式化验证的天堂，模型非常简单。

形式化验证的工具还有一些统一的语言如C、Java等，进行注释，可以用工具把源代码编译到语言中。我们用自动化证明算法检验形式化陈述的条件。

（接下来是形式化验证专家Dr. Yoichi Hirai，加入了以太坊基金会。他表示以太坊虚拟机非常好，是智能规范，所有客户端都要遵循这个规范，另外多次指出对于验证工程师，针对现实问题非常重要）

Dr. Yoichi Hirai ：

对于智能合约而言，针对Solidity的形式化验证，可以用转账的功能处理代币转账。合约本身十分简单，有转账函数可以规定发送地址，和Christian说的一样。整数溢出问题是一样的，如果不规定总数余额一样大，不然就没什么问题。Y3是针对自动化的程序证明算法，可以看到各种证明条件，如没有整数溢出，Y3可以验证大多数性能，还不知道这些蓝色问题是否站得住脚，右边黄色的是一段代码。这里是一个减法，看到这样的问题可以修改你的程序，要调整心理模型。

接下来，在找到以太坊之前，一直在寻找应用形式化验证的方法，但是没办法用到任何公司的源代码，因此加入了一家美国的公司，同事都在写证明的算法，但是我不是特别开心，因为这些代码都不是针对实际的问题，没有人把文档翻译成以太坊算法。后来看到有以太坊算法和黄皮书，我就说我可以翻译，Christian找到我，我就加入了有以太坊基金会。

以太坊虚拟机非常好，因为有智能的规范，这是针对现实问题，所有客户端都想针对这些规范，对于形式化验证工程师来说，针对现实问题非常重要，我们有一些未来研究工作，我们会遇到一些问题，如没办法调用翻译函数，或进行映射，我们想用Fstar，可以给我们提供开放源。

我们在向很多小的合约方面转移，还有推论solidity代码非常重要，推动联合代码有时会有错误。因此需要知道自解码非常有必要。

目前合约最大的条件就是代码，从第一个调用到回车，验证范围必须扩展，和链下协议进行合并，一旦下链 ，人们的行为不会受到规则的限制，但是一定要鼓励参与者和我们合作。

形式化验证可以探索所有互动的可能性。

我们之前看到了蓝色的问题，可能不足以让我们来找到一些问题。某种条件下这样的状态是崩溃的。

越来越多的形式化验证人员进入了智能合约研究领域，对很多开发人员来说区块链是一个天堂。

作者：Lydia | 来源：Chainb