本月19日在北京舉辦的 LC3 大會(huì) (LinuxCon + ContainerCon + CloudOpen)應(yīng)該是全球最頂級(jí)的開源大會(huì)了，而這一為期兩天的開源盛會(huì)過去幾年在北美、歐洲和日本都舉辦過，而此次是其首次來(lái)到中國(guó)。就在同一天，Linux 發(fā)布了 4.12-rc6 的 release，而Linux 基金會(huì)在這次大會(huì)上也獨(dú)家透露了一些未來(lái) Linux 內(nèi)核開發(fā)的新特性。
Linux 基金會(huì)的執(zhí)行董事 Jim Zemblin 是本次大會(huì)的主持人，他同時(shí)也出席了本次大會(huì)的發(fā)布會(huì)，接受了中國(guó)媒體的專訪，在19日上午 Linux Story 記者聞其詳?shù)脑L問中，Jim 透露，未來(lái) Linux 內(nèi)核可能會(huì)引入形式驗(yàn)證（維基百科鏈接），以獲得更好的安全性，如果完成形式驗(yàn)證的話，將大大增加 Linux 在內(nèi)核安全上的可信賴度，也有利于 Linux 對(duì)更多新特性的支持和未來(lái)長(zhǎng)遠(yuǎn)發(fā)展。但是形式驗(yàn)證是一項(xiàng)艱巨的任務(wù)，我們估計(jì) Linux 應(yīng)該首先對(duì)某些相對(duì)獨(dú)立的核心模塊完成形式驗(yàn)證。
據(jù)悉，形式驗(yàn)證(Formal Verification)含義是根據(jù)某個(gè)或某些形式規(guī)范或?qū)傩裕褂脭?shù)學(xué)的方法證明其正確性或非正確性。同時(shí)邏輯形式驗(yàn)證是一個(gè)系統(tǒng)性的驗(yàn)證過程，它使用數(shù)學(xué)方法來(lái)驗(yàn)證設(shè)計(jì)在實(shí)現(xiàn)中是否得以貫徹。目前主要常用的形式驗(yàn)證軟件包括 Coq / Isabelle / Metamath / TLA+ 等。
形式驗(yàn)證過程可以證明一個(gè)系統(tǒng)不存在某個(gè) bug 或符合某些規(guī)范。而傳統(tǒng)軟件測(cè)試方法的局限在于，有限的測(cè)試用例無(wú)法覆蓋幾乎無(wú)限的狀態(tài)空間，測(cè)試環(huán)境沒有考慮到的例外狀況往往會(huì)成為隱患，在生產(chǎn)環(huán)境中造成損失。測(cè)試用例再多，也無(wú)法保證系統(tǒng)不出現(xiàn)bug，然而對(duì)于一些關(guān)鍵應(yīng)用場(chǎng)景，我們又非常需要一個(gè)沒有bug的系統(tǒng)。“沒有bug”是一個(gè)很難嚴(yán)格定義的概念，更現(xiàn)實(shí)的做法是盡力排除“特定類型的bug”。形式驗(yàn)證方法可以針對(duì)業(yè)務(wù)邏輯或者代碼邏輯進(jìn)行數(shù)學(xué)證明，證明一個(gè)系統(tǒng)符合特定的設(shè)計(jì)規(guī)范，證明系統(tǒng)不存在任何已知類型的bug，以及證明系統(tǒng)滿足特定的功能屬性。
形式驗(yàn)證方法有超過30年的歷史。目前形式驗(yàn)證在芯片設(shè)計(jì)[1]，云計(jì)算[2]，操作系統(tǒng)[3],編譯器[4]，區(qū)塊鏈[5]等領(lǐng)域都有應(yīng)用。
如果 Jim 透露的計(jì)劃能夠順利實(shí)施，也許未來(lái)可以期待 Docker 之類的輕量級(jí)隔離實(shí)現(xiàn)跟傳統(tǒng)虛擬化媲美的安全級(jí)別，這對(duì) Linux 未來(lái)在云計(jì)算和容器方面的發(fā)展大有裨益，而 Docker 也將從 Linux 內(nèi)核安全性的加強(qiáng)中獲益，這也可能是 Linux 未來(lái)的發(fā)展方向的一部分。不過 Jim 同時(shí)也說(shuō)，這是一個(gè)很困難的過程，目前還不能保證形式驗(yàn)證相關(guān)工作的具體時(shí)間表。
京公網(wǎng)安備 11010502049343號(hào)