iNews新知科技 关注科技，自有新知
从诞生至今，形式化验证（Formal Verification）方法一直与“小众、冷门”等字眼挂钩。有人说形式化验证方法是一种“军用级别”的防黑客手段，更是为这项技术增添了一丝神秘感。
究竟什么是形式化验证方法？
维基百科对形式化验证的解释是这样的：
在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式化验证的含义是根据某个或某些形式化规范或属性，使用数学的方法证明其正确性或非正确性。
神秘感大抵来源于定义中的两个严谨而且抽象的关键词——“形式化规范”和“数学方法证明”。事实上，揭开这层神秘的面纱，你会发现形式化验证的许多有趣之处。
下面这篇文章想要讨论的问题是：在现阶段，以下哪个故事能够真正满足你对形式化验证的想象？形式化验证真的可以作为一种技术在区块链领域流行起来吗？如果可以，怎样才能做到？
（PS：上文中提到的“形式化规范”的概念，在下文中也会讲到。）
要回答上面这些问题，我们可以先思考另一个更简单的问题： 现阶段，人们使用形式化方法来做什么？ 这个问题的答案无非有两种： 1、 规避错误 2、 对抗攻击
| 规避错误
规避错误其实就是避免损失。
我们首先来探讨一下，哪些领域对程序错误是零容忍的？在哪些领域，程序错误带来的损失难以估量？
实际上，形式化方法是从硬件设计开始普及的。一个著名的例子是：当年Intel的Pentium CPU浮点运算单元出错(FDIV Bug)，数以万计的CPU不得不回收和替换，给Intel造成了巨大损失(475M $)[1]。
从那之后，Intel开始在其芯片设计中广泛采用形式化方法。
计算机硬件巨头如IBM，AMD， NVIDIA 和 CADENCE[2]等等也都是形式化方法的使用者…
要说起吃一堑才能长一智，其实各行各业都有试错者，在工业界也是如此。举个例子：1996年，欧洲航天局首次发射的阿丽亚娜5型（Ariane 5）火箭，由于惯性导航系统发送的错误指令（浮点数转换为整数造成溢出），导致火箭在发射仅仅37秒后便偏离了预定轨道，最终坠毁。欧洲航天局的巨额研发经费（8B $）[3]付之一炬。
在那之后不久，EADS公司开发阿丽亚娜火箭的任务调度模型就开始使用形式化方法。
美国国家宇航局NASA和英国国防部在90年代相继发布设计标准[4]，形式化方法的使用位列其中。我国的玉兔号月球车控制系统和我国第一个自主研发的空间飞行器嵌入式实时操作系统SpaceOS[5]，也都是通过形式化方法验证其正确性。
历史的发展告诉我们，金钱才是推动社会发展的第一动力！程序错误带来的巨额损失，任谁也只能叹一声伤不起。
如果说上面两个故事听起来都过分沉重了，我们不妨看一下下面这张图：
上图显示了全球范围内用形式化方法开发的地铁项目分布情况[6]。
可以看出，由巴黎地铁信号系统开始，在北美、欧洲、亚洲的主要国家，以及南美洲的部分国家的地铁系统开发中，形式化方法已经被广泛使用了。这或许是我们几乎从未听过由于地铁系统故障而造成重大损失和灾难的原因。
还是那句话，金钱是第一生产力。
既然形式化方法在保障日常出行方面做出的贡献已经得到广泛的认可，那么，在依托区块链技术而发展起来的数字资产领域，通过形式化验证技术来保障智能合约安全性、进而保障财产安全性的理念就显得合理甚至紧迫了。
具体需要怎么做？这里简单介绍一下。
首先需要引入一个“形式化规范”的概念了。
形式化规范 (formal specification) 是指通过数学语言对系统的预期行为 (例如将数量 S 的 token 从账户 A 转移到账户 B) 和性质 (例如转账不会造成账户 B 额度的溢出) 进行严格和全面的定义。形式化规范往往定义了系统的正确性和安全性。给定一个系统的形式化规范，我们即可以从规范出发开始迭代设计和实现出这个系统。在迭代的每一步中，我们可以通过精化 (refinement)、集成 (synthesis) 、形式化证明在内的一系列方法在数学上严格的保证迭代产生的系统和迭代前的规范或者系统保持一致。
除了从形式化规范出发设计和实现一个系统，我们也可以使用包括符号执行 (symbolic execution)、模型检测 (model check) 和形式化证明 (formal proving) 在内的一系列方法验证已有的设计和实现与该规范保持一致。
听起来很高大上，对不对？
举个例子来说，对于一段智能合约程序，我们可以从它所有可能的输入 (例如函数参数的组合) 和初始状态 (例如状态变量初始值的组合) 出发，根据每条语句的语义，逐句推导出程序的所有可能的结束状态 (例如合约执行结束后的状态变量的值和产生的 event log)，并检查合约的所有输入、初始状态、结束状态的组合是否都和形式化规范保持一致。这有点类似于柯南破案那样，一步步地推演。只不过，这里所有的定义都是通过严格的数学语言描述，推导和检查也是严格的数学推导和证明。根据待验证的系统及其形式化规范的复杂程度，推导和证明即可以手工构造，也可能可以由机器自动产生。
在实践中，推导和证明无法进行下去往往意味着设计和实现中存在不符合规范的 bug。通过分析推导和证明卡壳的位置和原因，可以定位出 bug 在设计和实现中的具体位置和成因。这样的方法，让数字资产领域中中严格意义上的规避错误、避免损失成为可能。
| 对抗攻击
对抗攻击其实是另一种意义上的避免损失。
故事从美国军方的一次电子攻击说起。2015年夏天，一起黑客奉命对美国军方Little Bird无人直升机发动电子攻击，并掌握无人机控制权的事件中，黑客最初的攻击十分顺利，如入无人之境。然而，当美国国防部重新开发了该无人机的核心控制程序后，黑客们使用了当今世界上所有的攻击手段，都未能攻破新部署的系统[7]。
到底是什么技术给予了Little Bird超强的防御能力，从而使它阻挡了所有的攻击？答案就是：形式化验证方法。
形式化验证方法通过严格的数学证明保证程序行为与预期一致，但形式化验证程序的正确性非常消耗人力，所以，与程序测试等通用技术不同的是，形式化验证方法常常只被应用于安全攸关领域，如无人机、航天器、操作系统等的程序正确性验证。
这里不得不提的是2016 年发现的一个非常严重的 linux 操作系统内核漏洞Dirty Cow (CVE-2016-5195)[8]，攻击者可以通过这个漏洞获得系统最高权限，从而使系统全部处于可被利用的状态之下。
在操作系统领域，一些人身先士卒，尝试用形式化方法避免安全攸关领域中的系统漏洞和黑客攻击。耶鲁大学邵中老师团队通过模块分层验证法(modular layered verification methods)成功研发了安全性和可靠性极高的计算机操作系统CertiKOS[9]; 中科大软件安全实验室冯新宇老师团队也提出了一个针对抢占式多任务操作系统内核的形式化验证框架，并成功的应用在对嵌入式操作系统 uC/OS-II （该操作系统被广泛应用于航空电子产品中）的验证中[10]。
| 安全攸关的区块链领域
区块链领域亦然，一方面，小错误也会导致大损失；另一方面，巨大的经济利益也会吸引大量的攻击者。
以太坊黑客攻击第一大案The DAO中，攻击者窃取了当时价值5500万美元的以太币，并且导致了以太坊的硬分叉[11]；这之后，与以太坊智能合约相关的攻击一直在继续——比如，2017年11月，以太坊Parity钱包由于被黑客攻击，导致用户损失了价值约为1.5亿美元的数字资产[11]。
据安比实验室统计，仅2018年上半年，就已经有大约11亿美元的数字资产被盗，与区块链系统相关的漏洞（如以太坊中的智能合约漏洞）以及围绕数字资产的生态系统安全问题（如多个中心化交易所被盗）更是层出不穷。
目前区块链系统中的相关漏洞，以及数字资产生态系统的安全问题，归根结底是相关程序设计与实现的问题。在形式化方法以前，这类问题多是通过程序测试来发现的。
形式化验证进入区块链领域的初期，以太坊社区的Yoichi Hirai对以太坊（Ethereum）的智能合约虚拟机EVM做了完整的形式化建模。此外，来自UIUC大学的团队也对EVM进行了形式化的建模和验证[12]。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
【2】王健：说说形式化验证（Formal Verification）吧
http://chainb.com/?P=Cont&id=1957
【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher
https://link.springer.com/chapter/10.1007/11768869_6
【4】Tenth NASA Formal Methods Symposium https://shemesh.larc.nasa.gov/NFM2018/
【5】玉兔使用的国产SpaceOS操作系统未来有望衍生出民用版本
http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html
【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.
【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/
【8】利用Dirty Cow实现docker逃逸
https://www.anquanke.com/post/id/84866
【9】CertiKOS: Yale develops world’s first hacker-resistant operating system
【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)
【11】从技术角度剖析针对THE DAO的攻击手法
https://www.8btc.com/article/93713
https://github.com/kframework/evm-semantics
【13】风投巨头 A16Z 投资稳定币项目 MakerDAO
https://www.jinse.com/bitcoin/246582.html
【14】构造形式化证明，解决智能合约安全问题——你的合约亟待证明
https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg
【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP ’09).
