*耶魯大學(xué)邵中教授在CCF-GAIR 2017大會(huì)現(xiàn)場(chǎng)

雷鋒網(wǎng)按：2017年7月9日，中國(guó)計(jì)算機(jī)學(xué)會(huì)（CCF）主辦、雷鋒網(wǎng)與香港中文大學(xué)（深圳）承辦的第二屆全球人工智能與機(jī)器人峰會(huì)（CCF-GAIR 2017）進(jìn)入到最后一天的議程。自動(dòng)駕駛作為人工智能大潮中一個(gè)最重要的分支，在這天得到廣泛而深入的探討。

事實(shí)上，自動(dòng)駕駛的各個(gè)環(huán)節(jié)，都不得不面對(duì)網(wǎng)絡(luò)安全問(wèn)題。來(lái)自耶魯大學(xué)的邵中教授，作為計(jì)算機(jī)程序語(yǔ)言設(shè)計(jì)的權(quán)威專家受邀進(jìn)行了大會(huì)主題演講，為我們闡述了其正在研發(fā)的“反黑客攻擊”操作系統(tǒng)CertiKOS背后的理念。

1.

大家都知道，無(wú)論是區(qū)塊鏈、機(jī)器人還是自動(dòng)駕駛，其核心軟件都有一個(gè)操作系統(tǒng)，操作系統(tǒng)一旦被黑客攻擊，上層安全便得不到保證。所以自動(dòng)駕駛汽車的信息安全問(wèn)題是一個(gè)特別大的挑戰(zhàn)。

最近幾年，業(yè)內(nèi)發(fā)生了很多黑客攻擊汽車的案例，他們根本不需要靠近車輛，便可輕松獲取十英里外車輛的控制權(quán)。這些攻擊還不能很快修復(fù)，且每年都有發(fā)生。此外，勒索病毒、物聯(lián)網(wǎng)病毒等，一直困擾著那些聯(lián)網(wǎng)的設(shè)備，哪怕只是其中某一部件被攻擊，后果也不堪設(shè)想。

近來(lái)，紐約時(shí)報(bào)的一篇文章中提到，自動(dòng)駕駛系統(tǒng)比你見(jiàn)到的手機(jī)、電腦的系統(tǒng)更加復(fù)雜，其上的聯(lián)網(wǎng)接口數(shù)不勝數(shù)，一旦被攻擊，不是修復(fù)（reboot）一下就了事的，這輛車很可能變成黑客的武器，危及公眾安全。

2.

為了從底層來(lái)解決這些問(wèn)題，邵中帶領(lǐng)耶魯大學(xué)的團(tuán)隊(duì)開(kāi)啟了研發(fā)項(xiàng)目，重新設(shè)計(jì)操作系統(tǒng)——黑客無(wú)法進(jìn)行攻擊。

目前，一般的軟件出了錯(cuò)，都是用Test的方式來(lái)找到Bug的位置，了解其在特定的執(zhí)行狀態(tài)和攻擊下會(huì)有什么狀況。如果要解決Bug就不能用Test，唯一能做的就是形式化驗(yàn)證。那么，如何能夠用Formal Methods（形式化方法）來(lái)驗(yàn)證新的不帶Bug的操作系統(tǒng)？

所謂Formal Methods，就跟中學(xué)里的數(shù)學(xué)證明一樣，一個(gè)簡(jiǎn)單的數(shù)學(xué)定理要花一頁(yè)紙，要驗(yàn)證它有什么樣的可能性，會(huì)不會(huì)成功。但是不管它能不能做到，形式化驗(yàn)證要證明這個(gè)程序滿足它的規(guī)范，而且是在任何執(zhí)行條件下，面對(duì)某一類攻擊時(shí)都不會(huì)有錯(cuò)，這是形式化驗(yàn)證要達(dá)到的效果。

形式化驗(yàn)證為什么到現(xiàn)在還沒(méi)有成功應(yīng)用到商業(yè)的各個(gè)部門呢？原因主要有這么幾類。

第一，寫證明要有形式化支持，比如下圖是在2009年操作系統(tǒng)大會(huì)上，第一個(gè)被驗(yàn)證的操作系統(tǒng)內(nèi)核。有7500行代碼，但是光7500行的C語(yǔ)言代碼就花了11個(gè)人年為其工作，其中還有500行的匯編代碼1000多行的C語(yǔ)言代碼沒(méi)有被驗(yàn)證，可以看出工作量非常大。

另外一個(gè)問(wèn)題是，用戶平時(shí)寫C語(yǔ)言代碼的時(shí)候，究竟對(duì)它有多清晰的概念？C語(yǔ)言也不是特別好的語(yǔ)言，一旦要用它來(lái)寫操作系統(tǒng)最底端的東西，可能就會(huì)出現(xiàn)C語(yǔ)言代碼、匯編代碼以及C語(yǔ)言代碼和匯編代碼雜交體并存的情況，依賴性很強(qiáng)，一旦這些代碼連在一起組成一個(gè)復(fù)雜的系統(tǒng)，要保證其不出錯(cuò)簡(jiǎn)直是不可能完成的任務(wù)。

除了這個(gè)問(wèn)題以外，所有的操作系統(tǒng)，尤其是現(xiàn)在新的多核的CPU平臺(tái)上，還有用Concurrency（并發(fā)）的，往往有好幾個(gè)版本，要驗(yàn)證它也非常難。

所以，現(xiàn)在的系統(tǒng)能做到的程度與理想狀態(tài)還有一個(gè)很大的Gap，像IoT、自動(dòng)駕駛平臺(tái)這類系統(tǒng)會(huì)變得越來(lái)越復(fù)雜，所以Gap會(huì)越拉越大。

3.

我們要做的這個(gè)系統(tǒng)就是要解決以上所有這些挑戰(zhàn)，我們所采用的技術(shù)是Certified Abstraction Layers。

Certified Abstraction Layers這個(gè)技術(shù)不只是用于現(xiàn)有的系統(tǒng)，而且還作為一種新的技術(shù)來(lái)開(kāi)發(fā)新的系統(tǒng)，目的就是要讓Gap變得越來(lái)越小。

怎么做到呢？我們會(huì)有一個(gè)個(gè)模塊，每一個(gè)小的模塊想象成一個(gè)代碼，每個(gè)軟件模塊寫的時(shí)候總會(huì)實(shí)現(xiàn)一些新的功能，所以有了M1，每一個(gè)被驗(yàn)證的模塊就叫Certified Abstraction Layers，這中間會(huì)有一個(gè)模擬的關(guān)系，如果都是在一個(gè)抽象層上建立的話，就可以把它們并成一塊。

如果這些代碼是運(yùn)用C語(yǔ)言寫的，已經(jīng)被驗(yàn)證滿足這些規(guī)范的話，可以把它用編譯器編譯以后生成匯編代碼，這些匯編代碼也是完全被驗(yàn)證的，因?yàn)檫@個(gè)編譯器能保證生成的代碼和原代碼之間是完全一致的。這樣就能組成一個(gè)大的系統(tǒng)，用模塊化的方式將其組成一個(gè)大的系統(tǒng)。

我們這個(gè)課題在2、3年前做的，加了支持中斷，用在車上可以保證車?yán)锩娴牟考ハ嗖皇苡绊?。最近我們做的是并發(fā)的內(nèi)核，可以在多核上運(yùn)行，每個(gè)核上都可以跑一個(gè)Linux系統(tǒng)。所以我們能證明的不只是功能性，還可以證明它不會(huì)“死”，所有普通意義上黑客能攻擊的模塊都會(huì)被去掉。

整個(gè)證明都是通過(guò)Coq Proof Assistant來(lái)進(jìn)行，該工具在2014年還獲得了（ACM Software System Award）獎(jiǎng)項(xiàng)。

在具體應(yīng)用上，CertiKOS可以用在機(jī)器人及智能系統(tǒng)上，也可以運(yùn)用在無(wú)人機(jī)上，好處就是能保證操作系統(tǒng)內(nèi)核里沒(méi)有任何可被黑客攻擊的模塊。

4.

接下來(lái)會(huì)介紹如果要建立這樣一個(gè)被驗(yàn)證可信的操作系統(tǒng)的一些具體技術(shù)。

我用比較小的一個(gè)操作系統(tǒng)來(lái)給你們看一個(gè)例子，如果說(shuō)是在并發(fā)系統(tǒng)上，會(huì)有一些Spin-lock Module，上面會(huì)支持一些Thread Queue，很可能上面會(huì)加一些Scheduling Module、Inter-Process Communication和Keyboard Driver等，這是一個(gè)操作系統(tǒng)怎么從底層往上搭建的方式。

其中用到的最主要的技術(shù)是Certified Abstraction Layers，就是說(shuō)把所有的程序的模塊分成一塊塊，稱為Certified Objects，一個(gè)Object就代表每一個(gè)模塊對(duì)外能做什么事情。而且，代碼和模塊遵循的規(guī)范是完全一致的，這樣的做法就是讓每個(gè)模塊都有一個(gè)抽象狀態(tài)（Abstract State）和模塊能做的基類型操作（Primitives）。

所以，你每次寫任何一個(gè)軟件模塊的時(shí)候，都會(huì)在一個(gè)抽象層上做，會(huì)使用一些內(nèi)層。如果你要驗(yàn)證這個(gè)模塊，就要在上面寫它的規(guī)范，你要驗(yàn)證的目標(biāo)就是要保證實(shí)現(xiàn)C代碼和寫的形式化模塊之間的關(guān)系。

比如說(shuō)上圖顯示的是C語(yǔ)言代碼中定義的Queue，這是它用的內(nèi)層，這個(gè)C語(yǔ)言代碼事實(shí)上是拿它來(lái)做雙向鏈表，用于實(shí)現(xiàn)一個(gè)隊(duì)列，中間還有一個(gè)State，上面還有一個(gè)head和tail，這樣做了之后你可能用其寫一些C語(yǔ)言代碼。

如果要保證這個(gè)代碼不會(huì)出錯(cuò)，你就得保證其與它上面的規(guī)范是一致的。

事實(shí)上這是我們所有寫程序用的最多的辦法，因?yàn)槟銈兤綍r(shí)寫每一行程序的時(shí)候，腦袋里都有一個(gè)自己想要實(shí)現(xiàn)的東西，所以復(fù)雜的系統(tǒng)其實(shí)都是在搭一層層的抽象層。構(gòu)建一個(gè)復(fù)雜的無(wú)人駕駛的汽車，也需要有很多抽象層，只不過(guò)是現(xiàn)在我們關(guān)注的是在最底層的操作系統(tǒng)的安全。

如果抽象規(guī)范寫成這樣，從隊(duì)列上拿下一個(gè)元素就非常簡(jiǎn)單，你要保證C代碼和函數(shù)的規(guī)范是具備一致性的，我從隊(duì)列里拿掉一個(gè)元素，C語(yǔ)言就要跑好幾步，但是你能保證兩者之間是一致的。這樣的證明就表示你做了一個(gè)Simulation Proof（模擬驗(yàn)證），能保證你寫的代碼和形式規(guī)范之間沒(méi)有任何Gap，那么黑客就無(wú)法攻擊系統(tǒng)。

有了這套名為Deep Specification的形式規(guī)范，就可以保證你在程序里觀察到的行為都能在規(guī)范中表達(dá)出來(lái)。有了它以后，我們能夠保證所有想要證明的Property（屬性）都可以在規(guī)范上提煉出來(lái)，便可以做一些操作系統(tǒng)的內(nèi)核驗(yàn)證。

如上圖所示，如果內(nèi)核代碼是這樣的，很可能大部分代碼會(huì)包括內(nèi)存管理、線程管理、進(jìn)程管理，還有上層的Trap。

如果先把內(nèi)存管理的模塊拿出來(lái)，把它分好層，所謂分層就是保證每一層都只依賴底層，把每一個(gè)模塊都驗(yàn)證了進(jìn)而并成一個(gè)。這個(gè)方式也適合用來(lái)驗(yàn)證線程管理模塊、進(jìn)程管理模塊、虛擬內(nèi)存模塊等。有了這些模塊，我們就可以搭建一個(gè)Certified Sequencial kernel。

如果你又要在上面加Hypervisor的功能，比如說(shuō)虛擬化的模塊，那么你只需要做的就是在硬件端有一個(gè)支持虛擬化的模塊，把硬件的功能體現(xiàn)出來(lái)。往上再提升到進(jìn)程管理，從那個(gè)地方就可以開(kāi)始來(lái)驗(yàn)證虛擬化模塊用來(lái)實(shí)現(xiàn)Hypervisor。這個(gè)驗(yàn)證以后，就可以得到一個(gè)Certified Hypervisor，在上面就可以Boot Linux，而且是多個(gè)版本的Linux。

有了這個(gè)以后，我們就能把多行代碼之間每一塊的關(guān)系都搞得非常透徹，比如此前提到的3000行代碼就可以轉(zhuǎn)變成37層的抽象層，這些抽象層都是邏輯上的抽象層，所以它真正實(shí)現(xiàn)的速度和功能跟原來(lái)是一樣的，用這些抽象層可以把中間各種各樣的關(guān)系理順，保證不會(huì)出任何的錯(cuò)誤。

在這個(gè)基礎(chǔ)上，我們還可以拿它來(lái)實(shí)現(xiàn)一些并發(fā)的Kernel。大家都知道，未來(lái)所有的自動(dòng)駕駛汽車上用的芯片越來(lái)越多的應(yīng)該是MPSOC，這些多核的CPU帶來(lái)了很多同步的問(wèn)題，所有的人都知道并發(fā)程序是現(xiàn)在寫程序最大的挑戰(zhàn)，如果這個(gè)問(wèn)題不解決，接下來(lái)整個(gè)自動(dòng)駕駛汽車、無(wú)人機(jī)都會(huì)有很大的局限性。

所以我們現(xiàn)在也做多核內(nèi)核的驗(yàn)證。多核內(nèi)核的驗(yàn)證跟剛才用的技術(shù)是類似的，我們做的是能夠讓你把用在串行系統(tǒng)上的驗(yàn)證方法運(yùn)用到了多核上，我們把多核的機(jī)器變得如串型一樣，只不過(guò)把其他的CPU變成了它的環(huán)境。

每一個(gè)模塊不僅能夠保證滿足規(guī)范，即使有其他并發(fā)的進(jìn)程進(jìn)行的時(shí)候，也不會(huì)出現(xiàn)任何問(wèn)題，黑客無(wú)法進(jìn)行攻擊。

我們?cè)隍?yàn)證并發(fā)操作系統(tǒng)的工作中發(fā)現(xiàn)，哪怕是大家用了十幾年的操作系統(tǒng)的教科書里的很多例子，一旦涉及到并發(fā)的代碼，很多都有錯(cuò)，即使老師講了很多，學(xué)生也看了很多，但我們拿它去驗(yàn)證時(shí)，還是會(huì)發(fā)現(xiàn)一些邊角的case沒(méi)有考慮到，所以我們?cè)隍?yàn)證過(guò)程中找到了很多Bug，這些Bug會(huì)變成網(wǎng)絡(luò)安全隱患。

在這個(gè)基礎(chǔ)上，我們還做了一些Device Driver的驗(yàn)證，這個(gè)其實(shí)是很有意思的。事實(shí)上，我們做操作系統(tǒng)驗(yàn)證的目標(biāo)不是只驗(yàn)證一個(gè)特定操作系統(tǒng)，而是要驗(yàn)證一類平臺(tái)，這個(gè)平臺(tái)可能不只是幾個(gè)CPU，比如汽車上會(huì)有很多的Device，有很多ECU。所以汽車操作系統(tǒng)不只是簡(jiǎn)單的Linux就在一個(gè)Box上運(yùn)行。

在這樣的Device上也可以用同樣的手段建抽象層，這方面的工作我們也做了很多，比如在一個(gè)Device Driver的最底層與硬件接觸的地方建立起大量的抽象層。此外，我們還可以拿它來(lái)驗(yàn)證一些Security，能夠在規(guī)范的層面上保證任何兩個(gè)線程之間不會(huì)互相影響，也就是說(shuō)，即使一個(gè)黑客控制了其中一個(gè)部件，也不能破壞剩下的部件。這在汽車上是非常重要的，因?yàn)槠嚿嫌泻芏嗖考?，如果黑客通過(guò)某個(gè)部件的操作系統(tǒng)黑進(jìn)了汽車，很可能會(huì)利用其攻擊其他部件或者整個(gè)主機(jī)。

總的來(lái)說(shuō)，雖然我們目前專注在CertiKOS這樣一個(gè)簡(jiǎn)單的操作系統(tǒng)上，但也在不斷尋求突破，比如在其上實(shí)現(xiàn)Real Time的功能，朝著做一個(gè)支持多核且非常安全的操作系統(tǒng)的方向前進(jìn)，這套技術(shù)也已經(jīng)變得越來(lái)越成熟。

事實(shí)上，這方面的工作以前大部分是在航天領(lǐng)域進(jìn)行?，F(xiàn)在，越來(lái)越多的業(yè)內(nèi)人士認(rèn)為，以往對(duì)于航天領(lǐng)域的諸多要求都會(huì)慢慢轉(zhuǎn)移到自動(dòng)駕駛汽車上。

5.

最后想說(shuō)的是，對(duì)于操作系統(tǒng)，中國(guó)以往做的工作大部分還只是停留在應(yīng)用層或系統(tǒng)級(jí)別更上的一層，而最核心的部分卻沒(méi)有太多涉足。

如今，新的應(yīng)用如智慧城市、區(qū)塊鏈以及自動(dòng)駕駛汽車等都已經(jīng)冒頭，原來(lái)的那些操作系統(tǒng)已經(jīng)不完全適用于這些新的應(yīng)用。但為了能馬上推向市場(chǎng)，很多都是稍微改一下便搭載到設(shè)備上，其實(shí)里面存在很多問(wèn)題。

所以操作系統(tǒng)已經(jīng)到了一個(gè)拐點(diǎn)，這時(shí)候如果有一個(gè)能保證安全的操作系統(tǒng)、出現(xiàn)一個(gè)新的平臺(tái)，我相信很多行業(yè)都會(huì)擁抱這個(gè)平臺(tái)。

*文中圖片由雷鋒網(wǎng)截自邵中演講PPT

雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見(jiàn)轉(zhuǎn)載須知。