科銀京城朱明遠(yuǎn)的發(fā)言題目為《工程實(shí)踐中的形式化方法——一個(gè)操作系統(tǒng)內(nèi)核VMK的形式開(kāi)發(fā)》。朱明遠(yuǎn)從安全和可靠性角度闡述了嵌入式操作系統(tǒng)的現(xiàn)狀，分析了一種基于形式化驗(yàn)證方式的嵌入式操作系統(tǒng)的實(shí)踐。
     

     
                   朱明遠(yuǎn) 北京科銀京成技術(shù)有限公司

      以下是文字實(shí)錄。

      我這個(gè)ppt是英文的，兩個(gè)禮拜以前，軟件所搞了國(guó)際的一個(gè)研討會(huì)，我過(guò)去講演就準(zhǔn)備了這樣一個(gè)稿子。我實(shí)在沒(méi)時(shí)間寫(xiě)新的稿子了，就使用這個(gè)吧。

      我的題目反應(yīng)了我們這一兩年的工程實(shí)踐，所以我把它叫做formal method is working，我估計(jì)在這個(gè)方向上研究差不多有20年了，但是在這個(gè)領(lǐng)域，好像大家都不知道你在干啥，忙啥呢，做的東西沒(méi)有人有強(qiáng)烈反應(yīng)，直到這幾年才在工業(yè)上，特別是航空工業(yè)上有了很多應(yīng)用，軟件系統(tǒng)，特別是操作系統(tǒng)可靠性，這樣提出了非常挑戰(zhàn)性的對(duì)我們的要求，反應(yīng)了我們這個(gè)方向上的工作。

      這個(gè)構(gòu)成就從這個(gè)開(kāi)始，我找到了McCarthy的一段話，McCarthy說(shuō)現(xiàn)在編程用debug，未來(lái)編程序則不使用，應(yīng)該去證明它滿足specifications，而且這個(gè)證明應(yīng)該可以由一個(gè)Computer program（程序）來(lái)check。這個(gè)理想或者dream，實(shí)際上我們?cè)诼龑?shí)現(xiàn)它，這個(gè)差不多有40年了，這是我們?cè)谧鲞@些事上，要回答的一些問(wèn)題，特別是操作系統(tǒng)的一些基本問(wèn)題，操作系統(tǒng)最基本的問(wèn)題其實(shí)應(yīng)該是可靠性和效率，操作系統(tǒng)圍繞的工作其實(shí)就是做這兩件事情，包括windows打補(bǔ)丁，也是說(shuō)明不夠可靠，補(bǔ)丁就是希望能夠更結(jié)實(shí)一點(diǎn)，但是實(shí)際結(jié)果可能越來(lái)越不結(jié)實(shí)了。

      這是我們碰到的基本問(wèn)題，特別是搞操作系統(tǒng)的問(wèn)題，為什么軟件總是不正確的？更細(xì)一點(diǎn)，就是為什么多數(shù)商業(yè)操作系統(tǒng)總有不正確的？和怎么樣寫(xiě)一個(gè)正確的程序？用debugging也好，用testing也好，或者用其他的方法。我們按照可靠性或者正確性給操作系統(tǒng)分分類(lèi)，實(shí)際上有這幾種：一種是the market proven operating system市場(chǎng)常見(jiàn)操作系統(tǒng)，就是不管好不好，反正我已經(jīng)賣(mài)了很多年了，像windows，已經(jīng)十幾年了，現(xiàn)在還是用著，市場(chǎng)證明了的操作系統(tǒng)；還有一種是certificated的操作系統(tǒng)，通過(guò)一些certificate組織或者office來(lái)驗(yàn)證操作系統(tǒng)的可靠性，包括瑞典的OSE，Green hill integrity 178B等；還有一個(gè)就是我們現(xiàn)在要做的，國(guó)際上工業(yè)界上已經(jīng)開(kāi)始在做provably correct operating system，就是說(shuō)通過(guò)一些形式化方法，在系統(tǒng)開(kāi)發(fā)的時(shí)候，就做驗(yàn)證。

      我們通過(guò)這幾年的實(shí)踐，感覺(jué)到，第一嵌入式實(shí)時(shí)操作系統(tǒng)很重要，其實(shí)硬件以上就是它了，只要一上電，操作系統(tǒng)就跑起來(lái)了，所以操作系統(tǒng)永遠(yuǎn)是個(gè)在底層，只要有軟件在運(yùn)行，操作系統(tǒng)肯定在跑；

      第二條，操作系統(tǒng)內(nèi)核比較小，所以我們有能力或者時(shí)間能夠把它整個(gè)形狀方法去Polish一遍的。現(xiàn)在美國(guó)有兩個(gè)對(duì)于軟件Assurance系統(tǒng)認(rèn)證的這種方式，一個(gè)就是大家都知道的航空系統(tǒng)使用DO-178B，它是按照軟件發(fā)生故障以后所產(chǎn)生的結(jié)果災(zāi)難程度來(lái)分析的，分為ABCDE五個(gè)等級(jí)，最高級(jí)就是如果軟件出現(xiàn)故障可能會(huì)造成生命損失，最低級(jí)的可能就是可以重啟，或者產(chǎn)生點(diǎn)小毛病，你不理會(huì)也沒(méi)有關(guān)系；還有一個(gè)就是common criteria evaluation assurance level，這個(gè)是分為7級(jí)，這個(gè)是從方法學(xué)的角度去考證這個(gè)軟件的級(jí)別，最高級(jí)別是7級(jí)，所有的從設(shè)計(jì)就開(kāi)始formally verified，最低級(jí)是functionally tested，這是7個(gè)級(jí)別的情況。第七級(jí)前三個(gè)階段是formal，LLD（low-level design）可以是semiformal，到implementation可以是informal，當(dāng)然最極端化，這五個(gè)步驟都可以是formal，就是整個(gè)都是用formal verified整一遍。[page]

      我們近來(lái)做的工作就是我們搞的操作系統(tǒng)內(nèi)核有點(diǎn)像韓青剛才講到的hypervisor的那種體系結(jié)構(gòu)的操作系統(tǒng)，在一個(gè)處理器內(nèi)核上通過(guò)虛擬的辦法支持幾個(gè)不同的操作系統(tǒng)的這樣的運(yùn)行環(huán)境，形狀方法使用過(guò)去我在研究所的時(shí)候，搞過(guò)的一個(gè)定理證明系統(tǒng)，這個(gè)系統(tǒng)我們一直用著，差不多有20年了?；镜姆椒ň褪沁@樣。

      建立一個(gè)model，然后translation成一個(gè)specification in powerEpsilon，根據(jù)model定義一些性質(zhì)，這些性質(zhì)實(shí)際上要通過(guò)定理證明系統(tǒng)證明產(chǎn)生一些結(jié)果，我在此就不詳細(xì)講解了。這是自然數(shù)歸納法的一個(gè)描述，證明specification實(shí)際上是一個(gè)過(guò)程，從最初的specification通過(guò)refinement到一個(gè)細(xì)的specification，證明整個(gè)系統(tǒng)比較復(fù)雜在于先用一個(gè)語(yǔ)言來(lái)描述一個(gè)操作系統(tǒng)，然后可能定義一個(gè)比較小的語(yǔ)言，必要時(shí)是一個(gè)完整的C語(yǔ)言，可能和C語(yǔ)言有點(diǎn)關(guān)系，這要建立起來(lái)，然后還要定義一個(gè)虛擬的machine或者TM codes，要描述一個(gè)VIE，最后完成specification應(yīng)該使用C語(yǔ)言和匯編語(yǔ)言寫(xiě)的一段編譯成X86 codes，這都要做verification。

      從操作系統(tǒng)的定義開(kāi)始，到機(jī)器上可以跑的東西，這個(gè)產(chǎn)生很大的工作量，基本上語(yǔ)言的描述、語(yǔ)言的語(yǔ)義定義、目標(biāo)機(jī)的定義、目標(biāo)機(jī)的語(yǔ)義定義，然后compiler之間的語(yǔ)義的準(zhǔn)確性，所有的東西都要描述，所以看起來(lái)不是特別復(fù)雜，但是工作量很大，由于時(shí)間的關(guān)系，我就稍微講一下。比較難的是，我們做的兩個(gè)東西，第一個(gè)是VMK虛擬化以后產(chǎn)生不同的partition，partition之后要證明是在這種體系結(jié)構(gòu)上通過(guò)硬件的一些支持以后得到的separation，一個(gè)操作系統(tǒng)的應(yīng)用如果產(chǎn)生故障，不影響其他操作系統(tǒng)，所以這叫做separation kernel theorem，主要來(lái)證明一個(gè)操作系統(tǒng)，虛擬系統(tǒng)里的一個(gè)應(yīng)用時(shí)如何產(chǎn)生的，一個(gè)故障只會(huì)影響到本身的這個(gè)separation、這個(gè)分區(qū)的狀態(tài)，而不會(huì)影響到其他分區(qū)，這個(gè)就是separation kernel定理，這是整個(gè)定理的一個(gè)證明。

      證明實(shí)際上挺簡(jiǎn)單的，機(jī)器可以check的一個(gè)定理，和編程序一樣，你寫(xiě)一段程序，機(jī)器可以自動(dòng)check，基本上就是這樣。實(shí)際上最難的不是這一點(diǎn)，最難的是操作系統(tǒng)有高層的東西，也有底層的東西，底層的東西就是你要描述的東西，因?yàn)椴僮飨到y(tǒng)要處理中斷，你就要描述中斷，一描述中斷，可能就要涉及到虛擬機(jī)的概念，通過(guò)machine的描述來(lái)描述中斷，在高級(jí)語(yǔ)言這塊是沒(méi)法描述的，所以為什么要有虛擬機(jī)的概念，那么有虛擬機(jī)的概念就麻煩了，因?yàn)槟阋枋鯿ompiler，compiler涉及到高級(jí)語(yǔ)言的問(wèn)題，但是有了兩級(jí)虛擬機(jī)的定義以后，就可以描述semantic of context saving，上下文的切換也可以描述，這樣就把整個(gè)東西描述比較完整了。這是我們工作還沒(méi)做完，因?yàn)楣ぷ髁勘容^大，先把重要的給描述了，慢慢地再做細(xì)節(jié)的處理。

      國(guó)際上實(shí)際上從2000年以后，有幾個(gè)比較大的工作。一個(gè)就是Rockwell Collins AAMP7 separation kernel microcode，這是個(gè)硬件，支持CPU，他們自己設(shè)計(jì)的一個(gè)CPU，形式化的方法按照EAL7的級(jí)別去做認(rèn)證，基本上全部是形式化的方法進(jìn)行設(shè)計(jì)的；然后還和Green Hills另外一個(gè)搞操作系統(tǒng)integrity OS kernel，達(dá)到EAL6+的級(jí)別；還有一個(gè)是Java虛擬機(jī)的工作。

      還是回到我們當(dāng)初談到的dream，實(shí)際上Computer Science，軟件工程，Tony Hoare 07年說(shuō)到，我們做的工作圍繞zero defect program，就是零缺陷程序，大家的目標(biāo)就是做到零缺陷的程序，編的程序一點(diǎn)缺陷都沒(méi)有。還有一些impossible，像物理中的測(cè)量的精度，根據(jù)測(cè)不準(zhǔn)原理是永遠(yuǎn)測(cè)不準(zhǔn)的，物理上有這么個(gè)缺陷，大家在追求物理上越來(lái)越精確，但絕對(duì)精確是達(dá)不到的；化學(xué)上就是材料的純度，要做到純度100%是不可能的。我們這些人每天忙活的就是這些。但是他還有個(gè)dream is possible，通過(guò)工作上的努力，實(shí)現(xiàn)不是zero defect program，而是zero defect programming，就是通過(guò)一些方法來(lái)實(shí)現(xiàn)你的夢(mèng)想，通過(guò)形式化的方法，來(lái)逐漸逼近，defect越來(lái)越少，越來(lái)越極限。

      基本上我的發(fā)言就這些，謝謝。

      （感謝嵌入式系統(tǒng)聯(lián)誼會(huì)提供本次文字實(shí)錄，相關(guān)PPT下載請(qǐng)?jiān)L問(wèn)：http://www.esbf.org.cn/img/0906zmy.pdf）