Data61的seL4安全实施现已可用于RISC-V生态系统

联邦科学与工业研究组织（CSIRO）的Data61已经完成了针对RISC-V指令集体系结构（ISA）的开源seL4微内核实现正确性的证明。

与大多数其他ISA设计不同，RISC-VISA是在开源许可证下提供的，无需付费。根据Data61的说法，许多组织正在基于开放式RISC-VISA开发处理器，其目标平台从嵌入式和网络物理系统到高端服务器。

Data61的发展意味着seL4的安全实施现在可用于RISC-V生态系统。

Data61的可信赖系统研究小组的证明工程小组负责人RafalKolanski博士说：“我们的目标是使软件业从临时的，不可靠的工程实践转变为基于数学基础的有原则的方法。”

“验证将成为危及安全性的默认选择，而在RISC-V架构上对seL4的验证是一个重要的里程碑。”

Data61宣称seL4是世界上第一个操作系统（OS）内核，在数学上已被证明是安全的，并且是世界上最快，最先进的OS微内核。

内核是在任何计算机系统的核心上运行的软件，负责确保总体安全性，安全性和可靠性。SeL4的部署范围从防御系统到自动驾驶的空中和地面车辆，其首要目标是保护它们免受网络威胁。

SeL4最初针对移动设备中使用的32位Arm处理器进行了验证，后来针对主导主流计算的64位Intel处理器进行了验证。

Linux基金会在四月宣布，它已与Data61合作，推动与向前的安全第一操作系统内核的工作。

尽管seL4与Linux不相关，但理论上seL4可以用作Linux和其他与Unix相关的操作系统的基础。

“这是seL4迈出的一大步，”seL4基金会主席GernotHeiser教授补充说，该基金会的任务是发展seL4生态系统。“这一证明使seL4的无与伦比的安全实施可用于增长最快的硬件生态系统，并且现在涵盖了所有主要的计算机体系结构。”

德国安全公司HensoldtCyber先前投资于seL4的RISC-V验证，以补充其自己的RISC-V处理器，该处理器旨在保护防御系统，智能工厂，自动驾驶汽车和关键基础设施免受网络攻击。

Hensoldt首席执行官玛丽安·拉乔（MarianRachow）周二表示，该公司已由Data61资助了正在进行的工作，因为它认为seL4是开源和最安全的微内核，而RISC-V作为一种开放和安全的处理器体系结构，可以成为确保安全的最佳基础。系统。

Rachow说：“安全系统的开源将是HensoldtCyber​​的核心战略。”“现在，使这些技术广泛进入市场很重要。基于seL4微内核的TRENTOS-MSDK是迈向安全生态系统的第一步。”

同时，RISC-V基金会主席KrsteAsanovic教授表示，他期待看到seL4在全球RISC-V社区中得到采用。