旧金山，2021 年 5 月 5 日——今天，seL4 基金会和 RISC-V International 宣布，在 CSIRO 的 Data61 中，经过验证的 RV64 架构上的 seL4 微内核已经被证明到可执行代码，这要感谢 HENSOLDT Cyber GmbH 提供的资金。这保证了 RV64 上的 seL4 微内核即使是用不可信的 C 编译器 GCC 构建的，也能按照规范操作。

在开放协作社区内或跨开放协作社区，在共同感兴趣的领域进行合作是至关重要的。RISC-V 和 seL4 很高兴地宣布他们的进展和他们的联盟，他们联合力量使更强的整体安全，结合面向安全的体系结构和操作系统设计。

“我们很高兴能成为第一个拥有安全的操作系统内核的架构，拥有如此强大的正式验证故事。”RISC-V International 首席技术官 Mark Himelstein 说：“RISC-V 正在继续增加包含 ISA 的安全特性，而安全的 seL4 内核是一个自然的补充。”

“这是 seL4 的另一个里程碑，它继续定义着操作系统安全的最新水平。”seL4 基金会主席 Gernot Heiser 教授补充说：“加强两个开放生态系统的协调非常有意义。”

“经过验证的 seL4 微内核构成了 TRENTOS 的核心，TRENTOS 是我们的 MiG-V 芯片的安全操作系统，是具有供应链安全的 RISC-V 处理器，”HENSOLDT Cyber GmbH 的 CTO Sascha Kegreiß 说。“这种独特的软硬件安全组合可以保护关键资产免受高级持久的网络威胁。”

“翻译验证将我们所有的验证工作联系在一起，”CSIRO 验证工程师 Zoltan Kocsis 博士说。“在现代 64 位处理器中引入翻译验证带来了巨大的可伸缩性挑战，但最终，我们能够克服这些挑战。”