內核開源新聞

Formal Verification Might be Built-in Linux Kernel in the Future, Message from Linux Foundation

Written by Hong Qian and Wen Qixiang

LC3 conference with the attendance of LinuxCon, ContainerCon and CloudOpen, which is the top open source conference in the world, was held in Beijing on June, 19, with a two-day session. It was its first presence to China after it had been held in North America, Europe and Japan in the past few years. Linux 4.12-rc6 was released on the same day, and voice from Linux Foundation shows us a few prospective new features will be considered in Linux kernel development at the conference.

Jim Zemblin, the Executive Director of Linux Foundation as well as the chair of the conference, told the reporter of Linux Story in the Chinese Media exclusive interview at the news conference that Formal Verification (Wikipedia) would be built-in Linux kernel for the purpose of more security. He said, the improved security credibility of Linux kernel was helpful in supporting more new features in Linux as well as the long-term development. However, it will be a hard work. We think the feature of Formal Verification will be implemented in some independent core modules first.

It is learnt that the definition of Formal Verification is to use formal methods of mathematics to prove or disprove the correctness of a certain or some formal specifications or properties. Meanwhile, Logical Formal Verification is a systematic verification process, which uses formal methods of mathematics to verify that if the design is implemented thoroughly. Today, the main Formal Verification software programs include Coq, Isabelle , Metamath ,TLA+ and so on.

The process of Formal Verification can be used to prove that there is no certain bug in one system or the system respects to some specifications. The limitation of traditional software testing methods is that limited test cases cannot cover almost infinite state space, and without considering the exception condition of test environment often leads to a loss by hidden danger in the production environment. We cannot promise a none-bug-system even if with more test cases. And in the other hand, we eagerly expect a system without bugs in some key application scenarios. NO BUG is a concept difficult to strictly define so that trying to exclude SPECIFIC TYPE of BUGs is more practicable. The Formal Verification method can prove that if a system respects to a certain design specification, if it does not contain unknown type of bugs and it can satisfy certain functions or properties with formal methods of mathematics to business logic or code logic.

The method of Formal Verification has a history of more than 30 years. Nowadays, Formal Verification is applied in the fields of chip design(1), cloud computing(2), operation system(3), compiler(4) and Blockchain(5).

If what Jim said in his plan could be implemented successfully, the security level of lightweight isolation such as Docker would be comparable to traditional virtualization, to which the improvement of Linux kernel security would not only benefit the development of cloud computing and container of Linux, but also Docker. This might be part of the future development direction of Linux. But Jim also said that there were many difficulties ahead and there was still no detailed schedule on Formal Verification at present.

Finally, we welcome any guys who are interested in Formal Verification to join our exchange group, our service account of WeChat Media Platform is bootingman, we also expect your brief introduction before your join.

對這篇文章感覺如何?

太棒了
0
不錯
0
愛死了
0
不太好
0
感覺很糟
0

You may also like

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」 一樣的軟鏈接指向它。