a²+b²=c² ；

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

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

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

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

「防黑客攻擊」的操作系統(tǒng)

邵中教授是計算機程序語言設(shè)計領(lǐng)域的國際權(quán)威，他所研發(fā)的 SML/NJ 已經(jīng)成為了 SML 語言最流行的編譯器。而目前，邵中教授在耶魯大學(xué)所做的有關(guān) CertiKOS 操作系統(tǒng)的關(guān)鍵研究，就是讓系統(tǒng)軟件變得更加可靠安全，「保證這些軟件不會出錯，把里面的 bug 都去掉?！?/p>

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

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

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

這就是保障程序不出錯的關(guān)鍵方法，也是邵中教授所提倡的「certified software with mechanized proofs」（可信軟件）的核心要義，它也已經(jīng)成為國際上非?；钴S的一個研究分支。

但計算機編程與數(shù)學(xué)證明的不同之處在于，系統(tǒng)軟件的結(jié)構(gòu)設(shè)計非常復(fù)雜，可能達到上萬行底層的匯編代碼。那么，如果程序設(shè)計者要實現(xiàn)十個功能，那么必須保證在任何情況下，這段代碼會嚴(yán)格按照這十個功能去執(zhí)行，這依然是非常具有挑戰(zhàn)性的一個事情。

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

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

自動駕駛的安全問題

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

邵中教授告訴雷鋒網(wǎng) AI 科技評論，自動駕駛的系統(tǒng)有多元性，且需要與多個領(lǐng)域進行緊密合作，因此車載系統(tǒng)軟件的最底端必須是可靠安全的?！溉祟愒谥鸩揭蕾囉嬎銠C控制的設(shè)備時，軟件是第一步，核心軟件里一定不能有任何的 bug。我們第一步要把最底端（的架構(gòu)）做安全，雖然不見得所有的零件與軟件都能保證安全，但它至少能保證一旦出錯，底端架構(gòu)能夠觀察與監(jiān)控部件，且不讓出錯部件影響其它的地方?！?/p>

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

一個是保險領(lǐng)域。有了安全可靠的軟件，保險費用及投保主體勢必會發(fā)生變化?！溉绻嚨娜瞬婚_車，而自動駕駛汽車不可能永遠不出問題，那么誰會為保險而買單？我想汽車制造商會把保險變成汽車成本的一部分。那么，如果汽車本身的 bug 越少，那么它的保費自然越便宜。因此，有了安全可靠的軟件，同樣能帶來經(jīng)濟上的好處?！?/p>

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

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

可信軟件，任重道遠

不過，伴隨而來的一些困難與挑戰(zhàn)也讓可信軟件的應(yīng)用帶來了困難。

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

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

其次，人工智能的大環(huán)境尚不成熟，很多商業(yè)化應(yīng)用目前還沒有發(fā)展到考慮安全的階段，也沒有足夠的人才能做這件事情。以自動駕駛為例，現(xiàn)在有很多企業(yè)還處于第一步，即在沒有黑客攻擊的前提下先讓車跑起來的狀態(tài)?！阜篮诳凸?，聽上去像是下一步的事情。但我覺得安全性的確是不能往后推移的。一旦汽車上路了，還是會有很多問題存在?！?/p>

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

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

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