形式化方法对软件开发的挑战:历史与发展



  • 作者:裘宗燕,北京大学教授,中国计算机学会杰出会员

    几年前到某著名大学参加学术活动,无意中听到该校两位老师闲聊,现在还记得的一句话就是“形式化方法已经不行了”。看来真是隔行如隔山,评价自己不熟悉的领域,而且随便说,难免出错。在对形式化方法了解的更多的人们看来,它不仅没有“不行”,近年还发展得挺迅猛。只不过,形式化方法也就是是做软件或者硬件,不做什么新东西,不太会像近来热炒的云计算、大数据、人工智能那样,被疯狂追捧。

    目前,计算机领域、以及软件业的许多人对形式化方法的了解还停留在上个世纪。为了交流情况,我们想在这里介绍一些事例,说明形式化方法已经取得了真正的进展,正在被人们用来解决软件开发中一直没有解决的问题,也实际开发出一些重要的系统或系统部件。

    较早开展的与实际软件开发有关的形式化工作是证明程序正确性,相关工作多以论文形式发表,其内容是证明了一些小程序或算法(抽象程序)的正确性。研究者们也试图用同样方法去证明复杂程序,但是,随着程序的结构和设计更复杂后,工作难度飞速增长,有关证明最终无法完成。由于这些情况,这方面的工作被人诟病为“只能对付小程序”,没用。

    一些研究者想到,证明已有的程序很难,如果是自己构造具有所需功能的正确程序(或软件),更多方面可以控制,可能反而更实用。根据这种想法,人们提出了采用某种构造与证明并进的方式,目标是做出“构造即正确”的程序(或软件)。最早提出这样想法的人可能是Dijkstra,其著名的A Discipline of Programming给出了许多严格推导的程序。随后又出现了一些相关的论文和著作,如The Science of Programming、Programming from Specification等。这些工作流行于上世纪80-90年代,由一批著名计算机科学家推动。但是,这类方法同样未受到软件领域的重视,主要批评还是说只能做“玩具程序”。

    用形式化技术开发实际系统的最早突破可能是法国Abrial的B方法。据Abrial自己说,他在牛津开发了Z语言后,觉得这种想法可以用于实际软件领域,回到法国后开发了B方法。B方法支持从系统的抽象规范描述到代码生成(生成C或Ada代码)的整个开发流程,现在已有工业级的开发工具(包括证明工具)。B方法的早期应用案例是开发了巴黎地铁的信号系统和一些控制系统,包括巴黎地铁14号线的自动驾驶系统等。据粗略统计,目前全世界有数十条地铁线路的自动驾驶系统是用B方法开发的。B方法也被应用到其他安全攸关领域,如铁路、汽车和航空等领域。用B开发生成的控制系统可能大到数十万行的目标代码。B方法也在西门子和阿尔斯通等公司里被广泛使用。据笔者从有关部门了解,在我国从欧洲引进的高铁系统和设备中,有一些软件也是用B方法开发的。Abrial曾在2006年国际软件大会(在上海召开)做过有关“形式化方法的工业应用”的特邀报告,其著作The B-Book介绍了B方法。Abrial与华东师大有长期合作,2016年被中国政府授予国际合作奖。Abrial曾告诉笔者,用B方法开发的(某个)系统在测试中没发现任何错误,长期运行中也没发现问题。对于常规的软件开发方法,这种情况大概是绝无可能的。

    形式化方法在系统软件领域也取得了许多成果。这方面的最重要成果之一是CompCert编译器。编译器显然是最重要的系统软件,正在各种计算机上运行的绝大多数程序都是由编译器生成的,如果编译器有错,后果可能很严重。但是,常用编译器都没经过验证,不能保证目标代码与源代码语义等价。2012年法国研究者发布了经过验证的优化编译器CompCert,之后继续完善和扩充,目前版本能处理ANSI C的几乎所有特征和一些C99扩充,能生成PowerPC、ARM和X86代码,支持64位系统结构、分别编译和连接,能生成DWARF调试信息和语法错误的解释等。CompCert基于计算机辅助证明系统Coq开发,严格证明了目标代码与源程序的等价性。在X. Yang等人的2011年发表的Finding and Understanding Bugs in C Compilers(PLDI)里报告了他们用6年时间检查各种在用编译器(包括VC、gcc等)错误的工作,只有CompCert验证过的部分没发现错误,其他编译器都发现了错误。

    近年的另一项有趣工作是2015年MIT学者开发的经过验证的文件系统FSCQ(SOSP'15)。FSCQ可以保证,在使用中的任何时候操作系统崩溃,重新boot时都FSCQ能正确恢复系统中的文件,不会丢失数据(称为crash safety)。常规文件系统无法提供这种保证。

    美国国防部的HACMS项目(High-Assurance Cyber Military Systems,高可信军事网络系统)的目标是开发高可信、黑客无法入侵的军用系统。该项目的一个成果是一个无人机控制系统,开发成功后组织黑客攻击,攻击者知道源码,并能访问系统的一些部分,目标是攻入系统的其他部分。攻击者工作了六周没有达到目的。这一系统的基础是经过形式化验证的OS内核seL4,整个系统在该内核上用Isabelle形式化工具开发和验证。HACMS项目的另一成果是邵中领导开发的操作系统内核CertiKOS(OSDI'16),它经过验证并支持多核CPU。

    显然,上述事例中的开发目标都是非常重要的软件,而且是很难做的软件。这些工作的完成,说明形式化方法确实能用于实际软件开发,而且能做出最高质量的软件系统。

    形式化开发的工作过程与常规软件开发有一些类似的地方。例如,B方法基于一阶逻辑和集合论,其开发过程从写出并证明一致的抽象高层规范开始,基于一种严格定义的精化(refinement)规则逐步扩展、填充和变形,最终做出所需要的经过严格验证的软件系统。软件领域有自上而下的开发方法,程序设计中有逐步求精方法,B方法中的精化可以看作是它们的严格化。上面提到的其他系统中有几个是用Coq辅助验证工具开发的,包括CompCert、FSCQ和CertiKOS。这些系统的开发工作基本上是一种自下而上的流程,逐个(逐层)构造所需软件概念和部件,最终得到整体的软件。其中CertiKOS的开发中还使用了CompCert,系统的大部分是经过验证的C代码,用CompCert编译到汇编。无论采用哪种方式,形式化开发的最关键特征就是开发与证明携手并进。

    特别值得提出,CertiKOS是一个操作系统内核体系结构,可用于开发实际的操作系统。报告这一工作的OSDI'16论文中特别提到一个基于CertiKOS开发的具体操作系统,其研发和验证仅用了两个人年,工作效率十分惊人。业界对形式化方法技术的另一重要质疑是开发代价太高。CertiKOS可以看作一个证据,说明实际情况可能不那么悲观。

    形式化开发的工作在国内也有许多工作。例如王生原领导的小组开发了从同步流语言Lustre到C语言的经过验证的编译器,通过CompCert接力就能生成可执行代码。Lustre是国际上控制系统开发领域使用很多的语言,特别是在核电领域应用广泛。上述工作成果已成为国内某核企的重要工具。此外,上海一些开发团队也在做轨道交通方面的应用系统的形式化开发。笔者没有下功夫去收集这方面信息,希望有关专家将来自己补充。

    当然,软件形式化开发技术和应用都还处在起步阶段,还有许多问题需要研究。例如,这里需要考虑的一个重要问题是正确性的组合和传播。复杂系统必然是一些部件的组合,部件可能是不同形式化开发方法的产物,即使每个部件都已经验证,如何模块化地验证由这些部分构造出来的系统仍然正确,还是一个问题。再如,作为与常规方式不同的软件质量保证手段,形式化方法怎样与常规开发方法协同工作?虽然如此,我们还是应该承认,形式化软件开发方法已经取得了实质性进展,并已开始在实际领域发挥作用了。

    可以认为,以B方法的成功应用,以及CompCert等重要系统的出现为标志,形式化软件开发方法已经真正进入了软件开发的实际领域。不难想象,今后我们一定会看到越来越多经过形式化验证的软件系统或部件,看到经过严格验证的程序库,也可能遇到某些用户要求系统必须经过形式化验证。另一方面,回顾各种重要的软件规范标准,其最高级别的质量保证都要求形式化方法的应用。当然,目前一般是作为可选要求,原因是人们在撰写标准时还缺乏实践基础。现在的情况不同了,这些标准的下一个版本会怎样变化?未来某些标准强制性地要求严格证明,不是不可能的事情。所有这些都要求我们及早做好准备。



  • 世界上最可靠的地铁是用形式化方法开发的,而且是一条无人驾驶线。安全运行18年没有发现任何bug,因此没有做过任何软件的升级。


Log in to reply
 

Looks like your connection to Asch was lost, please wait while we try to reconnect.