【预告】网络研讨会｜下一代汽车操作系统微内核 seL4：seL4 基金会主席谈物理系统安全工程实践

seL4 微内核是世界上第一个具有实现正确性和安全执行的数学、机器检查证明的操作系统 (OS) 内核。它在 ARM 和 RISC-V 处理器上的全面证明仍然是独一无二的。它也是开源的、免费使用的性能基准，并得到中立的、非营利的 seL4 基金会的支持。多年前，它已在军用自主空中和地面车辆中得到证明，现在正被设计用于自动驾驶汽车、医疗设备、物联网系统和关键基础设施。 

目前，包括鉴释在内的多家国内外自动驾驶、芯片、软件安全等科技企业相继加入了 seL4 基金会（如：理想、蔚来、莲花汽车、地平线等），共同推动 seL4 微内核的发展。（查看更多 seL4 基金会成员：http://sel4.systems/Foundation/Membership/）

本次研讨会，我们很荣幸的邀请到

seL4 基金会主席、悉尼新南威尔士大学教授

Gernot Heiser

跟大家分享他的见解和研究成果。

本次研讨会您将了解到：

1. seL4 基金会是什么？

2. seL4 的验证故事及其实际应用的意义

3. seL4 的开源生态系统是什么？

4. Gernot Heiser 教授在悉尼新南威尔士大学的研究课题

5. 以及这些研究课题如何确保 seL4 继续定义安全操作系统技术的前沿。

2021 年 9 月 16 日下午 2 点

点击加入直播微信群

关于主讲人 Gernot Heiser 

Gernot Heiser 是悉尼新南威尔士大学 Scientia 杰出教授和 John Lions 操作系统主席。他的研究兴趣是操作系统、实时系统、安全和安全。他的研究愿景是彻底改变网络安全游戏，从追赶攻击者到可证明安全的系统。作为 Trustworthy Systems 小组的负责人，他开创了大规模系统代码形式验证的先河，特别是 seL4 微内核的设计、实现和形式验证；seL4 现在被用于现实世界的安全和安全关键系统。 

Gernot 的前公司 Open Kernel Labs 于 2012 年被 General Dynamics 收购，该公司推出了 OKL4 微内核，该微内核搭载了数十亿个移动无线芯片，并部署在所有 iOS 设备的安全区域。他目前担任 HENSOLDT Cyber 首席软件科学家、Neutrality 首席科学家和 seL4 基金会主席。Gernot 是 ACM、IEEE 和澳大利亚技术与工程学院 (ATSE) 的研究员，也是 ACM 杰出讲师。 

关于 seL4 基金会 

seL4 基金会类似于其他开源项目的基金会，例如 Linux 基金会的云原生基金会、RISC-V 基金会等。 它形成了一个开放、透明和中立的组织，负责发展 seL4 生态系统。 它将 seL4 内核的开发人员、基于 seL4 的组件和框架的开发人员以及在实际系统中采用 seL4 的开发人员聚集在一起。它的重点是协调、指导和标准化 seL4 生态系统的开发，以减少采用障碍，为加速开发筹集资金，并确保验证声明的清晰度。