朱明远：工程实践中的形式化方法

      科银京城朱明远的发言题目为《工程实践中的形式化方法——一个操作系统内核VMK的形式开发》。朱明远从安全和可靠性角度阐述了嵌入式操作系统的现状，分析了一种基于形式化验证方式的嵌入式操作系统的实践。
     

     
                   朱明远 北京科银京成技术有限公司

      以下是文字实录。

      我这个ppt是英文的，两个礼拜以前，软件所搞了国际的一个研讨会，我过去讲演就准备了这样一个稿子。我实在没时间写新的稿子了，就使用这个吧。

      我的题目反应了我们这一两年的工程实践，所以我把它叫做formal method is working，我估计在这个方向上研究差不多有20年了，但是在这个领域，好像大家都不知道你在干啥，忙啥呢，做的东西没有人有强烈反应，直到这几年才在工业上，特别是航空工业上有了很多应用，软件系统，特别是操作系统可靠性，这样提出了非常挑战性的对我们的要求，反应了我们这个方向上的工作。

      这个构成就从这个开始，我找到了McCarthy的一段话，McCarthy说现在编程用debug，未来编程序则不使用，应该去证明它满足specifications，而且这个证明应该可以由一个Computer program（程序）来check。这个理想或者dream，实际上我们在慢慢实现它，这个差不多有40年了，这是我们在做这些事上，要回答的一些问题，特别是操作系统的一些基本问题，操作系统最基本的问题其实应该是可靠性和效率，操作系统围绕的工作其实就是做这两件事情，包括windows打补丁，也是说明不够可靠，补丁就是希望能够更结实一点，但是实际结果可能越来越不结实了。

      这是我们碰到的基本问题，特别是搞操作系统的问题，为什么软件总是不正确的？更细一点，就是为什么多数商业操作系统总有不正确的？和怎么样写一个正确的程序？用debugging也好，用testing也好，或者用其他的方法。我们按照可靠性或者正确性给操作系统分分类，实际上有这几种：一种是the market proven operating system市场常见操作系统，就是不管好不好，反正我已经卖了很多年了，像windows，已经十几年了，现在还是用着，市场证明了的操作系统；还有一种是certificated的操作系统，通过一些certificate组织或者office来验证操作系统的可靠性，包括瑞典的OSE，Green hill integrity 178B等；还有一个就是我们现在要做的，国际上工业界上已经开始在做provably correct operating system，就是说通过一些形式化方法，在系统开发的时候，就做验证。

      我们通过这几年的实践，感觉到，第一嵌入式实时操作系统很重要，其实硬件以上就是它了，只要一上电，操作系统就跑起来了，所以操作系统永远是个在底层，只要有软件在运行，操作系统肯定在跑；

      第二条，操作系统内核比较小，所以我们有能力或者时间能够把它整个形状方法去Polish一遍的。现在美国有两个对于软件Assurance系统认证的这种方式，一个就是大家都知道的航空系统使用DO-178B，它是按照软件发生故障以后所产生的结果灾难程度来分析的，分为ABCDE五个等级，最高级就是如果软件出现故障可能会造成生命损失，最低级的可能就是可以重启，或者产生点小毛病，你不理会也没有关系；还有一个就是common criteria evaluation assurance level，这个是分为7级，这个是从方法学的角度去考证这个软件的级别，最高级别是7级，所有的从设计就开始formally verified，最低级是functionally tested，这是7个级别的情况。第七级前三个阶段是formal，LLD（low-level design）可以是semiformal，到implementation可以是informal，当然最极端化，这五个步骤都可以是formal，就是整个都是用formal verified整一遍。[page]

      我们近来做的工作就是我们搞的操作系统内核有点像韩青刚才讲到的hypervisor的那种体系结构的操作系统，在一个处理器内核上通过虚拟的办法支持几个不同的操作系统的这样的运行环境，形状方法使用过去我在研究所的时候，搞过的一个定理证明系统，这个系统我们一直用着，差不多有20年了。基本的方法就是这样。

      建立一个model，然后translation成一个specification in powerEpsilon，根据model定义一些性质，这些性质实际上要通过定理证明系统证明产生一些结果，我在此就不详细讲解了。这是自然数归纳法的一个描述，证明specification实际上是一个过程，从最初的specification通过refinement到一个细的specification，证明整个系统比较复杂在于先用一个语言来描述一个操作系统，然后可能定义一个比较小的语言，必要时是一个完整的C语言，可能和C语言有点关系，这要建立起来，然后还要定义一个虚拟的machine或者TM codes，要描述一个VIE，最后完成specification应该使用C语言和汇编语言写的一段编译成X86 codes，这都要做verification。

      从操作系统的定义开始，到机器上可以跑的东西，这个产生很大的工作量，基本上语言的描述、语言的语义定义、目标机的定义、目标机的语义定义，然后compiler之间的语义的准确性，所有的东西都要描述，所以看起来不是特别复杂，但是工作量很大，由于时间的关系，我就稍微讲一下。比较难的是，我们做的两个东西，第一个是VMK虚拟化以后产生不同的partition，partition之后要证明是在这种体系结构上通过硬件的一些支持以后得到的separation，一个操作系统的应用如果产生故障，不影响其他操作系统，所以这叫做separation kernel theorem，主要来证明一个操作系统，虚拟系统里的一个应用时如何产生的，一个故障只会影响到本身的这个separation、这个分区的状态，而不会影响到其他分区，这个就是separation kernel定理，这是整个定理的一个证明。

      证明实际上挺简单的，机器可以check的一个定理，和编程序一样，你写一段程序，机器可以自动check，基本上就是这样。实际上最难的不是这一点，最难的是操作系统有高层的东西，也有底层的东西，底层的东西就是你要描述的东西，因为操作系统要处理中断，你就要描述中断，一描述中断，可能就要涉及到虚拟机的概念，通过machine的描述来描述中断，在高级语言这块是没法描述的，所以为什么要有虚拟机的概念，那么有虚拟机的概念就麻烦了，因为你要描述compiler，compiler涉及到高级语言的问题，但是有了两级虚拟机的定义以后，就可以描述semantic of context saving，上下文的切换也可以描述，这样就把整个东西描述比较完整了。这是我们工作还没做完，因为工作量比较大，先把重要的给描述了，慢慢地再做细节的处理。

      国际上实际上从2000年以后，有几个比较大的工作。一个就是Rockwell Collins AAMP7 separation kernel microcode，这是个硬件，支持CPU，他们自己设计的一个CPU，形式化的方法按照EAL7的级别去做认证，基本上全部是形式化的方法进行设计的；然后还和Green Hills另外一个搞操作系统integrity OS kernel，达到EAL6+的级别；还有一个是Java虚拟机的工作。

      还是回到我们当初谈到的dream，实际上Computer Science，软件工程，Tony Hoare 07年说到，我们做的工作围绕zero defect program，就是零缺陷程序，大家的目标就是做到零缺陷的程序，编的程序一点缺陷都没有。还有一些impossible，像物理中的测量的精度，根据测不准原理是永远测不准的，物理上有这么个缺陷，大家在追求物理上越来越精确，但绝对精确是达不到的；化学上就是材料的纯度，要做到纯度100%是不可能的。我们这些人每天忙活的就是这些。但是他还有个dream is possible，通过工作上的努力，实现不是zero defect program，而是zero defect programming，就是通过一些方法来实现你的梦想，通过形式化的方法，来逐渐逼近，defect越来越少，越来越极限。

      基本上我的发言就这些，谢谢。

      （感谢嵌入式系统联谊会提供本次文字实录，相关PPT下载请访问：http://www.esbf.org.cn/img/0906zmy.pdf）