Preethi Kasireddy， medium.com （来源）
智能合同的正式验证仍然是一个大问题。首先，让我们理解“正式验证”一个合同的含义，即理解什么是“正式证明”。数学中的“正式证明”意味着一个证明已经被计算机用数学的基本公理和原始推理规则检验了的数学证明。
更广泛地说，与软件程序相关的正式验证是确定程序是否按照规范行事的方法。一般来说，这是用一个具体的规范语言来完成的，这个语言用来描述函数的输入和输出应该如何相关。换句话说，我们首先声明一个关于该程序的不变性，然后我们需要证明这个说法。
规范语言的一个例子是Isabelle，它是一个通用的证明助手，允许数学公式以正式语言表达，并提供在逻辑演算中证明这些公式的工具。另一种规范语言的例子是Coq，它是编写数学定义，可执行算法和定理的正式语言。
那么，为什么对智能合约中编码的程序进行正式验证很重要？
首先，智能合约是不可改变的，这意味着一旦将它们部署到以太网的主网后，就不能更新或修复它们。所以这意味着在我们在真实世界的应用程序中部署和使用这些合同之前，我们需要把所有的事情完善了。而且，智能合约是可以公开访问的，任何存储在智能合约中的东西都是开放的，任何人都可以调用智能合约的公共方法。虽然这提供了开放性和透明度，但它也使得智能合约成为黑客极具吸引力的目标。
事实上，无论您采取多少预防措施，编写无缺陷的智能合约都很困难。而且，以太坊为例，由于EVM指令的设计方式，验证EVM代码非常困难。这使得为以太坊建立正式的验证解决方案变得更加困难。无论如何，正式验证是减少漏洞和攻击风险的有效方法。它们比传统方法（例如测试，同行评审等）提供了更高的正确性保证，我们迫切需要更好的解决方案。
关于正式验证的解决方案
我希望我有更多公开的解决方案在本节炫耀，但不幸的是并不多。我发现的一个非常早期的例子是由以太坊基金会的正式验证工程师Yoichi Hirai完成的。他能够早日获得验证几个智能合同的结果，包括一个小的“契约”合同。虽然很小，但这是我在定理证明环境中分析的第一个“真实”合约。
正如Yoichi Hirai本人说的
“验证结果还不够完善。在验证设置方面，我仍然发现比验证合同更多的问题。 EVM（以太坊虚拟机）实施不针对其他人进行测试！我已经公开这个项目了，因为这个项目是使用机器辅助逻辑推理验证智能合约所需的工作量（和细节水平）的一个很好的例子。在这个时候，如果我要实现一个价值超过10万美元的智能合约，并且我负责这个计划，我会考虑这种发展（另一个选择是先尝试较小值的合同）“。
还有其他一些团队，如Tezos完全放弃使用Solidity作为语言，EVM作为VM，而是建立自己的智能合约编程语言和虚拟机，以促进正式验证。
无论是正确的方法，无论是彻底改革EVM使其更容易正式验证或建立一个本身更容易验证的全新语言，我们需要做更多的工作。我们需要更多的正式验证的研究人员和开发人员。我们需要更多的研究人员和开发人员关注正式验证。对每种可用于正式验证的编程语言中需要验证库和标准。
网友评论