为了确保规定我们的网络服务如何运行的协议是安全、可靠和按预期运行的重要一步，密歇根大学的研究人员已经自动化了一种称为形式验证的技术。

他们的系统无需任何人力就证明了最基本的分布式计算协议之一(称为Paxos)符合其规范。这一成就驳斥了一个普遍的假设，即Paxos协议和其他类似协议过于复杂，如果没有数小时的手动工作就无法证明是安全的。

“Paxos是最早也是最著名的想法之一，它为不同的事物如何异步达成一致奠定了基础，”计算机科学与工程博士生AmanGoel说，他在计算机的形式方法上展示了这项工作。辅助设计会议10月20日。

云计算的主导地位和区块链应用等新兴技术改变了组织和个人参与计算的方式，在不断增长的负载下创造了一个由网机器驱动的世界。

因此，我们的关键基础设施比以往任何时候都更容易受到服务器中断、黑客和有问题的网络行为的广泛影响。需要密闭的分布式协议来确保软件系统能够在遍布全球的机器上有效运行。

这些协议是极其复杂的算法，定义了网络中的机器如何作为单个系统协同工作。Paxos是该类别中最重要的示例之一，它描述了一种称为共识的方法，该方法已被用于几乎所有关键的分布式系统，包括云计算支持的所有应用程序。

最近，共识因支持加密货币等区块链应用而引起了广泛关注。通过帮助网络中的所有节点在交易发生时验证交易，此类协议构成了区块链的主干。

“大多数——如果不是全部——共识算法从根本上从Paxos派生出概念，”Goel说。

形式验证是一类技术，用于通过逻辑证明的优雅来证明某事是正确和可靠的。该过程对软件和硬件都非常有用，它提供了一个证书，证明某个算法、工作软件或计算机芯片将始终按照其规范规定的方式运行。从理论上讲，这将使软件能够以比当前所需的测试少得多的测试来发布。

计算机科学与工程教授KaremSakallah说：“拥有一个万无一失的系统，它说：你开发它，你自动检查它并获得正确性证书，这让你相信你可以毫无问题地部署程序。”

不幸的是，证明具有许多复杂行为的程序的正确性从乏味到不可能——这使得新兴的自动化过程的技术变得非常强大。但是对于Paxos规模的算法，自动化其形式验证被认为是一项无法成功完成的工作。

“过去曾多次尝试验证Paxos，包括许多手动尝试，”Goel说。“每个人都指出先前的理论结果表明自动化是不可能的——自动化工具无法证明这一点。”

该团队的解决方案利用了所有分布式协议的共同特性：规律性。在所考虑的系统中，所有处理特定功能的服务器都将处理大量看起来基本相同的请求，并且它们的任务性质随着时间的推移几乎没有变化。

这种规律性使Goel和Sakallah能够将原本看似不可能的大任务转变为看起来小而易于管理的任务。他们确实这样做了——通过在假设它具有固定的少量节点的情况下验证协议，然后将解决方案推广到“理论上无限数量”的节点。

研究人员为此证明设计的工具称为IC3PO，这是一个模型检查系统，可以查看程序可以进入的每个状态，并确定它是否与安全行为的描述相匹配。如果协议是正确的，IC3PO会产生所谓的归纳不变量——通过归纳证明该属性在所有情况下都成立。相反，如果在协议中发现错误，它将产生一个反例和执行跟踪，逐步显示错误的表现方式。

在不到一个小时的时间内为Paxos生成的归纳不变式IC3PO与之前使用称为交互式定理证明的技术通过大量人工努力得出的人工编写的一致。除了加快流程之外，它还生成了一个带有非常简洁易懂的文档的证明。

自动验证Paxos的正确性会对未来产生重大影响。由于新的共识协议是基于其不断变化的应用程序的原则构建的，因此它们需要被证明是安全可靠的。使用像这样的模型检查器可以使人们能够使用已被证明是安全的复杂软件，而无需了解其工作原理的每一个小细节。