本月19日在北京舉辦的 LC3 大會 (LinuxCon + ContainerCon + CloudOpen)應該是全球最***的開源大會了，而這一為期兩天的開源盛會過去幾年在北美、歐洲和日本都舉辦過，而此次是其***來到中國。就在同一天，Linux 發布了 4.12-rc6 的 release，而Linux 基金會在這次大會上也獨家透露了一些未來 Linux 內核開發的新特性。 

Linux 基金會的執行董事 Jim Zemblin 是本次大會的主持人，他同時也出席了本次大會的發布會，接受了中國媒體的專訪，在19日上午 Linux Story 記者聞其詳的訪問中，Jim 透露，未來 Linux 內核可能會引入形式驗證，以獲得更好的安全性，如果完成形式驗證的話，將大大增加 Linux 在內核安全上的可信賴度，也有利于 Linux 對更多新特性的支持和未來長遠發展。但是形式驗證是一項艱巨的任務，我們估計 Linux 應該首先對某些相對獨立的核心模塊完成形式驗證。

據悉，形式驗證(Formal Verification)含義是根據某個或某些形式規范或屬性，使用數學的方法證明其正確性或非正確性。同時邏輯形式驗證是一個系統性的驗證過程，它使用數學方法來驗證設計在實現中是否得以貫徹。目前主要常用的形式驗證軟件包括 Coq / Isabelle / Metamath / TLA+ 等。

形式驗證過程可以證明一個系統不存在某個 bug 或符合某些規范。而傳統軟件測試方法的局限在于，有限的測試用例無法覆蓋幾乎***的狀態空間，測試環境沒有考慮到的例外狀況往往會成為隱患，在生產環境中造成損失。測試用例再多，也無法保證系統不出現bug，然而對于一些關鍵應用場景，我們又非常需要一個沒有bug的系統。“沒有bug”是一個很難嚴格定義的概念，更現實的做法是盡力排除“特定類型的bug”。形式驗證方法可以針對業務邏輯或者代碼邏輯進行數學證明，證明一個系統符合特定的設計規范，證明系統不存在任何已知類型的bug，以及證明系統滿足特定的功能屬性。

形式驗證方法有超過30年的歷史。目前形式驗證在芯片設計[1]，云計算[2]，操作系統[3],編譯器[4]，區塊鏈[5]等領域都有應用。

如果 Jim 透露的計劃能夠順利實施，也許未來可以期待 Docker 之類的輕量級隔離實現跟傳統虛擬化媲美的安全級別，這對 Linux 未來在云計算和容器方面的發展大有裨益，而 Docker 也將從 Linux 內核安全性的加強中獲益，這也可能是 Linux 未來的發展方向的一部分。不過 Jim 同時也說，這是一個很困難的過程，目前還不能保證形式驗證相關工作的具體時間表。