澳大利亚国家信息通信技术研究所（NICTA）宣布， 将其与美国军工企业通用动力合作研究的基于微内核架构的安全操作系统seL4开源。seL4安全性号称是经过严格的数学证明，其代码符合安全规范。 这次seL4开源遵循GPLv2开源协议。 开源部分包括所有内核源代码， 数学证明，以及搭建一个高度安全的系统所必需的其它一些代码以及证明。
seL4 是从 L4 微内核基础上开发的一个安全操作系统。与Unix/Linux采用的宏内核架构不同， 微内核架构下，大部分内核都作为单独的进程在特权状态下运行，他们通过消息传递进行通讯。 L4 微内核是第三代微内核， 其中包括了大约 8700 行 C 代码。 seLA 的所有功能经过了“功能正确性证明”。 可以证明其 C 代码符合安全规范， 而二进制码则是 C 代码的正确翻译。 这意味着， 在这里不需要可信的编译器来确保二进制代码的功能正确性。
函数式编程语言 Haskell 用来开发基于 ARM 架构的高性能的 seL4 基于 C 语言的实现。 NICTA 软件系统研究组的 Genor Heiser 教授告诉媒体， 与军工企业合作也就意味着关于这一系统在军工以外的领域的应用还没有太多研究。 ”军工方面的应用是通用动力主要感兴趣的方面。 因此， 他们对其它领域的用例并不太感兴趣。 而有些应用可能起初看起来很小， 但是有可能具有巨大的前景。“
“军方主要关注的安全， 它们要求很严格， 并且不断地寻找新的技术和解决方案。 但是， 我们不想这个项目一直依靠军方。后来， 我们说服了通用动力， 我们的理由是如果能够让每个人都能够使用， 基于这个项目创造出更多的产品来的话， 对通用动力是有好处的， 可能会创造一些商业机会。“
Heiser 教授认为， 医疗设备和工业自动化是两个很有应用前景的领域。“网络犯罪分子可能通过远程攻击心脏起搏器危害生命。 在美国，胰岛素泵的问题每年导致几千人死亡。 而每个大型工厂都有很多工业自动化控制的计算机， 或者工业机器人等等。 很多情况下， 出现问题是因为软件太过复杂， 而一个非重要组件的故障会影响到重要组件的运行。 seL4 可以保证系统中重要部分与非重要部分的独立运行。“
目前， seL4 的主要应用还是在无人机方面。 上个月， NICTA 对安装在无人机上的seL4 进行了网络攻击检测和防范的测试。 seL4 能够把飞行控制的不同部件隔离运行， 这样保证了如果一个部件被攻破不会导致其它控制部件的运行受到影响。
这个项目有美国国防部高级研究项目署（ DARPA ）资助。 DARPA 资助的另一个机器人项目 Boston Dynamics 去年被 Google 收购。 除了 DARPA ， NICTA 还与波音， Galois, Rockwell Collins 以及明尼苏达大学在这个项目上有合作。 seL4 还将在波音 2016 年的一个新型号的飞机上部署。
在开源后， NICTA 和通用动力还将继续对 seL4 提供支持。 此外， 任何人基于此开发的操作系统根据 GPLv2 协议， 也必须按照 GPL 协议进行开源。 而如果有人需要在开源协议范围外使用 seL4, 则需要向通用动力购买商业许可。
Heiser 教授说：“如果与 Linux 对比， 如果你想找人要一个不同的协议， 你根本就找不到人。因为版权和所有权分散在几千人那里。 而对于 seL4 来说， 由于通用动力会继续拥有它的所有权， 因此你可以找它要一份不同的协议。”
而对于 seL4 的库函数， 规范和示例程序， 则是大部分基于 BSD 许可。 而工具则基于 BSD 或者 GPL 。 有些用户级的示例因为包括了第三方的开源软件， 因此需要在许可方面更加灵活。
有兴趣的读者可以去 seL4 的 网站 去下载其源代码和文档。
滇公网安备 53230102000482号