0
本文作者: 張偉 | 2017-07-12 15:28 | 專題:GAIR 2017 |
*耶魯大學(xué)邵中教授在CCF-GAIR 2017大會現(xiàn)場
雷鋒網(wǎng)按:2017年7月9日,中國計算機(jī)學(xué)會(CCF)主辦、雷鋒網(wǎng)與香港中文大學(xué)(深圳)承辦的第二屆全球人工智能與機(jī)器人峰會(CCF-GAIR 2017)進(jìn)入到最后一天的議程。自動駕駛作為人工智能大潮中一個最重要的分支,在這天得到廣泛而深入的探討。
事實上,自動駕駛的各個環(huán)節(jié),都不得不面對網(wǎng)絡(luò)安全問題。來自耶魯大學(xué)的邵中教授,作為計算機(jī)程序語言設(shè)計的權(quán)威專家受邀進(jìn)行了大會主題演講,為我們闡述了其正在研發(fā)的“反黑客攻擊”操作系統(tǒng)CertiKOS背后的理念。
大家都知道,無論是區(qū)塊鏈、機(jī)器人還是自動駕駛,其核心軟件都有一個操作系統(tǒng),操作系統(tǒng)一旦被黑客攻擊,上層安全便得不到保證。所以自動駕駛汽車的信息安全問題是一個特別大的挑戰(zhàn)。
最近幾年,業(yè)內(nèi)發(fā)生了很多黑客攻擊汽車的案例,他們根本不需要靠近車輛,便可輕松獲取十英里外車輛的控制權(quán)。這些攻擊還不能很快修復(fù),且每年都有發(fā)生。此外,勒索病毒、物聯(lián)網(wǎng)病毒等,一直困擾著那些聯(lián)網(wǎng)的設(shè)備,哪怕只是其中某一部件被攻擊,后果也不堪設(shè)想。
近來,紐約時報的一篇文章中提到,自動駕駛系統(tǒng)比你見到的手機(jī)、電腦的系統(tǒng)更加復(fù)雜,其上的聯(lián)網(wǎng)接口數(shù)不勝數(shù),一旦被攻擊,不是修復(fù)(reboot)一下就了事的,這輛車很可能變成黑客的武器,危及公眾安全。
為了從底層來解決這些問題,邵中帶領(lǐng)耶魯大學(xué)的團(tuán)隊開啟了研發(fā)項目,重新設(shè)計操作系統(tǒng)——黑客無法進(jìn)行攻擊。
目前,一般的軟件出了錯,都是用Test的方式來找到Bug的位置,了解其在特定的執(zhí)行狀態(tài)和攻擊下會有什么狀況。如果要解決Bug就不能用Test,唯一能做的就是形式化驗證。那么,如何能夠用Formal Methods(形式化方法)來驗證新的不帶Bug的操作系統(tǒng)?
所謂Formal Methods,就跟中學(xué)里的數(shù)學(xué)證明一樣,一個簡單的數(shù)學(xué)定理要花一頁紙,要驗證它有什么樣的可能性,會不會成功。但是不管它能不能做到,形式化驗證要證明這個程序滿足它的規(guī)范,而且是在任何執(zhí)行條件下,面對某一類攻擊時都不會有錯,這是形式化驗證要達(dá)到的效果。
形式化驗證為什么到現(xiàn)在還沒有成功應(yīng)用到商業(yè)的各個部門呢?原因主要有這么幾類。
第一,寫證明要有形式化支持,比如下圖是在2009年操作系統(tǒng)大會上,第一個被驗證的操作系統(tǒng)內(nèi)核。有7500行代碼,但是光7500行的C語言代碼就花了11個人年為其工作,其中還有500行的匯編代碼1000多行的C語言代碼沒有被驗證,可以看出工作量非常大。
另外一個問題是,用戶平時寫C語言代碼的時候,究竟對它有多清晰的概念?C語言也不是特別好的語言,一旦要用它來寫操作系統(tǒng)最底端的東西,可能就會出現(xiàn)C語言代碼、匯編代碼以及C語言代碼和匯編代碼雜交體并存的情況,依賴性很強(qiáng),一旦這些代碼連在一起組成一個復(fù)雜的系統(tǒng),要保證其不出錯簡直是不可能完成的任務(wù)。
除了這個問題以外,所有的操作系統(tǒng),尤其是現(xiàn)在新的多核的CPU平臺上,還有用Concurrency(并發(fā))的,往往有好幾個版本,要驗證它也非常難。
所以,現(xiàn)在的系統(tǒng)能做到的程度與理想狀態(tài)還有一個很大的Gap,像IoT、自動駕駛平臺這類系統(tǒng)會變得越來越復(fù)雜,所以Gap會越拉越大。
我們要做的這個系統(tǒng)就是要解決以上所有這些挑戰(zhàn),我們所采用的技術(shù)是Certified Abstraction Layers。
Certified Abstraction Layers這個技術(shù)不只是用于現(xiàn)有的系統(tǒng),而且還作為一種新的技術(shù)來開發(fā)新的系統(tǒng),目的就是要讓Gap變得越來越小。
怎么做到呢?我們會有一個個模塊,每一個小的模塊想象成一個代碼,每個軟件模塊寫的時候總會實現(xiàn)一些新的功能,所以有了M1,每一個被驗證的模塊就叫Certified Abstraction Layers,這中間會有一個模擬的關(guān)系,如果都是在一個抽象層上建立的話,就可以把它們并成一塊。
如果這些代碼是運(yùn)用C語言寫的,已經(jīng)被驗證滿足這些規(guī)范的話,可以把它用編譯器編譯以后生成匯編代碼,這些匯編代碼也是完全被驗證的,因為這個編譯器能保證生成的代碼和原代碼之間是完全一致的。這樣就能組成一個大的系統(tǒng),用模塊化的方式將其組成一個大的系統(tǒng)。
我們這個課題在2、3年前做的,加了支持中斷,用在車上可以保證車?yán)锩娴牟考ハ嗖皇苡绊?。最近我們做的是并發(fā)的內(nèi)核,可以在多核上運(yùn)行,每個核上都可以跑一個Linux系統(tǒng)。所以我們能證明的不只是功能性,還可以證明它不會“死”,所有普通意義上黑客能攻擊的模塊都會被去掉。
整個證明都是通過Coq Proof Assistant來進(jìn)行,該工具在2014年還獲得了(ACM Software System Award)獎項。
在具體應(yīng)用上,CertiKOS可以用在機(jī)器人及智能系統(tǒng)上,也可以運(yùn)用在無人機(jī)上,好處就是能保證操作系統(tǒng)內(nèi)核里沒有任何可被黑客攻擊的模塊。
接下來會介紹如果要建立這樣一個被驗證可信的操作系統(tǒng)的一些具體技術(shù)。
我用比較小的一個操作系統(tǒng)來給你們看一個例子,如果說是在并發(fā)系統(tǒng)上,會有一些Spin-lock Module,上面會支持一些Thread Queue,很可能上面會加一些Scheduling Module、Inter-Process Communication和Keyboard Driver等,這是一個操作系統(tǒng)怎么從底層往上搭建的方式。
其中用到的最主要的技術(shù)是Certified Abstraction Layers,就是說把所有的程序的模塊分成一塊塊,稱為Certified Objects,一個Object就代表每一個模塊對外能做什么事情。而且,代碼和模塊遵循的規(guī)范是完全一致的,這樣的做法就是讓每個模塊都有一個抽象狀態(tài)(Abstract State)和模塊能做的基類型操作(Primitives)。
所以,你每次寫任何一個軟件模塊的時候,都會在一個抽象層上做,會使用一些內(nèi)層。如果你要驗證這個模塊,就要在上面寫它的規(guī)范,你要驗證的目標(biāo)就是要保證實現(xiàn)C代碼和寫的形式化模塊之間的關(guān)系。
比如說上圖顯示的是C語言代碼中定義的Queue,這是它用的內(nèi)層,這個C語言代碼事實上是拿它來做雙向鏈表,用于實現(xiàn)一個隊列,中間還有一個State,上面還有一個head和tail,這樣做了之后你可能用其寫一些C語言代碼。
如果要保證這個代碼不會出錯,你就得保證其與它上面的規(guī)范是一致的。
事實上這是我們所有寫程序用的最多的辦法,因為你們平時寫每一行程序的時候,腦袋里都有一個自己想要實現(xiàn)的東西,所以復(fù)雜的系統(tǒng)其實都是在搭一層層的抽象層。構(gòu)建一個復(fù)雜的無人駕駛的汽車,也需要有很多抽象層,只不過是現(xiàn)在我們關(guān)注的是在最底層的操作系統(tǒng)的安全。
如果抽象規(guī)范寫成這樣,從隊列上拿下一個元素就非常簡單,你要保證C代碼和函數(shù)的規(guī)范是具備一致性的,我從隊列里拿掉一個元素,C語言就要跑好幾步,但是你能保證兩者之間是一致的。這樣的證明就表示你做了一個Simulation Proof(模擬驗證),能保證你寫的代碼和形式規(guī)范之間沒有任何Gap,那么黑客就無法攻擊系統(tǒng)。
有了這套名為Deep Specification的形式規(guī)范,就可以保證你在程序里觀察到的行為都能在規(guī)范中表達(dá)出來。有了它以后,我們能夠保證所有想要證明的Property(屬性)都可以在規(guī)范上提煉出來,便可以做一些操作系統(tǒng)的內(nèi)核驗證。
如上圖所示,如果內(nèi)核代碼是這樣的,很可能大部分代碼會包括內(nèi)存管理、線程管理、進(jìn)程管理,還有上層的Trap。
如果先把內(nèi)存管理的模塊拿出來,把它分好層,所謂分層就是保證每一層都只依賴底層,把每一個模塊都驗證了進(jìn)而并成一個。這個方式也適合用來驗證線程管理模塊、進(jìn)程管理模塊、虛擬內(nèi)存模塊等。有了這些模塊,我們就可以搭建一個Certified Sequencial kernel。
如果你又要在上面加Hypervisor的功能,比如說虛擬化的模塊,那么你只需要做的就是在硬件端有一個支持虛擬化的模塊,把硬件的功能體現(xiàn)出來。往上再提升到進(jìn)程管理,從那個地方就可以開始來驗證虛擬化模塊用來實現(xiàn)Hypervisor。這個驗證以后,就可以得到一個Certified Hypervisor,在上面就可以Boot Linux,而且是多個版本的Linux。
有了這個以后,我們就能把多行代碼之間每一塊的關(guān)系都搞得非常透徹,比如此前提到的3000行代碼就可以轉(zhuǎn)變成37層的抽象層,這些抽象層都是邏輯上的抽象層,所以它真正實現(xiàn)的速度和功能跟原來是一樣的,用這些抽象層可以把中間各種各樣的關(guān)系理順,保證不會出任何的錯誤。
在這個基礎(chǔ)上,我們還可以拿它來實現(xiàn)一些并發(fā)的Kernel。大家都知道,未來所有的自動駕駛汽車上用的芯片越來越多的應(yīng)該是MPSOC,這些多核的CPU帶來了很多同步的問題,所有的人都知道并發(fā)程序是現(xiàn)在寫程序最大的挑戰(zhàn),如果這個問題不解決,接下來整個自動駕駛汽車、無人機(jī)都會有很大的局限性。
所以我們現(xiàn)在也做多核內(nèi)核的驗證。多核內(nèi)核的驗證跟剛才用的技術(shù)是類似的,我們做的是能夠讓你把用在串行系統(tǒng)上的驗證方法運(yùn)用到了多核上,我們把多核的機(jī)器變得如串型一樣,只不過把其他的CPU變成了它的環(huán)境。
每一個模塊不僅能夠保證滿足規(guī)范,即使有其他并發(fā)的進(jìn)程進(jìn)行的時候,也不會出現(xiàn)任何問題,黑客無法進(jìn)行攻擊。
我們在驗證并發(fā)操作系統(tǒng)的工作中發(fā)現(xiàn),哪怕是大家用了十幾年的操作系統(tǒng)的教科書里的很多例子,一旦涉及到并發(fā)的代碼,很多都有錯,即使老師講了很多,學(xué)生也看了很多,但我們拿它去驗證時,還是會發(fā)現(xiàn)一些邊角的case沒有考慮到,所以我們在驗證過程中找到了很多Bug,這些Bug會變成網(wǎng)絡(luò)安全隱患。
在這個基礎(chǔ)上,我們還做了一些Device Driver的驗證,這個其實是很有意思的。事實上,我們做操作系統(tǒng)驗證的目標(biāo)不是只驗證一個特定操作系統(tǒng),而是要驗證一類平臺,這個平臺可能不只是幾個CPU,比如汽車上會有很多的Device,有很多ECU。所以汽車操作系統(tǒng)不只是簡單的Linux就在一個Box上運(yùn)行。
在這樣的Device上也可以用同樣的手段建抽象層,這方面的工作我們也做了很多,比如在一個Device Driver的最底層與硬件接觸的地方建立起大量的抽象層。此外,我們還可以拿它來驗證一些Security,能夠在規(guī)范的層面上保證任何兩個線程之間不會互相影響,也就是說,即使一個黑客控制了其中一個部件,也不能破壞剩下的部件。這在汽車上是非常重要的,因為汽車上有很多部件,如果黑客通過某個部件的操作系統(tǒng)黑進(jìn)了汽車,很可能會利用其攻擊其他部件或者整個主機(jī)。
總的來說,雖然我們目前專注在CertiKOS這樣一個簡單的操作系統(tǒng)上,但也在不斷尋求突破,比如在其上實現(xiàn)Real Time的功能,朝著做一個支持多核且非常安全的操作系統(tǒng)的方向前進(jìn),這套技術(shù)也已經(jīng)變得越來越成熟。
事實上,這方面的工作以前大部分是在航天領(lǐng)域進(jìn)行?,F(xiàn)在,越來越多的業(yè)內(nèi)人士認(rèn)為,以往對于航天領(lǐng)域的諸多要求都會慢慢轉(zhuǎn)移到自動駕駛汽車上。
最后想說的是,對于操作系統(tǒng),中國以往做的工作大部分還只是停留在應(yīng)用層或系統(tǒng)級別更上的一層,而最核心的部分卻沒有太多涉足。
如今,新的應(yīng)用如智慧城市、區(qū)塊鏈以及自動駕駛汽車等都已經(jīng)冒頭,原來的那些操作系統(tǒng)已經(jīng)不完全適用于這些新的應(yīng)用。但為了能馬上推向市場,很多都是稍微改一下便搭載到設(shè)備上,其實里面存在很多問題。
所以操作系統(tǒng)已經(jīng)到了一個拐點,這時候如果有一個能保證安全的操作系統(tǒng)、出現(xiàn)一個新的平臺,我相信很多行業(yè)都會擁抱這個平臺。
*文中圖片由雷鋒網(wǎng)截自邵中演講PPT
雷峰網(wǎng)原創(chuàng)文章,未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。
本專題其他文章