写点什么

无 Bug 微内核 seL4 7.0.0 发布

2017 年 11 月 06 日

微内核 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

2017 年 11 月 06 日 18:001763
用户头像

发布了 1008 篇内容, 共 308.1 次阅读, 收获喜欢 272 次。

关注

评论

发布
暂无评论
发现更多内容

Java零基础到进阶宝典!从小白到大神,金九银十面试这届斩获23K月薪

Java架构追梦

Java 学习 架构 面试 核心知识点

vidyo在数字化办公中提供了什么便利?

dwqcmo

音视频会议 集成架构 解决方案 智能硬件

区块链钱包开发需要注意哪些问题?区块链数字钱包搭建

135深圳3055源中瑞8032

LeetCode题解:145. 二叉树的后序遍历,栈,JavaScript,详细注释

Lee Chen

LeetCode 前端进阶训练营

2020年第三季度《全国移动App 风险监测评估报告》

InfoQ_11eaedef67e9

App 移动安全 个人隐私安全

惊险的B站Java后端岗面试之旅,复盘面试经历及面试真题

Java架构之路

Java 程序员 面试 编程语言

面向对象编程会被抛弃吗?这五大问题不容忽视

Java架构师迁哥

教育场景方案升级| 打通业务前后端,少量开发快速上线(一):互动小班

ZEGO即构

在线教育 低代码

区块链USDT支付开发方案,USDT跨境支付搭建

135深圳3055源中瑞8032

生态共赢-anyRTC创业扶持计划

anyRTC开发者

ios 音视频 WebRTC RTC 安卓

[Go 并发编程实战课]02.Mutex 源代码

custer

go

springboot+Redis+Shiro+MyBatis炸翔版CMS开源系统(代码+视频)

周老师

Java 编程 程序员 架构 面试

极客时间架构师培训 1 期 - 第 4 周总结

Kaven

【全球案例】ESL 游戏公司如何通过 Jira 定制化解决方案连接全球团队

Atlassian速递

项目管理 敏捷 Atlassian Jira

详细分析定制企业应用的价格

Philips

敏捷开发 快速开发

解释一下==和equals的区别,你以为就这么简单?那你就草率了

小Q

Java 学习 架构 面试 基础

BATJ内部Java求职面试宝典,尤其应届生如果还没有学过那后悔去吧,也许你已经错过N多家大厂offer;

Java架构师迁哥

合约跟单平台搭建,交易所跟单软件开发商

135深圳3055源中瑞8032

随机森林原理介绍与适用情况(综述篇)

计算机与AI

数据挖掘 学习 数据科学 随机森林

数字货币交易系统定制开发,区块链交易所

135深圳3055源中瑞8032

手把手带你玩转 openEuler | 初识 openEuler

openEuler

Linux 开源 操作系统

WebSocket从入门到精通,半小时就够!

JackJiang

html5 网络编程 websocket 即时通讯

蚁架构师首推SpringBoot套餐(原理+实战+面试)

小Q

Java 学习 架构 微服务 SpringBoot 2

月薪60k的Java开发在阿里是什么级别?对技术能力有哪些要求?

Java架构之路

Java 阿里巴巴 程序员 面试 编程语言

手把手带你玩转 openEuler | 如何安装 openEuler

openEuler

Linux 开源 操作系统 openEuler

TNFE-Weekly[第七十五周已更新]

莹姐🙈

小程序 前端 周报

[Go并发编程实战课]01.Mutex学习笔记

custer

go

4年Java经验,备战两月成功拿到美团、京东、字节offer

Java架构之路

Java 程序员 面试 编程语言

视频会议的应用

anyRTC开发者

ios 音视频 WebRTC 直播 安卓

1分钟将vscode撸成小霸王

gamedilong

前端 vscode

详细讲解:python中的lambda与sorted函数

计算机与AI

Python

InfoQ 极客传媒开发者生态共创计划线上发布会

InfoQ 极客传媒开发者生态共创计划线上发布会

无Bug微内核seL4 7.0.0发布-InfoQ