專訪耶魯大學(xué)邵中：一個(gè)“沒有BUG”的反黑客操作系統(tǒng)，如何為自動(dòng)駕駛保駕護(hù)航？ | CCF-GAIR 2017

雷鋒網(wǎng)按：現(xiàn)為耶魯大學(xué)計(jì)算機(jī)系教授及系主任的邵中如今正帶領(lǐng)研究小組為其“反黑客攻擊”操作系統(tǒng)CertiKOS而工作。

CertiKOS具有極高的安全性和可靠性，采用了模塊分層驗(yàn)證法（Modular Layered Verification Methods），擁有并發(fā)性，可同時(shí)在多個(gè)CPU內(nèi)核上多線程運(yùn)行。此外，該系統(tǒng)整合了形式化驗(yàn)證，對(duì)無論是智能家電還是物聯(lián)網(wǎng)設(shè)備亦或是自動(dòng)駕駛汽車都能起到防黑客攻擊的保護(hù)作用。

2017年7月9日，中國(guó)計(jì)算機(jī)學(xué)會(huì)（CCF）主辦、雷鋒網(wǎng)與香港中文大學(xué)（深圳）承辦的第二屆全球人工智能與機(jī)器人峰會(huì)（CCF-GAIR 2017）的智能駕駛論壇上，邵中教授發(fā)表了題為《CertiKOS: A Breakthrough toward Hacker-Resistant Operating Systems》的主題演講，詳述了如何打造一款“反黑客攻擊”操作系統(tǒng)。

演講結(jié)束后，邵中接受了雷鋒網(wǎng)專訪，以下為對(duì)話實(shí)錄，雷鋒網(wǎng)做了不改變?cè)獾木庉嫛?/span>

雷鋒網(wǎng)：你們的目標(biāo)是要用CertiKOS替代掉Windows、Mac OS或者Linux這樣的現(xiàn)有操作系統(tǒng)嗎？

邵中：也不是說代替，操作系統(tǒng)是一個(gè)很大的概念，比如說Windows系統(tǒng)、Mac OS系統(tǒng)或者Linux，它往往是幾百萬行代碼，它把上頭的對(duì)應(yīng)用端做的各種各樣的庫(kù)都當(dāng)成是操作系統(tǒng)的一部分。

但是，另外還有一個(gè)概念叫操作系統(tǒng)內(nèi)核，那個(gè)內(nèi)核一般就比較小了，可以做個(gè)幾萬行或者小于十萬行。你說的那些操作系統(tǒng)都有一個(gè)不同的內(nèi)核，那個(gè)內(nèi)核目前是不安全的，我們就想取代那個(gè)內(nèi)核，上頭還可以跑這些不同的操作系統(tǒng)。

雷鋒網(wǎng)：也就是說，CertiKOS要與已有的操作系統(tǒng)的上層部分進(jìn)行配合，那適配性問題如何解決？

邵中：所以現(xiàn)在就有如虛擬機(jī)和Hypervisor這樣的東西存在。其實(shí)虛擬化是計(jì)算機(jī)最近幾年來最大的一個(gè)突破，像云端都是用虛擬化實(shí)現(xiàn)的，人們可以在一個(gè)云上面執(zhí)行諸多程序。其實(shí)就是把一個(gè)機(jī)器虛擬化成了多個(gè)機(jī)器。比如說很多國(guó)內(nèi)公司有很多終端設(shè)備，并不是每個(gè)終端都連著一個(gè)主機(jī)，它其實(shí)就幾臺(tái)主機(jī)放在那，然后把它分成了10-20個(gè)虛擬化的東西。

我們的內(nèi)核跟現(xiàn)有操作系統(tǒng)的上層部分結(jié)合時(shí)也是這種虛擬的形式，在汽車上也是虛擬形式，因?yàn)樗豢赡苊恳粋€(gè)東西都做。

雷鋒網(wǎng)：“反黑客攻擊”操作系統(tǒng)普及后，黑客會(huì)受到什么影響？失業(yè)？

邵中：不會(huì)，他會(huì)去黑沒用我們CertiKOS系統(tǒng)的那些地方，因?yàn)榧词拱惭b了我們的系統(tǒng)，上層的代碼還是有被黑的可能，只是不能黑到最底層。

因?yàn)槟汩_著車希望的是它即使地圖壞了、導(dǎo)航儀壞了還可以開，但它絕對(duì)不能讓被黑到把引擎、閘的控制權(quán)都交出，那是很糟糕的。

從上世紀(jì)60年代開始，我們就對(duì)寫軟件的人提出要求，不能只寫個(gè)軟件然后發(fā)表賣錢就走了，你需要對(duì)你的軟件負(fù)責(zé)，不能有bug。只是因?yàn)樽罱鼛资陙恚驗(yàn)樯虡I(yè)化的原因，人們開始不在乎軟件是否有bug，才會(huì)導(dǎo)致現(xiàn)在那么多的軟件對(duì)安全性的要求那么低。

但是我們做這個(gè)行業(yè)、這個(gè)技術(shù)就是為了改變軟件行業(yè)的現(xiàn)狀，只不過，原來人家就覺得，這么多東西還要證明，這對(duì)我要求太高了。對(duì)一個(gè)計(jì)算機(jī)游戲人家可能不在乎，但是，對(duì)關(guān)鍵軟件確實(shí)是這樣。

雷鋒網(wǎng)：目前您做這個(gè)項(xiàng)目最大的困難，要跨越的技術(shù)難題主要是什么？

邵中：非常多，做操作系統(tǒng)有意思的是，它里頭描繪的各種各樣的情景，跟我們描繪生活當(dāng)中各種各樣的情景是一樣的。操作系統(tǒng)無非是要管理各種各樣的資源、各種各樣的空間，一旦有兩個(gè)不同的東西要互相共享資源又要增值的時(shí)候，你就要找到有一種好的處理方式。

我把一個(gè)操作系統(tǒng)寫好了，我就可以像管理一堆機(jī)器人或者管理一個(gè)虛擬世界的最主宰的東西，就像上帝一樣，搭一個(gè)安全操作系統(tǒng)就有點(diǎn)像我給你這么一個(gè)平臺(tái)，給你這么多的資源，你一定得把它管理好，不能有不公平，因?yàn)橐坏┯胁还剑妥兂珊诳凸舻牡胤健?/p>

所以，其實(shí)我們里頭做的各個(gè)模塊的管理、用到的一些技術(shù)是非常有哲理的。它們來自程序設(shè)計(jì)語言、形式化語義領(lǐng)域最近30年做的很多突破性研究工作。

雷鋒網(wǎng)：現(xiàn)在這個(gè)項(xiàng)目進(jìn)展到了一個(gè)什么階段？

邵中：已經(jīng)有幾個(gè)非常好的里程碑，在去年11月份，我們做的并發(fā)操作系統(tǒng)是最難的一個(gè)課題，已經(jīng)克服了很多困難，接下去就是致力于擴(kuò)充它，讓其更好地落地到實(shí)際應(yīng)用場(chǎng)景。

應(yīng)用場(chǎng)景有很多，自動(dòng)駕駛汽車、物聯(lián)網(wǎng)設(shè)備現(xiàn)在就可以用上去。只不過，要去做這些事情我們就得成立創(chuàng)業(yè)公司來進(jìn)行，但是我們并不覺得現(xiàn)在就要放棄做學(xué)術(shù)研究，因?yàn)槲易约罕救诉€是想把這個(gè)生態(tài)圈打造得更大，然后再去進(jìn)入某一個(gè)行業(yè)。

雷鋒網(wǎng)：您可能對(duì)哪些機(jī)構(gòu)或者企業(yè)比較有興趣？

邵中：我在中國(guó)的交流還不是很多，我希望多跟中國(guó)做汽車行業(yè)、智慧城市、物聯(lián)網(wǎng)、區(qū)塊鏈等方面的企業(yè)接觸，如果他們對(duì)安全問題感興趣，可以多交流。

雷鋒網(wǎng)：目前，很多做自動(dòng)駕駛的企業(yè)其實(shí)對(duì)網(wǎng)絡(luò)安全還沒有太多的考慮和研究，那么您覺得未來可能會(huì)出現(xiàn)的對(duì)自動(dòng)駕駛汽車系統(tǒng)進(jìn)行攻擊的漏洞和缺陷是什么？

邵中：所有都可能會(huì)被侵入，但是我們要做到的并不是保護(hù)每一塊，因?yàn)槟莻€(gè)工作量太大了。我們要保護(hù)的是最底層的一層，因?yàn)榧词褂心硞€(gè)機(jī)器被攻擊了，它也不會(huì)把整個(gè)汽車上的最關(guān)鍵的部分都弄壞。

比如車上有30個(gè)機(jī)器，中間有2-3個(gè)是管著主控的，我們做這種安全系統(tǒng)要達(dá)到的最主要的目標(biāo)就是要保證，即使另外27個(gè)機(jī)器都被攻擊成功了，另外那3個(gè)還可以正常運(yùn)行。

雷鋒網(wǎng)：現(xiàn)在在傳統(tǒng)汽車或者自動(dòng)駕駛汽車上有沒有一些應(yīng)用？

邵中：我們現(xiàn)在做的大部分都還是在學(xué)術(shù)實(shí)驗(yàn)室范圍內(nèi)。

因?yàn)樽詣?dòng)駕駛汽車即使在大部分的公司里頭也無非是一個(gè)Demo，雖然說有幾個(gè)已經(jīng)在路上跑了，但大部分是不考慮網(wǎng)絡(luò)安全的。所以，這是一個(gè)非常新的領(lǐng)域，這次回來的一個(gè)原因也是希望能夠跟現(xiàn)在在做其他部分的廠家能夠有更多的接觸。

圍繞著自動(dòng)駕駛汽車和無人機(jī)的創(chuàng)業(yè)公司太多了，但是設(shè)備重視網(wǎng)絡(luò)安全的還是不多。因?yàn)榫W(wǎng)絡(luò)安全的門檻比較高，沒有幾個(gè)人是真正能夠放下心來去鉆操作系統(tǒng)軟件的實(shí)現(xiàn)，這也是為什么操作系統(tǒng)是核心軟件，為什么那么難，為什么中國(guó)到現(xiàn)在還沒有自主開發(fā)的操作系統(tǒng)。

雷鋒網(wǎng)：對(duì)CertiKOS的期待是什么？

邵中：我們準(zhǔn)備開源，所以大家都可以在上面建立應(yīng)用，就像當(dāng)初Linux從1990開始一步步滾雪球滾到現(xiàn)在這么大，我們也希望我們的安全操作系統(tǒng)也能一步步壯大并最后變成一個(gè)比較成熟的、安全的、被驗(yàn)證的、沒有bug的、黑客不能攻擊的操作系統(tǒng)。到那一步就需要慢慢吸引更多企業(yè)和機(jī)構(gòu)加入到生態(tài)圈中推動(dòng)其發(fā)展。

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