Linux 基金会透露未来 Linux 内核可能会引入形式验证
摘要：本月19日在北京举办的LC3大会(LinuxCon+ContainerCon+CloudOpen)应该是全球最顶级的开源大会了，而这一为期两天的开源盛会过去几年在北美、欧洲和日本都举办过，而此次是其首次来到中国。
本月19日在北京举办的LC3大会(LinuxCon+ContainerCon+CloudOpen)应该是全球最顶级的开源大会了，而这一为期两天的开源盛会过去几年在北美、欧洲和日本都举办过，而此次是其首次来到中国。就在同一天，Linux发布了4.12-rc6的release，而Linux基金会在这次大会上也独家透露了一些未来Linux内核开发的新特性。
image
Linux基金会的执行董事JimZemblin是本次大会的主持人，他同时也出席了本次大会的发布会，接受了中国媒体的专访，在19日上午LinuxStory记者闻其详的访问中，Jim透露，未来Linux内核可能会引入形式验证（维基百科链接），以获得更好的安全性，如果完成形式验证的话，将大大增加Linux在内核安全上的可信赖度，也有利于Linux对更多新特性的支持和未来长远发展。但是形式验证是一项艰巨的任务，我们估计Linux应该首先对某些相对独立的核心模块完成形式验证。
据悉，形式验证(FormalVerification)含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。同时逻辑形式验证是一个系统性的验证过程，它使用数学方法来验证设计在实现中是否得以贯彻。目前主要常用的形式验证软件包括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
文章转载自开源中国社区[http://www.oschina.net]