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

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

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

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

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

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

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

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

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

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

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

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

更多大會內容精彩報道、本演講圖文全文，請繼續關注雷鋒網。

雷峰網原創文章，未經授權禁止轉載。詳情見轉載須知。