RISC-V 和 seL4 基金会宣布新的安全里程碑
旧金山,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 教...



