耶魯大學終身教授邵中：「沒有 bug」的操作系統是如何煉成的？| CCF-GAIR 2017

a²+b²=c² ；

毫無疑問，勾股定理是固若金湯的真理，因此也不存在被推翻的可能性。

而在顛撲不破的數學真理之外，這個世界上還存在著病毒，不論是猖獗不已的勒索蠕蟲，或是防不勝防的「全家桶」流氓軟件，都在無孔不入地尋找軟件的漏洞。

那么，世界上是否可能有一種軟件「沒有 bug」，就像真理般沒有漏洞、不可攻破？

耶魯大學終身教授、FLINT 實驗室主任邵中教授堅定地告訴雷鋒網：有。

「防黑客攻擊」的操作系統

邵中教授是計算機程序語言設計領域的國際權威，他所研發的 SML/NJ 已經成為了 SML 語言最流行的編譯器。而目前，邵中教授在耶魯大學所做的有關 CertiKOS 操作系統的關鍵研究，就是讓系統軟件變得更加可靠安全，「保證這些軟件不會出錯，把里面的 bug 都去掉。」

所謂「沒有 bug」的操作系統，嚴格意義來說，指的是能夠防黑客攻擊的軟件體系。邵中教授告訴雷鋒網，這個問題從根本上可以通過編程或者程序的設計來實現。

這聽上去有些不可思議，但「完美的」操作系統是真實存在的。

「這與我們小時候做數學證明有點類似。以勾股定理為例，我們證明這個定理時，不會將所有的邊都窮盡列舉出來，而是通過一組引理經過邏輯演繹進行證明。也就是說，我們將程序當成一個數學公式，保證在任何情況下，所有的輸入都會按照設計者所想的那樣執行，即與原本設計的功能保持一致。如果保持一致，那么就表示它不可能有病毒可以侵入。」邵中教授這樣告訴雷鋒網 AI 科技評論。

這就是保障程序不出錯的關鍵方法，也是邵中教授所提倡的「certified software with mechanized proofs」（可信軟件）的核心要義，它也已經成為國際上非常活躍的一個研究分支。

但計算機編程與數學證明的不同之處在于，系統軟件的結構設計非常復雜，可能達到上萬行底層的匯編代碼。那么，如果程序設計者要實現十個功能，那么必須保證在任何情況下，這段代碼會嚴格按照這十個功能去執行，這依然是非常具有挑戰性的一個事情。

那么在如此龐大的信息體系中，如果程序設計者每設計一個系統，便要將可能涉及的定理從頭證明一次，這樣的工作量顯然是不現實的。計算機發展到現在，每一次進步都是在把人類生活當中的每一樣東西放到虛擬世界里。而在構建了形式化證明工具（proof assistant）時，設計者能將程序的邏輯證明過程存在計算機中，在寫形式規范之時，可以通過調用的方式直接生成程序，同時又可以生成證明。

「我們所做的這種軟件一旦被證明，這些代碼里就不可能有任何的 bug。因為如果有 bug，那么就意味著這個證明是不對的，如果證明不對，說明數學上的邏輯就不對了。而如果數學邏輯有不對的地方，可能這就不是一個程序設計問題，而是一個顛覆數學圈的問題了（笑）。」

自動駕駛的安全問題

邵中教授非常關注操作系統的安全應用問題，他認為隨著人工智能、物聯網、自動駕駛的發展，軟件對安全也會有越來越高的需求。而自動駕駛作為多家汽車廠商競逐的熱點，它的安全性便成了一個不可忽視的議題。中國科恩實驗室曾通過安全漏洞，在無物理接觸的情況下攻破特斯拉；切諾基吉也曾經被美國網絡安全專家查利·米勒和克里斯·瓦拉塞克「黑」過。如果被不法之徒抓到可趁之機，后果不堪設想。

邵中教授告訴雷鋒網 AI 科技評論，自動駕駛的系統有多元性，且需要與多個領域進行緊密合作，因此車載系統軟件的最底端必須是可靠安全的。「人類在逐步依賴計算機控制的設備時，軟件是第一步，核心軟件里一定不能有任何的 bug。我們第一步要把最底端（的架構）做安全，雖然不見得所有的零件與軟件都能保證安全，但它至少能保證一旦出錯，底端架構能夠觀察與監控部件，且不讓出錯部件影響其它的地方。」

如果有了這樣完美的軟件，又會對自動駕駛產生怎樣的影響呢？邵中教授提及了兩個有意思的領域。

一個是保險領域。有了安全可靠的軟件，保險費用及投保主體勢必會發生變化。「如果坐車的人不開車，而自動駕駛汽車不可能永遠不出問題，那么誰會為保險而買單？我想汽車制造商會把保險變成汽車成本的一部分。那么，如果汽車本身的 bug 越少，那么它的保費自然越便宜。因此，有了安全可靠的軟件，同樣能帶來經濟上的好處。」

第二個是法律倫理方面。就像「電車問題」一樣，如果是人做抉擇，可能只是一瞬間的反應，但如果把這個選擇權交給自動駕駛汽車，又需要如何用程序來限定它的行為？人與人之間的約束是通過法律來達成，而人與機器自然也會有一些形式規范存在。「法律條款與我們所說的形式規范，其實是一個東西。只不過前者可能是用法律語言寫出來，而后者是用數學語言寫出來。這一點對于我們做科研的人而言就非常有意思。」

在今年 7 月 7 日的 CCF－GAIR 2017 大會，邵中教授也將親臨自動駕駛分會場，與我們分享他在軟件安全性的真知灼見。

可信軟件，任重道遠

不過，伴隨而來的一些困難與挑戰也讓可信軟件的應用帶來了困難。

首先，可信軟件的發展是一個循序漸進的過程。原來的軟件系統已經沿用了 30 年，已經在不斷的迭代中形成了屬于自己的生態系統。而新軟件一開始的功能相對有限，因此這個演變的過程肯定需要一些時間。

「但我認為，人類對軟件安全的追求肯定是不會停止的，一旦技術上具有可行性，那么所有的人都不會希望自己用的是一個會被勒索的、會被黑客攻擊的軟件。」

其次，人工智能的大環境尚不成熟，很多商業化應用目前還沒有發展到考慮安全的階段，也沒有足夠的人才能做這件事情。以自動駕駛為例，現在有很多企業還處于第一步，即在沒有黑客攻擊的前提下先讓車跑起來的狀態。「防黑客攻擊，聽上去像是下一步的事情。但我覺得安全性的確是不能往后推移的。一旦汽車上路了，還是會有很多問題存在。」

此外，研發可信軟件的成本還是非常高的，目前主要集中于高校研究。這也是邵中教授今年 7 月受邀參加 CCF-GAIR 2017 大會的另一個原因，他希望在這個千人盛會上，通過表達自己的想法與思考，與多方尋求可能的合作。

邵中教授一直堅信，設計安全可靠的程序，才是實現人工智能的必由之路。「所有的人工智能到最后，都是用程序來實現的。這就是一個搞懂不同模塊之間關系的過程。而實現復雜人工智能功能的一個過程，就是從根本上弄懂底層這些功能的機制是如何實現的。那么，保證安全可靠的目的，就是要徹底弄懂功能之間的關系，讓它們的邏輯非常清晰，沒有矛盾。」如果你想更深入地了解邵中教授的觀點，歡迎來到 7 月 7 日-9 日中國計算機學會（CCF）主辦，雷鋒網與香港中文大學（深圳）承辦的第二屆 CCF－GAIR全球人工智能與機器人峰會，目前六折票正在火熱銷售中，詳情可訪問大會官網了解。

雷峰網原創文章，未經授權禁止轉載。詳情見轉載須知。