无Bug微内核seL4 7.0.0发布
极客时间编辑部
讲述:丁婵大小:1.09M时长:02:23
近日,微内核 seL4 7.0.0 版本发布,提供了另外一种基于 CMake 的构建系统,支持源码树外构建和交互式配置。
seL4 是一个高可靠性的开源微内核,提供基于端到端验证的强隔离保障。实际上,这是说 seL4 代码库是无 Bug 的,当“验证假设”满足时,就发生指定的行为。正因如此,它已经被用于将运行在同一个处理器上的受信任组件和不受信任组件隔离。
seL4 微内核由 NICTA 开发和维护,并通过了 NICTA 的正式验证,目前归 GDC4S(General Dynamics C4 Systems)所有。2014 年,“为了帮助每个人构建更可信赖(安全、无风险、可靠)的计算机系统”,NICTA 和 GDC4S 决定开源 seL4。
功能正确性初步验证是在 2009 年通过 L4.verified 项目完成的。该项目表明,代码正确地实现了正式的内核规范。后续对该内核的全面正式验证证明,该规范既能提供期望的高级安全属性,如“可用性、权限限制、完整性和保密性”等,又能提供那些用于代码及二进制级别转译的属性。值得注意的是,10 多年来,该验证一直随着内核的发展而变化,成为在这种规模下前所未有的验证。
按照设计,虽然 seL4 内核有大量的验证工作,但它仍然保持着很高的性能,实际上,它已经促进了性能优化的实现。当前,验证提供的属性和不变量用于获悉内核的最坏情况执行时间,也就是 WCET,从而改进内核实现,进一步减少 WCET。类似地,增加的“快速路径(fastpath)”在可能的时候会自动提升进程间通信(IPC)速度。
后来,该验证经过了扩展,不管是否使用了快速路径,都可以验证内核行为是否符合规范。这项工作的结果就是一个速度、安全性、可靠性可证的内核,其应用领域包括国防、汽车、航空、医疗设备和工业自动化。美国通过 SBIR(小型企业创新研究)项目发放了超过 230 万美元奖金,用于资助那些与 seL4 相关的国防项目。
公开
同步至部落
取消
完成
0/2000
荧光笔
直线
曲线
笔记
复制
AI
- 深入了解
- 翻译
- 解释
- 总结
该免费文章来自《极客视点》,如需阅读全部文章,
请先领取课程
请先领取课程
免费领取
© 版权归极客邦科技所有,未经许可不得传播售卖。 页面已增加防盗追踪,如有侵权极客邦将依法追究其法律责任。
登录 后留言
精选留言
由作者筛选后的优质留言将会公开显示,欢迎踊跃留言。
收起评论