在過去的數十年間我們一直在為此而努力,但是結果卻並不理想：可以肯定的說人類編寫的任何代碼都布滿了漏洞,我們編寫的軟體如此複雜以致這些漏洞經常是時隔多年都沒有被發現.
舉例來說,上周谷歌公司的兩位研究專家Tavis Ormandy和Julien Tinnes發現一個漏洞潛伏在Linux系統核心中將近1年的時間.Tinnes在他的博客中表示"自從2001年以來,這個漏洞對所有體系架構上的所有2.4和2.6核心造成了影響".
從理想狀態來說,我們人類需要的是一組永遠正確的機器人來檢查我們的工作,來保證我們在編寫企業操作系統軟體時不會犯下任何代碼編譯的錯誤.
我們沒有這種機器人,但是我們有"伊莎貝拉",一種由劍橋大學和Technische Universit?t München共同開發的校驗輔助應用軟體,可在在BSD授權下免費下載伊莎貝拉可以讓精確的數學公式以形式語言表現出來,為證明邏輯微積分學上的這些公式提供工具.
上周,澳大利亞的研究專家宣布他們使用伊莎貝拉來完成了首個常規用途操作系統核心的形式機器檢驗證法.正在論證的核心是安全的內置L4(SEL4)微核心,這個核心的設計是專門用來監管航空和交通領域的重要安全系統.
根據指導SEL4研發工作的澳大利亞研究專家團隊負責人Gerwin Klein博士的說法,他們實現的是常規功能的正確校驗.同時還顯示出核心對許多常規的攻擊反應並不敏感,諸如緩衝區溢出等,如果是涉及航空領域安全的操作系統,這種結果無疑是令人期待的.
好消息是Klein的工作可能會幫助未來的企業級操作系統更加安全和可靠.劍橋大學計算機實驗室的計算機邏輯學教授兼負責伊莎貝拉計劃的科學家Larry Paulson強調說,證明操作系統核心中7500行C代碼的正確性是一項獨一無二的成就,應該最終能實現滿足目前不可思議的可靠性標準的軟體.他還補充說"這項計劃實現的不僅是經過識別的微核心,而其是能夠作為用來研發其他識別軟體的技術母體來使用".
不過還有個壞消息是在SEL4中驗證的7500行C代碼花費了12個專家4年的時間才完成,在超過20萬行的形式證法中涉及了超過1萬個中間定理--才得出伊莎貝拉的驗證結果.鑒於Linux和Windows核心有超過500萬行代碼,他們當然不可能為了證明中間定理再冷凍多年,因此對於時下的企業級操作系統,來自於緩衝區溢出漏洞的可靠性和靈活性不是很快就能實現的.
