BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

无Bug微内核seL4 7.0.0发布

| 作者 Kevin Neaton 关注 2 他的粉丝 ,译者 谢丽 关注 9 他的粉丝 发布于 2017年11月7日. 估计阅读时间: 3 分钟 | 如何结合区块链技术,帮助企业降本增效?让我们深度了解几个成功的案例。

微内核seL4 7.0.0版本发布,提供了另外一种基于CMake的构建系统,支持源码树外构建和交互式配置。该版本还支持独立的ia32构建,并包含aarch64的详细文档。

seL4是一个高可靠性开源微内核,提供基于端到端验证的强隔离保障。实际上,这是说seL4代码库是无Bug的,当“验证假设”满足时,就发生指定的行为。正因如此,它已经被用于将运行在同一个处理器上的受信任组件和不受信任组件隔离。

seL4微内核由NICTA开发和维护,并通过了NICTA(现在是Data61的Trustworthy Systems Group)的正式验证,目前归General Dynamics C4 Systems(GDC4S)所有。2014年,“为了帮助每个人构建更可信赖(安全、无风险、可靠)的计算机系统”,NICTA和GDC4S决定开源seL4。

功能正确性初步验证是在2009年通过L4.verified项目完成的。该项目表明,代码正确地实现了正式的内核规范。后续对该内核的全面正式验证证明,该规范既能提供期望的高级安全属性,如“可用性、权限限制、完整性和保密性”,又能提供那些用于代码及二进制级别转译的属性。总的结果就是一个通用操作系统内核的首次端到端验证。值得注意的是,10多年来,该验证一直随着内核的发展而变化,成为在这种规模下前所未有的验证。

按照设计,虽然seL4内核有大量的验证工作,但它仍然保持着很高的性能,实际上,它已经促进了性能优化的实现。当前,验证提供的属性和不变量用于获悉内核的最坏情况执行时间(WCET),从而改进内核实现,进一步减少WCET。类似地,增加的“快速路径(fastpath)”在可能的时候会自动提升进程间通信(IPC)速度。后来,该验证经过了扩展,不管是否使用了快速路径,都可以验证内核行为是否符合规范。这项工作的结果就是一个速度、安全性、可靠性可证的内核,其应用领域包括国防、汽车、航空、医疗设备和工业自动化。

美国通过SBIR(小型企业创新研究)项目发放了超过230万美元奖金,用于资助那些与seL4相关的国防项目。在其中一个这样的项目中,SMACCM团队使用seL4构建了具有“非法入侵高度复原性”的无人机(UVV)。该团队使用seL4将运行非关键代码的虚拟化Linux实例和运行在同一块“任务板(mission board)”上的关键代码隔离开。在红队设法非法入侵时,蓝队仍然能够有效地操作基于seL4的系统。该系统最初开发时使用了一个普通的四轴飞行器,后来换成了由Boeing开发的“无人小鸟(ULB)”无人直升机。但是,seL4不限于国防承包商。由于支持Raspberry Pi 3,基于seL4开发安全、无风险、可靠的系统也在学生的研究范围内。

虽然seL4在安全操作系统开发领域最先进,但按照定义,它是最小的,不是一个像Linux这样的全功能操作系统,并没有包含所有为了提供使用便利的东西,比如,支持各种设备及简单的进程间通信。

开发和验证工作的当前状态来自经常更新的开发和验证路线图。常见问题的答案可以从项目的FAQ页查看。

查看英文原文seL4 Bug-Free Microkernel 7.0.0

评价本文

专业度
风格

您好,朋友!

您需要 注册一个InfoQ账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我
社区评论

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT