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

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

邵中教授研究的內(nèi)容是如何提高與保證現(xiàn)代操作系統(tǒng)的安全性，這是為了避免攻擊者攻擊智能系統(tǒng)、造成智能車異常或者近期的勒索病毒類似的事情出現(xiàn)。邵中教授引用了紐約時(shí)報(bào)的一則報(bào)道，目前沒有證據(jù)表明智能車系統(tǒng)比傳統(tǒng)計(jì)算機(jī)系統(tǒng)安全。但智能車系統(tǒng)如果受到攻擊、出現(xiàn)問題，可以對(duì)社會(huì)造成很大的威脅。

為了達(dá)到安全的目標(biāo)，邵中教授在耶魯大學(xué)研發(fā)了一個(gè)新型的操作系統(tǒng)。由于通過測(cè)試的方法是無法發(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é)作等功能?，F(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ā)線程的處理上也有自己的處理方法。

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

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

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

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

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