内核

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