內核

Linux 基金會透露未來 Linux 內核可能會引入形式驗證

本文作者為洪謙和聞其詳

本月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 同時也說,這是一個很困難的過程,目前還不能保證形式驗證相關工作的具體時間表。

[1] https://www.cl.cam.ac.uk/~jrh13/slides/nasa-14apr10/slides.pdf
[2] http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
[3] https://github.com/seL4/seL4
[4] http://compcert.inria.fr/compcert-C.html
[5] https://github.com/pirapira/eth-isabelle

最後,歡迎所有關注形式驗證的朋友加入微信交流群(6月28日失效)群已滿,可以添加 微信ID: opensourceleslie 方便拉入群中(添加請做簡單自我介紹)

對這篇文章感覺如何?

太棒了
1
不錯
0
愛死了
0
不太好
0
感覺很糟
0
bootingman,是「booting」 加上 「man」的一個合成詞。 術語「booting(引導)」是「bootstrapping」的簡寫,描述計算機從零開始啟動的過程,同時也表示一個古老的諺語「通過自力更生而出人頭地「。 「引導」的思想在於一個困難的、複雜的目標可以通過一個小的動作開始,然後以這個小的動作為基礎,一步一步地達到期望目標而完成。這也是我想做和正在做的。

    You may also like

    1 Comment

    Leave a reply

    您的電子郵箱地址不會被公開。 必填項已用 * 標註

    此站點使用Akismet來減少垃圾評論。了解我們如何處理您的評論數據

    More in:內核

    內核

    rootfs initramfs kexec 與 Linux 啟動過程

    作為 Debian 用戶,在使用 apt 更新系統時偶爾會發現某次安裝更新的時間特別長,這往往出現在較大版本的更新中,仔細觀察後就會發現,這個耗時極長的操作並不是安裝某個軟體,而是對一個名為 init […]
    內核

    龍芯開始發布針對3A6000系列CPU的Linux補丁

    儘管龍芯3A6000處理器尚未正式推出,但自去年以來的傳言將其定於在今年上半年推出,並有人聲稱這種性能提升可以與AMD Zen 3或英特爾Tiger Lake的性能水平相媲美。在3A6000系列推出之 […]
    內核

    Linux 共享庫的 soname 命名機制

    Linux 有一套規則來命名系統中的每一個共享庫,它規定共享庫的文件命名規則如下:libname.so.x.y.z,即前綴"lib"+庫名稱+後綴".so"+三個數字組成的版本號,其中,x 表示主版本號,y 表示次版本號,z 表示發布版本號。SO-NAME 命名機制,就是把共享庫的文件名去掉次版本號和發布版本號,只保留主版本號。在 Linux 系統中,系統會為每個共享庫在它所在的目錄創建一個跟它的 」SO-NAME」 一樣的軟鏈接指向它。