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

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

從理想狀態(tài)來說，我們?nèi)祟愋枰氖且唤M永遠(yuǎn)正確的機(jī)器人來檢查我們的工作，來保證我們?cè)诰帉懫髽I(yè)操作系統(tǒng)軟件時(shí)不會(huì)犯下任何代碼編譯的錯(cuò)誤。

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

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

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

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

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

當(dāng)然除非有人制造出代碼檢驗(yàn)的機(jī)器人。

【編輯推薦】

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