验证区块链开发程序和验证程序

智能合约是一种自我执行的工具，它的增长是随着区块链的兴起而出现的。随着这项技术的采用，这些金融工具的实际存款额不断增加，同时它们的复杂性也严重升级。这种情况会周期性地导致代价高昂的bug和漏洞，从而为更严格的程序分析方法带来光明。

在这方面，在永久部署分散式的应用程序之前，测试和审计通常为开发人员和用户提供一定的保证。但是，由于没有代码检查可以100%保证消除所有bug，所以正式的验证可以通过数学方法带来更高的可信度。这就是为什么这一领域受到以太坊基金会的积极支持，并可能迅速得到更广泛的应用。

动态分析包括执行代码或模拟代码，以发现任何bug。创建测试计划包括列出要测试的用例，并为每个用例建立一个测试。由于这些测试不能全面，动态分析一般不能构成正确性的证明。

另一方面，静态分析包括遍历代码而不执行代码，以证明某些属性。存在不同的方法，例如基于模型检查或Hoare逻辑。形式验证依赖于静态分析。

2016 年初，一组研究人员分析了部署在以太坊主网上的字节码，以查找常见的安全缺陷。他们惊人的评估被大量引用：在19366份研究合约中，8833份至少存在一次安全漏洞。在本文提倡改进以太坊的操作语义以帮助形式化验证的同时，出现了一个问题：一些区块链框架是否比其他框架更不容易进行形式化验证？

很难否认，每个区块链都是为了满足特定的期望子集而设计的，比如快速采用或安全性。

直接的结果是，正式的验证在一些框架上是当前的现实，而在另一些框架上可能是长期的目标。

在这方面，2018年发表的一份有趣的研究报告概述了合同语言和验证方法，作为对当前解决方案的全面调查。它有助于确定以下区分因素，并概述当前主要框架上正式方法的可用性。

随着区块链价值的增加和分散化应用程序复杂性的增加，推广一种更严格的程序分析方法似乎是向客户和合与所有者提供更高安全级别的唯一可接受的方法。

形式验证是一门成熟的科学，可以为实现这一目标作出重大贡献。

然而，在其他框架上，今天可以进行正式的验证。现在要靠分散式应用程序的创建者来迎接这一挑战，并努力为更安全的智能合约铺平道路。