本月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，以及证明系统满足特定的功能属性。更多消息大家可以关注本次专辑…… 在2017年19-20日在北京国家会议中心举行的LC3会议上，Linux 基金会授予中国开源软件推进联盟（China Open Source Software Promotion Union）名誉主席陆首群教授“开源软件推进终身成就奖”。
在颁奖仪式上，Linux基金会执行总监Jim Zemlin先生评价陆主席作为Linux基金会十多年的老朋友，一直关心开源软件运动，积极推进包括Linux基金会在内的开源软件组织在中国蓬勃发展。同时作为中国开源软件推进联盟的创始人和名誉主席，为利用开源技术促进信息技术产业发展和信息技术的广泛应用做出了重要的贡献。 在陆主席所著新书《开源、创新和新经济》的扉页上，Linux和Git创始人LinusTorvalds先生写道：“陆主席感谢您对中国全部开源事业作出的杰出贡献”。 Jim Zemlin先生写道：“陆首群主席作为中国开源软件的先锋，为中国和全世界开源软件的推广作出了很多重要的贡献，我对您一直心存感激”。 Apache基金会创始人、Linux基金会区块链开源软件Hyperledger项目负责人BrainBehlendorf先生写道：“感谢陆首群主席一直以来对于开源软件的信念、热情和远见”。 Linux基金会内核稳定版维护者GregKroah-Hartman先生写道：“感谢陆主席过去很多年对于开源软件的全力支持，祝福您在未来的日子里继续推动这一卓有价值的工作。”更多内容，大家不妨在本次专辑里了解一下…… 作为技术转移计划的一部分，NSA（美国国家安全局）近日公开了它的 Github 账号，分享了它开发的 32 个开源项目。NSA 最著名的开源项目是增强 Linux 内核安全的 SELinux，除此之外还有 K/V存储方案 Apache Accumulo 等项目。
该机构在计划书中写道：“NSA 技术转移计划（TTP）与希望通过此类协作将技术转移到商业的创作者合作。OSS 诚邀技术的合作开发，通过增强和调整商业软件来实现公共利益，政府将从开源社区对技术的改进中获益。”更多情况，大家可以关注本次专辑。 |
