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