耶魯大學(xué)教授邵中：如何構(gòu)建無法被攻破的黑客防御系統(tǒng) | CCF-GAIR 2017

2017年7月7日至9日，全球人工智能與機(jī)器人峰會CCF-GAIR大會在深圳大中華喜來登酒店舉行。本次由CCF中國計(jì)算機(jī)學(xué)會主辦、雷鋒網(wǎng)與香港中文大學(xué)（深圳）承辦的大會聚集了全球30多位頂級院士、近300家AI明星AI企業(yè) ，參會人數(shù)規(guī)模高達(dá)3000人，都是國內(nèi)頂級陣容。雷鋒網(wǎng)記者在會議期間第一時(shí)間進(jìn)行現(xiàn)場報(bào)告。

在9日上午的智能駕駛專場，耶魯大學(xué)教授邵中進(jìn)行了題為“CertiKOS：A Breakthrough toward Hacker-Resistant Operating Systems”的演講（突破性的防黑客系統(tǒng)CertiKOS）。

邵中教授研究的內(nèi)容是如何提高與保證現(xiàn)代操作系統(tǒng)的安全性，這是為了避免攻擊者攻擊智能系統(tǒng)、造成智能車異?；蛘呓诘睦账鞑《绢愃频氖虑槌霈F(xiàn)。邵中教授引用了紐約時(shí)報(bào)的一則報(bào)道，目前沒有證據(jù)表明智能車系統(tǒng)比傳統(tǒng)計(jì)算機(jī)系統(tǒng)安全。但智能車系統(tǒng)如果受到攻擊、出現(xiàn)問題，可以對社會造成很大的威脅。

為了達(dá)到安全的目標(biāo)，邵中教授在耶魯大學(xué)研發(fā)了一個(gè)新型的操作系統(tǒng)。由于通過測試的方法是無法發(fā)現(xiàn)所有的bug的，所以邵中教授使用了一種新的“Formal Verification” - “形式化驗(yàn)證”的方法來保證在各種狀況下都能夠保證安全。

但這樣的操作系統(tǒng)編寫難度非常大，系統(tǒng)中也需要匯編、C、形式化代碼互相引用嵌合，最后還需要全部編譯為機(jī)器語言。這還沒完，現(xiàn)代硬件都是多核CPU，還有一個(gè)多核協(xié)作的問題。

為了解決這些問題，邵中教授教授的CertiKOS采用了模塊化（certified abstraction layers）的結(jié)構(gòu)，然后使用了先驗(yàn)證再編譯的組織邏輯，保證了整個(gè)系統(tǒng)的安全性。

在系統(tǒng)初期研發(fā)結(jié)束、設(shè)計(jì)方法得到驗(yàn)證以后，系統(tǒng)也逐步加上了中斷、協(xié)作等功能。現(xiàn)在系統(tǒng)已經(jīng)可以在排雷無人車、無人機(jī)上運(yùn)行，而且可以抵御攻擊。

根據(jù)邵中教授介紹，系統(tǒng)之上的軟件也是要符合系統(tǒng)的規(guī)范，經(jīng)過形式規(guī)范化的驗(yàn)證，代碼和狀態(tài)要保持一致，等等。系統(tǒng)在并發(fā)線程的處理上也有自己的處理方法。

接下來，邵中教授對系統(tǒng)的設(shè)計(jì)、功能實(shí)現(xiàn)、高層抽象、系統(tǒng)驗(yàn)證與測試等方面進(jìn)行了非常詳細(xì)的介紹。

邵中教授最后表示，目前的智能系統(tǒng)為了圖快，都是基于Linux、Andriod這樣開源但不夠安全的系統(tǒng)進(jìn)行開發(fā)的；但是隨著相關(guān)技術(shù)的進(jìn)一步發(fā)展、對安全性的要求越來越高，操作系統(tǒng)進(jìn)化的拐點(diǎn)即將到來。

演講結(jié)束后，邵中教授還與組委會主席、Session主持人哈爾濱工業(yè)大學(xué)（深圳）教授、朱曉蕊就操作系統(tǒng)在智能車中的支持和應(yīng)用進(jìn)行了對話。

更多大會內(nèi)容精彩報(bào)道、本演講圖文全文，請繼續(xù)關(guān)注雷鋒網(wǎng)。

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