区块链概念图。信用:U-M工程在确保决定我们的网络服务如何安全运行的协议方面迈出了重要的一步，密歇根大学的研究人员已经自动化了一种称为正式验证的技术。他们的系统无需任何人工努力就证明了最基本的分布式计算协议之一——被称为Paxos——符合其规范。这项成就驳斥了一个普遍的假设，即Paxos协议和其他类似协议过于复杂，如果没有数小时的手动工作，就无法证明是安全的。
“Paxos是第一个也是最著名的想法之一，它为不同的事物如何异步达成一致奠定了基础，”计算机科学和工程专业的博士生Aman Goel说，他在10月20日的计算机辅助设计正式方法会议上介绍了这项工作。
云计算的主导地位和区块链应用程序等新兴技术改变了组织和个人参与计算的方式，创造了一个由不断增长的负载下的联网机器驱动的世界。
因此，我们的关键基础设施比以往任何时候都更容易受到服务器中断、黑客和漏洞百出的网络行为的广泛影响。需要密封的分布式协议来确保软件系统能够在遍布世界各地的机器上有效运行。
这些协议是极其复杂的算法，定义了网络中的机器如何作为单个系统协同工作。Paxos是这一类别中最重要的例子之一，它描述了一种被称为共识的方法，该方法已被用于几乎所有关键的分布式系统，包括云计算支持的所有应用程序。
最近，人们一致认为加密货币等区块链应用程序已经得到广泛关注。这种协议通过帮助网络中的所有节点在事务发生时验证事务，形成了blockcha的主干。
“大多数——如果不是全部的话——共识算法从根本上源自Paxos的概念，”Goel说。
形式验证是一类用逻辑证明的优雅来证明某事是正确和可靠的技术。该过程对软件和硬件都非常有用，它提供了一个证书，证明某个算法、软件的工作部分或计算机芯片将始终按照其规范要求的方式运行。理论上，这将使软件的发布比当前需要的测试少得多。
“拥有一个万无一失的系统，上面写着:你开发它，你自动检查它，你会得到一个正确性证书，这让你有信心可以毫无问题地部署一个程序，”计算机科学与工程教授Karem Sakallah说。
不幸的是，用许多复杂的行为来证明一个程序的正确性从乏味到不可能，这使得新兴的自动化过程的技术变得极其强大。但是对于Paxos这样规模的算法来说，自动化它的正式验证被认为是一项太大的工作，永远无法成功完成。
Goel说:“过去有很多验证Paxos的尝试，包括很多手动尝试。“每个人都指出一个先前的理论结果，即自动化是不可能的——能够证明这一点超出了自动化工具的范围。”
该团队的解决方案利用了所有分布式协议共有的一个特性:规律性。在所考虑的系统中，所有在特定功能上工作的服务器将处理大量看起来基本相同的请求，并且它们的任务性质将随着时间的推移变化很小。
这种规律性使戈尔和萨卡拉能够把一开始不可能完成的大任务转变成看起来小而易管理的任务。他们实际上是这样做的——通过在假设协议有固定的少量节点的情况下验证协议，然后将解决方案推广到“理论上无界数量”的节点。
研究人员为这一证明设计的工具被称为IC3PO，这是一个模型检查系统，它查看程序可以进入的每个状态，并确定它是否与安全行为的描述相匹配。如果pr otocol是正确的，IC3PO产生一个所谓的归纳不变量——一个通过归纳证明该属性在所有情况下都成立的证明。相反，如果在协议中发现一个错误，它将产生一个反例和执行跟踪，一步一步地显示这个错误是如何表现出来的。
在不到一个小时的时间里，为Paxos制作的归纳不变IC3PO与之前人工编写的IC3PO完全一致，后者是使用一种称为交互式定理证明的技术通过大量人工努力获得的。除了加快流程之外，它还通过非常简洁和易于理解的文档提供了证据。
自动验证Paxos的正确性对未来有重大影响。随着新的共识协议建立在其不断变化的应用原则之上，它们需要被证明是安全的。使用像这样的模型检查器可以让人类使用被证明是安全的复杂软件，而不必了解它如何工作的每一个小细节。
来源：由phyica.com整理转载自PH，转载请保留出处和链接！
