防崩潰系統

大家早上好。我來自澳大利亞國家信息與通訊技術研究機構（NICTA），主要從事軟件研究。此次，我為大家介紹一下可信賴的軟件系統。大家知道軟件在生活當中無處不在，我們想象一下每天的日常生活，手機、汽車、電梯，工作時用的電腦，要用到的這一切都是離不開其中的軟件。

我們每年編寫以億行計的代碼，代碼是人編寫的，難免犯錯，軟件也會就會存在一些BUG，在商業軟件測試里面每1000行里面就有5個BUG，BUG會讓電腦死機，也可能被一些黑客利用。黑客的入侵不但會造成經濟損失，甚至可能威脅生命安全。例如說使用很廣泛的心臟起搏器，要通過無線的方式進行更新，有研究人員發現可以在幾米之外黑掉心臟起搏器，發出超強的電脈沖致人死命。

所以我們需要的是可信賴的軟件，這就是NICAT現在研究的一個課題。在介紹我們的技術前，我首先講一下目前減少軟件BUG的方法。首先就是測試，輸入數據進去以后看輸出的結果是什么，結果不符合預計就修改錯誤。如果經過很多次測試都沒有出現問題就算合格了。但這不能夠排除BUG存在的可能性。

現在另外一個提高軟件可靠性的方式就是流程的認證。有一系列的標準規則，基于這些標準來評價軟件的開發、整合等等。如果說每一項標準都符合，軟件就是合格的，同樣不能排除BUG的存在。

第三個就是形式驗證。用數學方法徹底的分析每一個系統里面可能存在的行為，通過數學計算的結果，證明這個系統具備了所需的一系列功能和性能。這種方法要把真實的系統抽象為簡化模型，對模型進行驗證。形式驗證雖然很全很徹底，但是模型不能百分之百的復制現實系統。

所以我們所做的就是在真實環境當中，去驗證一個大系統的性能和功能是符合我們要求的。我們首先把系統組件化。在任何一個系統中，各種代碼和組件并非每個都是關鍵的。所以我們要做的就是，找出哪些重要的，哪些不重要。分析這些組件如何溝通和相互影響，注意控制不關鍵的代碼所獲得的權力。

然后我們用形式驗證的流程驗證這一點，驗證不同的組件滿足了對于組件功能的要求。對于核心組件我們需要按最嚴格的要求進行檢測，我們使用叫做seL4的技術來驗證內核是符合安全要求的。

之后我們去驗證各種各樣的功能，代碼的阻截、緩沖的流量等等。我們還要確保seL4和其他組件是區分開來的，其他組件沒有權力控制內核的。我們首先驗證內核關鍵功能，確保有效安全的，然后將內核組件和非關鍵組件實現隔離，其他非關鍵組件的代碼沒有權力控制內核，這就可以確保系統的安全性。