内核开源新闻

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” 一样的软链接指向它。