在過去的數(shù)十年間我們一直在為此而努力，但是結(jié)果卻并不理想：可以肯定的說人類編寫的任何代碼都布滿了漏洞，我們編寫的軟件如此復(fù)雜以致這些漏洞經(jīng)常是時隔多年都沒有被發(fā)現(xiàn)。

舉例來說，上周谷歌公司的兩位研究專家Tavis Ormandy和Julien Tinnes發(fā)現(xiàn)一個漏洞潛伏在Linux系統(tǒng)核心中將近1年的時間。Tinnes在他的博客中表示"自從2001年以來，這個漏洞對所有體系架構(gòu)上的所有2.4和2.6核心造成了影響"。

從理想狀態(tài)來說，我們?nèi)祟愋枰氖且唤M永遠正確的機器人來檢查我們的工作，來保證我們在編寫企業(yè)操作系統(tǒng)軟件時不會犯下任何代碼編譯的錯誤。

我們沒有這種機器人，但是我們有"伊莎貝拉"，一種由劍橋大學(xué)和Technische Universit?t München共同開發(fā)的校驗輔助應(yīng)用軟件，可在在BSD授權(quán)下免費下載伊莎貝拉可以讓精確的數(shù)學(xué)公式以形式語言表現(xiàn)出來，為證明邏輯微積分學(xué)上的這些公式提供工具。

上周，澳大利亞的研究專家宣布他們使用伊莎貝拉來完成了首個常規(guī)用途操作系統(tǒng)核心的形式機器檢驗證法。正在論證的核心是安全的內(nèi)置L4(SEL4)微核心，這個核心的設(shè)計是專門用來監(jiān)管航空和交通領(lǐng)域的重要安全系統(tǒng)。

根據(jù)指導(dǎo)SEL4研發(fā)工作的澳大利亞研究專家團隊負責(zé)人Gerwin Klein博士的說法，他們實現(xiàn)的是常規(guī)功能的正確校驗。同時還顯示出核心對許多常規(guī)的攻擊反應(yīng)并不敏感，諸如緩沖區(qū)溢出等，如果是涉及航空領(lǐng)域安全的操作系統(tǒng)，這種結(jié)果無疑是令人期待的。

好消息是Klein的工作可能會幫助未來的企業(yè)級操作系統(tǒng)更加安全和可靠。劍橋大學(xué)計算機實驗室的計算機邏輯學(xué)教授兼負責(zé)伊莎貝拉計劃的科學(xué)家Larry Paulson強調(diào)說，證明操作系統(tǒng)核心中7500行C代碼的正確性是一項獨一無二的成就，應(yīng)該最終能實現(xiàn)滿足目前不可思議的可靠性標準的軟件。他還補充說"這項計劃實現(xiàn)的不僅是經(jīng)過識別的微核心，而其是能夠作為用來研發(fā)其他識別軟件的技術(shù)母體來使用"。

不過還有個壞消息是在SEL4中驗證的7500行C代碼花費了12個專家4年的時間才完成，在超過20萬行的形式證法中涉及了超過1萬個中間定理--才得出伊莎貝拉的驗證結(jié)果。鑒于Linux和Windows核心有超過500萬行代碼，他們當然不可能為了證明中間定理再冷凍多年，因此對于時下的企業(yè)級操作系統(tǒng)，來自于緩沖區(qū)溢出漏洞的可靠性和靈活性不是很快就能實現(xiàn)的。

當然除非有人制造出代碼檢驗的機器人。

【編輯推薦】

1. Windows和Linux如何在一臺計算機上共存
2. Linux置CVS集成cvstrac
3. 如何在64位的Linux中運行32位的應(yīng)用程序