说说形式化验证(Formal Verification)吧

Unknown view 49 2016-9-1 06:12
share to
Scan QR code with WeChat

说说形式化验证(Formal Verification)吧 (1)

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

作者:王健 达闼

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

说说形式化验证(Formal Verification)吧 (2)

实际上,形式化方法是从硬件设计开始普及的,举一个例子:当年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做好了,证明代码和需求(的形式化描述)是(数学)等价的就是形式化验证。建模是个手艺活,如果完全从需求出发,那么恭喜你,你可以完整的跑一遍形式化方法的开发流程了,代码慢慢重构去吧… 当然,比较聪明的方法是从代码出发,手动建模,兼顾需求和实际的实现,尽量避免对代码的重构。

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

说说形式化验证(Formal Verification)吧 (3)

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

现阶段对于软件的形式化验证多集中在几个微内核的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

btcfans公众号

Scan QR code with WeChat

From the Internet
Disclaimer:

Previous: 结算币USC关乎银行自身利益 Next: Coinfirm和Billon展开合作,提供区块链和数字货币交易解决方案

Related