苹果公司正式加入 seL4 基金会
source link: https://openingsource.org/11734/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
苹果公司正式加入 seL4 基金会
seL4 基金会在当地时间2024年4月29日正式披露苹果公司（Apple Inc）加入 seL4 基金会，成为其普通会员，具有投票权，但不具有董事席位。seL4 基金会对此表示欢迎，并期待未来苹果公司在形式验证与 seL4 上的工作。
seL4 基金会成立于2020年，基金会创始成员包括 Cog Systems、DornerWorks、Ghost Locomotion、HENSOLD Cyber 与 UNSW Sydney，是 Linux 基金会 (LF) 下的一个项目，并遵循 LF 的既定结构。
seL4 在 2004 年开始开发，2009 年完成形式化验证，2014 年开源，目前主要贡献者和发起人是 Gernot Heiser。澳大利亚联邦科学与工业研究组织 CSIRO/ Data61实现了对于其L4 内核的形式化证明，并创造出世界上第一个此类的实用操作系统内核 seL4。他们在2013年进一步证明了内核的信息流安全性，使得该系统成为最安全的操作系统内核之一。
seL4 是世界上第一个通过形式验证，用数学方法被证明其安全 bug-free 的操作系统内核，并且在安全的基础上拥有高性能。它对于计算系统的内核安全的可信赖度具会有极大意义，具体来看可能影响到航空航天电子、自动驾驶汽车、太空宇宙开发、医疗设备、关键基础设施、国防等行业。理论上，SeL4 可以用作 Linux 和其它类 Unix 操作系统的底层基础，甚至曾被考虑用于 GNU 计划的内核项目 GNU Hurd。此前 Linus Tolvalds 在接受 LinuxStory 采访时明确表示“形式验证”会用于 Linux 内核的开发。
更多信息欢迎访问 https://sel4.systems/
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK