【预告】网络研讨会|下一代汽车操作系统微内核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点

点击加入直播微信群icon-default.png?t=L892https://www.bagevent.com/event/7748494?code=011G2Jll2Kx4M74yrDkl2qCAIV2G2Jlj&state=STATE

关于主讲人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 生态系统的开发,以减少采用障碍,为加速开发筹集资金,并确保验证声明的清晰度。 

 

本文链接http://metronic.net.cn/metronic/show-53478.html