究竟什么是形式化验证方法？ 维基百科对形式化验证的解释是这样的： 「在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式化验证的含义是根据某个或某些形式化规范或属性，使用数学的方法证明其正确性或非正确性。」 神秘感大抵来源于定义中的两个严谨而且抽象的关键词——「形式化规范」和「数学方法证明」。事实上，揭开这层神秘的面纱，你会发现形式化验证的许多有趣之处。 下面这篇文章想要讨论的问题是： 在现阶段，以下哪个故事能够真正满足你对形式化验证的想象？形式化验证真的可以作为一种技术在区块链领域流行起来吗？如果可以，怎样才能做到？（PS：上文中提到的「形式化规范」的概念，在下文中也会讲到。） 要回答上面这些问题，我们可以先思考另一个更简单的问题： 现阶段，人们使用形式化方法来做什么？ 这个问题的答案无非有两种： 规避错误对抗攻击规避错误 规避错误其实就是避免损失。 我们首先来探讨一下，哪些领域对程序错误是零容忍的？在哪些领域，程序错误带来的损失难以估量？ 实际上，形式化方法是从硬件设计开始普及的。一个著名的例子是：当年 Intel 的 Pentium CPU 浮点运算单元出错（FDIV Bug），数以万计的 CPU 不得不回收和替换，给 Intel 造成了巨大损失（$475M）1。 从那之后，Intel 开始在其芯片设计中广泛采用形式化方法。 计算机硬件巨头如 IBM，AMD， NVIDIA 和 CADENCE2 等等也都是形式化方法的使用者… 要说起吃一堑才能长一智，其实各行各业都有试错者，在工业界也是如此。举个例子：1996 年，欧洲航天局首次发射的阿丽亚娜 5 型（Ariane 5）火箭，由于惯性导航系统发送的错误指令（浮点数转换为整数造成溢出），导致火箭在发射仅仅 37 秒后便偏离了预定轨道，最终坠毁。欧洲航天局的巨额研发经费（$8B）3 付之一炬。 在那之后不久，EADS 公司开发阿丽亚娜火箭的任务调度模型就开始使用形式化方法。 美国国家宇航局 NASA 和英国国防部在 90 年代相继发布设计标准 [4]，形式化方法的使用位列其中。我国的玉兔号月球车控制系统和我国第一个自主研发的空间飞行器嵌入式实时操作系统 SpaceOS[5]，也都是通过形式化方法验证其正确性。 历史的发展告诉我们，金钱才是推动社会发展的第一动力！程序错误带来的巨额损失，任谁也只能叹一声伤不起。 如果说上面两个故事听起来都过分沉重了，我们不妨看一下下面这张图：
上图显示了全球范围内用形式化方法开发的地铁项目分布情况 [6]。 可以看出，由巴黎地铁信号系统开始，在北美、欧洲、亚洲的主要国家，以及南美洲的部分国家的地铁系统开发中，形式化方法已经被广泛使用了。这或许是我们几乎从未听过由于地铁系统故障而造成重大损失和灾难的原因。 还是那句话，金钱是第一生产力。 既然形式化方法在保障日常出行方面做出的贡献已经得到广泛的认可，那么，在依托区块链技术而发展起来的数字资产领域，通过形式化验证技术来保障智能合约安全性、进而保障财产安全性的理念就显得合理甚至紧迫了。 具体需要怎么做？这里简单介绍一下。 首先需要引入一个「形式化规范」的概念了。
听起来很高大上，对不对？ 举个例子来说，对于一段智能合约程序，我们可以从它所有可能的输入（例如函数参数的组合）和初始状态（例如状态变量初始值的组合）出发，根据每条语句的语义，逐句推导出程序的所有可能的结束状态（例如合约执行结束后的状态变量的值和产生的 event lo），并检查合约的所有输入、初始状态、结束状态的组合是否都和形式化规范保持一致。这有点类似于柯南破案那样，一步步地推演。只不过，这里所有的定义都是通过严格的数学语言描述，推导和检查也是严格的数学推导和证明。根据待验证的系统及其形式化规范的复杂程度，推导和证明即可以手工构造，也可能可以由机器自动产生。 在实践中，推导和证明无法进行下去往往意味着设计和实现中存在不符合规范的 bug。通过分析推导和证明卡壳的位置和原因，可以定位出 bug 在设计和实现中的具体位置和成因。这样的方法，让数字资产领域中中严格意义上的规避错误、避免损失成为可能。 对抗攻击 对抗攻击其实是另一种意义上的避免损失。 故事从美国军方的一次电子攻击说起。2015 年夏天，一起黑客奉命对美国军方 Little Bird 无人直升机发动电子攻击，并掌握无人机控制权的事件中，黑客最初的攻击十分顺利，如入无人之境。然而，当美国国防部重新开发了该无人机的核心控制程序后，黑客们使用了当今世界上所有的攻击手段，都未能攻破新部署的系统 [7]。
到底是什么技术给予了 Little Bird 超强的防御能力，从而使它阻挡了所有的攻击？答案就是：形式化验证方法。 形式化验证方法通过严格的数学证明保证程序行为与预期一致，但形式化验证程序的正确性非常消耗人力，所以，与程序测试等通用技术不同的是，形式化验证方法常常只被应用于安全攸关领域，如无人机、航天器、操作系统等的程序正确性验证。 这里不得不提的是 2016 年发现的一个非常严重的 linux 操作系统内核漏洞 Dirty Cow （CVE-2016-5195）[8]，攻击者可以通过这个漏洞获得系统最高权限，从而使系统全部处于可被利用的状态之下。 在操作系统领域，一些人身先士卒，尝试用形式化方法避免安全攸关领域中的系统漏洞和黑客攻击。耶鲁大学邵中老师团队通过模块分层验证法（modularlayered verification methods）成功研发了安全性和可靠性极高的计算机操作系统 CertiKOS[9]；中科大软件安全实验室冯新宇老师团队也提出了一个针对抢占式多任务操作系统内核的形式化验证框架，并成功的应用在对嵌入式操作系统 uC/OS-II （该操作系统被广泛应用于航空电子产品中）的验证中 [10]。 安全攸关的区块链领域 区块链领域亦然，一方面，小错误也会导致大损失；另一方面，巨大的经济利益也会吸引大量的攻击者。 以太坊黑客攻击第一大案 The DAO 中，攻击者窃取了当时价值 5500 万美元的以太币，并且导致了以太坊的硬分叉 [11]；这之后，与以太坊智能合约相关的攻击一直在继续——比如，2017 年 11 月，以太坊 Parity 钱包由于被黑客攻击，导致用户损失了价值约为 1.5 亿美元的数字资产 [11]。 据安比实验室统计，仅 2018 年上半年，就已经有大约 11 亿美元的数字资产被盗，与区块链系统相关的漏洞（如以太坊中的智能合约漏洞）以及围绕数字资产的生态系统安全问题（如多个中心化交易所被盗）更是层出不穷。 目前区块链系统中的相关漏洞，以及数字资产生态系统的安全问题，归根结底是相关程序设计与实现的问题。在形式化方法以前，这类问题多是通过程序测试来发现的。 形式化验证进入区块链领域的初期，以太坊社区的 Yoichi Hirai 对以太坊（Ethereum）的智能合约虚拟机 EVM 做了完整的形式化建模 [12]。此外，来自 UIUC 大学的团队也对 EVM 进行了形式化的建模和验证。EVM 是以太坊智能合约的底层核心，关系到以太坊安全，涉及到数字资产保护等重大议题，引起了社区的广泛关注。 此外，MakerDAO 项目方发布了第一个经过形式化验证的去中心化应用程序（DApp）[13]。MakerDAO 是一个基于以太坊的智能合约平台，该平台提供了稳定币（stablecoin），抵押贷款（collateral loans），以及去中心化社区治理功能。为了保证所部署的智能合约的安全性，MakerDAO 团队对抵押贷款（CDP）核心引擎合约代码通过 K-Framewok 进行了验证，因此而表明其智能合约程序能够完全抵抗黑客攻击。 安比实验室也在以太坊智能合约形式化验证方面做了大量的工作，提出了一个智能合约形式化验证框架，并在该框架内证明了一些常见的 Token 合约，比如 ERC20，ERC721 等（其中包含转账、Token 总量等通用性功能）。这些被数学证明过的智能合约可以直接使用，不再需要担心安全问题。这些合约源代码和证明过程已经以开源 [14] 的方式贡献给社区。 Github 仓库地址： https://github.com/sec-bit/tokenlibs-with-proofs 结论 大多数人认为形式化验证方法高深莫测，究其原因，形式化验证方法不是一种通用技术，而是需要和领域结合来发挥价值的一种特定技术。在区块链领域，形式化方法究竟是一种 nice to have 还是一种 must have，也是与项目特点密不可分的。 随着区块链技术与项目应用的探索不断深入，项目方对于规避错误、对抗黑客攻击和避免财产损失的需求已经越来越强。 当互联网世界中的绝大部分活动都完成上链，当社会中的绝大部分群体都需要区块链的绝对安全来保护自己的财产安全的时候，形式化验证方法作为区块链技术的 must have 才会迎来大爆发。 写在最后 关于 Verification 与 Testing 的纠葛，你了解多少？ 最后来谈一下形式化验证（Formal Verification）与程序测试（Testing）之间的关系。 「程序测试能证明错误的存在 , 但不能证明错误不存在」。Edsger Dijkstra （1972 年图灵奖获得者、形式化方法核心思想的提出者）如此评述。 在实践中，尤其是在代码足够复杂的场景中，形式化验证（Verification）与程序测试方法（Testing） 的验证效果有如云泥之别。 举个例子来说：2009 年，澳大利亚的科学家使用形式化方法对工业级操作系统 seL4 微内核进行了完整功能性验证 [15]，验证方式同时以形式化验证和程序测试两种方式分别展开，验证的结果是：形式化方法共发现 460 多个 Bug，而程序测试只发现了 16 个 Bug。 更有趣的是，在以高验证成本著称的形式化验证领域，完全验证 seL4 微内核只需要 600 万美元的验证成本，而以测试的方式通过 CC EAL6 级认证的成本竟高达 8700 万美元 [15]。 由此可见，通过形式化验证可以更经济的为 seL4 微内核提供更强的安全性保证。 当然，有人说，程序测试是在「真实」环境里进行的，形式化验证只是数学层面，在「真实」环境中的测试是形式化验证无法取代的。从这个角度来说，形式化验证与程序测试如何做到共生互补？让这项技术在区块链领域真正流行起来，可能就是链圈同仁们接下来要共同探索的方向了。 参考文献 1 History of Formal Verification at Intel?https://dac.com/blog/post/history-formal-verification-intel 
—- 编译者/作者：安比实验室SECBIT 玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。 |
哪个故事真正符合你对形式化验证的想象？
2020-04-14 安比实验室SECBIT 来源：链闻
LOADING...