说说形式化验证（Formal Verification）吧

前言：被@暴走恭亲王点名，不得不写这个小文，笔者学识浅薄，而形式化验证这个题目不但大，而且深，笔者掌握的数学知识在专业人士里也就是幼儿园没毕业的水平，因此尽量不涉及任何数学问题，也欢迎真正的专家认真打脸。

作者：王健 达闼

说形式化验证（Formal Verification）之前，就不能不提一下形式化方法（Formal Method）。形式化方法简单的说就是用数学工具进行定义、开发和验证（specification, development and verification）。数学家们认为，不论硬件还是软件工程，就像世间万物一样，所有的学问一样，归根结底是数学问题。“一个不懂数学的工程师不是一个好工程师”。如果所有的设计开发都能够按照严格的数学方法进行，那么开发出来的系统就会像数学本身一样的完美：软件不会出错，硬件永远正常。当然，这是数学家的理想。

实际上，形式化方法是从硬件设计开始普及的，举一个例子：当年Intel的Pentium CPU浮点运算单元出错(FDIV Bug)，数以万计的CPU不得不回收和替换，给Intel造成了巨大损失(475M $)。

笔者按：小钱钱是推动社会进步的真正动力啊。

再按：IBM，AMD，ATMEL，STMicro等等半导体巨头也都是形式化方法的使用者…

从那之后，Intel开始在其芯片设计中广泛采用形式化方法。话说回来，软件方面的形式化方法进展如何呢？很不幸，软件行业对于形式化不太感冒。原因无非是如下几个：

a. 对数学技能的要求太高：域啊，格啊，建模啊，你的明白？（按：码农的数学水平看来是不入法眼啊）

b. 时间成本太高：先做纯数学的specification，然后需求一变，再来一次，互联网时代这个很致命啊，现在这个版本迭代的速度，文字上的spec有时候都是糊弄的c. 用户习惯：用户已经习惯了软件崩溃（码农的耻辱…）

好，啰嗦了这么久了，那么我们就往回拉拉，说说形式化验证（Formal Verification）。前面已经说了，形式化验证是形式化方法的重要组成部分。如果用形式化方法来做设计开发，必然涉及到形式化验证的问题。

在有了形式化的spec的情况下，那么可以Verification就大致可以分为“手算”和“机算”两种了（不要打我，高明的数学家的“手算”未必就比纯自动化的“机算”差）。举个例子，全自动化的Verification里面有一个叫做“Model Checking”的方法，简单的说就是穷举系统运行过程中所能达到的所有状态（States），这个如果建模，也就是写Spec的时候不是那么高明的话，嘿嘿嘿… 还有一个就是 “机器定理证明”，听起来很高大上，对不对？1954年，Martin Davis第一次用机器证明了一个定理：“两个偶数相加还是偶数”，不过在更早之前，图灵就已经通过一个著名的“停机问题”证明了图灵完备的机器的不可解问题。

好吧，似乎又扯远了，再拉回来。如果一个系统的开发不是形式化方法的，咋办？还能做形式化验证么？比如说给定代码，然后直接做形式化验证？

答案是“uncomputable”，呵呵，开个玩笑。其实道理上来讲很简单，就是你把没有做的Formal Specification补上就行了。当然，说着容易做着可就难了。从代码里面直接转换为形式化描述语言的工具有，但是别忘了specification是对功能，对需求的描述。直接转换的描述语言不是人类能够理解的，如果这个specification你都不知道它到底定义了什么，那么所谓的验证就没有任何意义了，于是“然并卵”了。

那么怎么办呢？ 老老实实的建模吧，从需求出发，从头开始。需求的specification做好了，证明代码和需求（的形式化描述）是（数学）等价的就是形式化验证。建模是个手艺活，如果完全从需求出发，那么恭喜你，你可以完整的跑一遍形式化方法的开发流程了，代码慢慢重构去吧… 当然，比较聪明的方法是从代码出发，手动建模，兼顾需求和实际的实现，尽量避免对代码的重构。

这个“聪明”的办法看起来是唯一可行的，但有两个缺点

对人的素质要求太高了，既要熟悉代码，又要熟悉形式化方法。时间成本随着代码量的增加达到了不可接受的程度，可以类比正向和逆向的开发。

现阶段对于软件的形式化验证多集中在几个微内核的OS上（如OKL4），也仅仅是对微内核那区区数千行代码的验证。这里再扯两句，微内核顾名思义就是最简单的，构成一个操作系统的要素都有了的内核，一切从简的目的就在于保证其安全性和稳定性。如果有人说他准备对某个宏内核系统（比如Linux）进行形式化验证，那么他一定不懂形式化验证…

好吧，代码层面的形式化验证做完了，那么是不是就万无一失了呢？且不说形式化验证的结果只是验证了系统“are we building the system right”，我们不能忘记编译器啊，还有runtime呢？前文提到了，Ada这个语言的编译器是形式化方法做的，就是为了保证其稳定性和安全性，加上执行环境呢？执行环境（比如OS）有没有做形式化验证啊？那么有同学问了，你这样是不是有点变态？我的回答是，有现成的例子，比如大家熟悉的智能卡，其硬件和OS（Firmware）均是通过形式化方法开发的，所有的API和Protocol均有形式化验证背书，所以，涉及到小钱钱的事情，大家是真的不含糊的。

扯了这么多，其实起因是因为有人要对以太坊（Ethereum）的EVM做形式化验证。EVM（Ethereum Virtual Machine）其实是一个很好的，好的不能再好的理想化目标，其功能需求明确，实现简单，而且最重要的，也是涉及小钱钱的事情。这里大胆的想一下，有人能够按照智能卡的方案，从硬件（比如说ASIC）到OS（比如专用micro kernel），再到EVM，做一个完整的基于形式化方法开发的产品，那就完美了。

最后扯一下Verification和Testing的关系。形式化验证是验证系统是否正确（are we building the system right），这个就很了不起了，完美，但是成本（金钱、人力和时间）太高。而testing就像穷人的“verification”，对人的技能要求低，时间成本也低，但是只能找到存在的问题，不能找到所有问题（vs. Formal Verification）。但从另一个层面来说，测试是在“真实”环境里进行的，形式化验证只是数学层面。在“真实”环境中的测试是形式化验证无法取代的，除非“真实”的环境本身也是形式化验证过的…

嗯，世界大同，数学家赢了…

作者：王健 达闼 | 来源：Chainb