区块链研究实验室｜区块链系统和智能合约的形式验证101

区块链技术与智能合约的结合提供了诱人的前景：为具有严格安全要求的应用程序（如财务，安全消息传递等）启用分布式，可信任且可验证的计算平台。不幸的是，人们不必很难看出，区块链的实现道路还是充满很多不知因素，例如Gox，DAO，对以太坊经典版的攻击以及智能合约bug。尽管从理论上讲区块链系统可能听起来不错，但在实践中，区块链系统和智能合约仍然很容易出现开发人员bug。
区块链系统的支持者必须扪心自问的问题是：我们如何才能挽救（a）区块链技术在构建新一类分布式系统方面的承诺，以及（b）它在警惕的公众眼中的声誉？显然，这是一个多方面的问题，不能在一篇文章中完全解构。但是在本系列文章中，我们将论证形式验证（以下更多内容）将在应对这两个挑战（a）-（b）中发挥越来越重要的作用。
该系列文章涉及适用于区块链系统和智能合约的形式验证。在第一篇文章中，我们希望对形式化验证（没有具体提及区块链或智能合约）以及为什么需要它提供一个概括而温和的介绍。在以后的文章中，我们将详细介绍技术细节。除了介绍之外，让我们开始吧！
无论是建立业务，产品还是软件系统，您都必须回答以下问题：我们的系统是否满足我们的基本要求？这个问题涉及两部分：
1. 待验证的系统2. 需求清单
我们称此为回答问题验证的过程。完整的验证意味着检查系统是否满足其所有要求，即通过检查所有可能的情况，检查系统是否完成了它应该做的所有事情，而没有做不应该做的事情。这就引出了一个重要的问题：我们如何验证我们的系统？
如果您向大多数软件开发人员询问此问题，他们将通过一些不同的测试来回答。什么是测试？测试是我们采用系统并询问自己是否的过程。如果我们从某些初始条件开始（例如，我们的Web服务器具有1 GB的RAM），我们能否达到预期的效果？答案当然取决于我们正在研究的系统。不幸的是，通过添加更多的测试用例来扩展测试功能只能确保对最简单的系统进行完整的验证，因为这些系统对复杂性有固定的限制。
作为一个简单的例子，考虑必须为许多用户服务的Web应用程序，例如银行网站。理论上可能有多少套初始条件？显然，同时服务5个用户不同于同时服务6个用户。无限期地应用此参数，请注意由于单个输入变量（即同时使用的用户数），我们已经可以考虑无数种情况。
这正是验证（特别是形式验证）可以提供帮助的地方。
形式验证通常不使用显式状态（如我们上面所使用的那样），而是使用符号输入变量（例如如果我们的网站有n个同时用户怎么办？）以及相关系统的精确数学模型。从本质上讲，我们将验证问题转化为精确的数学命题，然后使用数学证明来证明该命题的正确性。
这是形式验证的主要优点：当一个命题被正式证明时，您就可以通过有限的测试步骤来验证无限数量的测试用例。我们将从以下图表开始调查如何（针对软件系统）执行此操作：

在图中，方框表示在验证过程中产生的不同工件，而连接线表示从一种工件到另一种工件的转换。实线表示保留所有基本信息的转换，而虚线表示有损转换，可能丢失基本信息。所有行均由执行所需转换所需的实体注释。在常规软件开发中，开发人员（通常也是编译器）一起将系统需求转换为可执行代码。然后（可能是不同的）开发人员将采用相同的系统要求，并编写挂接到可执行代码中的测试，以确保某些代码路径返回期望的结果。这些测试有助于显示我们的代码正确，但是我们已经知道测试还不够。尽管测试可以证明存在bug，但是通常无法证明没有缺陷。形式验证的好处在于，我们可以证明我们的要求与系统规范之间的对应关系，即我们可以证明我们的源代码没有bug。
我们在此过程中使用的关键工具是语义。您可以将语义视为将代码映射为其数学含义的编译器。我们使用的另一个关键工具是定理证明器，它只是一个计算机程序，可以帮助我们证明数学命题并避免粗心大意的bug。由于我们的形式化需求和形式化系统规范都是数学陈述，因此我们可以使用定理证明者来讨论它们之间的关系。因此要回答这个问题：
我们怎么知道我们的系统实现满足我们的系统要求？
我们将思维转移到形式化的数学领域，而是问：
定理证明者可以证明我们的形式化系统规范满足我们的形式化要求吗？
在接下来的三篇文章中，您将学习形式验证如何将系统正确性问题从非正式的人类推理转变为形式化的数学推理。结果，您将能够在实践中理解并享受采用正式验证的好处：

精确。系统，形式和数学推理为我们提供了思考系统设计的精确语言；
自动化。许多重要的正式验证任务都可以由计算机自动执行。这意味着我们可以考虑非常棘手的问题，这些问题对于人类来说是难以解决的。
置信度。当使用复杂的旧系统时，尤其是在不受信任的环境中（例如IoT /嵌入式系统等），正式验证可以高度确保您没有做错事。
速度。 在设计新系统时，我们认为基于语义的形式验证可以通过减少代价高昂的设计错误来加速系统设计和编写良好代码的过程。

我们希望您对正式验证有一个简单的概述，并且您将加入我们的系列文章的下三篇文章，其中将放大基于语义的正式验证过程的三个阶段，如上图所示，以及它们如何应用于区块链系统：
（i）形式化需求（ii）用于形式化验证的定理证明工具（iii）形式化系统语义。

描下方二维码添加我，拉您进入技术交流群
扫码
关注我们

获得