活动

Gernot Heiser教授开创了大规模系统代码形式验证的先河，特别是seL4微内核的设计、实现和形式验证。现在，这项设计被用于自动驾驶汽车、医疗设备、物联网系统和关键基础设施建设。seL4微内核是世界上第一个具有实现正确性和安全执行的数学、机器检查证明的操作系统 (OS) 内核。它在Arm和RISC-V处理器上的全面证明仍然是独一无二的。它也是开源的、免费使用的性能基准，并得到中立的、非营利的seL4基金会的支持。Gernot Heiser教授表示：“鉴释正积极地与seL4基金会的成员合作，且由鉴释自主研发的代码分析工具正被成员使用。开发高质量和安全的代码是我们共同的愿景。”鉴释CEO梁宇宁和合作的新一代汽车企业来组织这次直播活动目的是让验证的理论和工程的设计和实现的配合做法传授到新一代智能汽车行业的软件开发中去。因为如Gernot的直播所说“Verifying code is not written for verification is infeasible”，在直播中，在传达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的开发和验证
• 还有更多有关汽车行业功能的模块开发和验证

完整问答和讨论，请观看直播回放。