直播回顾 | seL4 基金会主席谈物理系统安全工程实践

9 月 16 日下午，seL4 基金会主席、悉尼新南威尔士大学教授 Gernot Heiser，以及鉴释 CEO 梁宇宁，围绕下一代汽车操作系统微内核 seL4，在直播间分享了 seL4 的验证故事及其实际的工程实践，此次直播是中英双语进行，也体现了鉴释的国际化趋势。

Gernot Heiser 教授开创了大规模系统代码形式验证的先河，特别是 seL4 微内核的设计、实现和形式验证。现在，这项设计被用于自动驾驶汽车、医疗设备、物联网系统和关键基础设施建设。seL4 微内核是世界上第一个具有实现正确性和安全执行的数学、机器检查证明的操作系统 (OS) 内核。它在 Arm 和 RISC-V 处理器上的全面证明仍然是独一无二的。它也是开源的、免费使用的性能基准，并得到中立的、非营利的 seL4 基金会的支持。

Gernot Heiser 教授表示：“鉴释正积极地与 seL4 基金会的成员合作，且由鉴释自主研发的代码分析工具正被成员使用。开发高质量和安全的代码是我们共同的愿景。”

鉴释 CEO 梁宇宁和合作的新一代汽车企业来组织这次直播活动目的是让验证的理论和工程的设计和实现的配合做法传授到新一代智能汽车行业的软件开发中去。在直播中，在传达 seL4 微内核各项功能和设计的同时，也向观众表达了鉴释作为物联网领域的开发团队在提供安全系统方面的引领作用，如将来我们会和基金会/汽车企业组织一系列的线下活动，把验证的方法和步骤在下一代智能汽车系统核心模块实现中应用起来，如 seL4 Core Foundation 模块/WASM VM/AOT 编译器等。

以下节选自部分直播精彩 Q&A

Q1. 安全与系统的性能方面有时存在矛盾，怎么看待这个问题？seL4 怎么去平衡安全和性能？

安全和性能的确是矛盾的，你可以根据业务去做一个系统工程的垂直分析，分析哪些性能最重要，哪些是可以优化的，从而得出最佳方案。比如说相机性能很高，但是安全就不太重要，所以可以更专注于性能优化。我觉得，针对整个垂直业务来说，可以做很好的设计的话，是可以做到安全和性能皆容的。

Q2.请问现在 seL4 在各个汽车厂商的研发投入以及应用进度有什么介绍吗？

如果你看 seL4 基金会的会员页面，你会看到已经有很多汽车公司进行合作了。汽车行业的成员涌入大约才开始 3 个月，但我们正积极商谈，未来在自动驾驶方面的合作会有显著的增长。如果大家对这个有兴趣的话，可以来联系我，一起进行联合设计，所以请加入我们的行列。

Q3. seL4 和 qnx 比较有什么区别吗？

seL4 运行得更快，对有安全保护的内核来说，它拥有健全的操作系统，它在 ARM 和 RISC-V 处理器上的全面证明仍然是独一无二的。如果能做垂直设计，还能达到更好效果。qnx 已经是比较商用的平台，提供 SDK 服务。seL4 还在研究设计中，很快就能提供 SDK 服务。

Q4. seL4 的将来哪些开发需要社区和会员合作的？

seL4 有很多模块的开发需要更多的资源的支持，比如在人和资金方面，例如：

• aarch64 上的验证

• core foundation 的开发和验证

• 还有更多有关汽车行业功能的模块开发和验证

关注“鉴释”公众号后回复关键词“sel4”获得完整的演讲 PPT 下载链接。

如果想要了解完整问答和讨论，您可以点击观看直播回放。