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

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

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

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

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

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

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

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

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

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

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

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

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

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