在過去的數(shù)十年間我們一直在為此而努力，但是結(jié)果卻并不理想：可以肯定的說人類編寫的任何代碼都布滿了漏洞，我們編寫的軟件如此復雜以致這些漏洞經(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)軟件時不會犯下任何代碼編譯的錯誤。

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

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

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

好消息是Klein的工作可能會幫助未來的企業(yè)級操作系統(tǒng)更加安全和可靠。劍橋大學計算機實驗室的計算機邏輯學教授兼負責伊莎貝拉計劃的科學家Larry Paulson強調(diào)說，證明操作系統(tǒng)核心中7500行C代碼的正確性是一項獨一無二的成就，應該最終能實現(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位的應用程序