Google KataOS,大部分代码用Rust编写的嵌入式安全操作系统

原文链接:Google KataOS – A secure OS for embedded systems written in Rust (mostly) 由Jean-Luc Aufranc撰写。
本文共计 860 字,预计阅读 2 分钟

Google Research 一直致力于开发自己基于Rust的操作系统 KataOS,主要的目的就是为了保护运行 ML(机器学习)应用的嵌入式系统。

近来我们也听到了很多关于 Rust 编程语言的讨论,这一语言提供了与 C 语言编程大致相同的性能水平,它可以帮助程序员编写更安全的代码,而且有“针对缓冲区溢出的内置防护”功能。多年来,Rust 编程语言的吸引力越来越大了,Linux 6.1 就是第一个包含 Rust 代码的 kernel 版本

基于 sel4、使用 Rust 编程的 KataOS

Google Research 注意到,系统安全性通常被认为是一项可以通过软件或额外的安全芯片添加到现有系统中的功能。但在当今世界,越来越多的私人数据通过互联网暴露在外,这一点十分不好。因此该公司开发了 KataOS 开源安全操作系统,针对运行 ML 应用的嵌入式设备进行了优化,而且此次他们决定使用 Rust 来编写大部分代码。

KataOS 基于 seL4 微内核,因为它在数学上被证明是安全的,这保证了机密性、完整性和可用性。Antmicro 还通过使用 Renode 模拟器为 seL4 微内核启用 Rust 应用提供了一些帮助。Google 方面也提供了关于该操作系统在安全方面的很多详细信息,部分如下所示:

通过 seL4 CAmkES 框架,我们还提供静态定义和可分析的系统组件。KataOS 提供了一个可验证安全的平台来保护用户隐私,因为应用程序在逻辑上不可能违反内核的硬件安全保护,且系统组件是可验证安全的。KataOS 几乎完全是在 Rust 中实现的,它为软件安全性提供了一个强大的起点,因为它消除了整个 class  bug,比如:off-by-one 错误和缓冲区溢出。

Sparrow 项目就是一个通过 KataOS 实现的参考案例 ,Sparrow 是为 Ambient ML 应用而设计的。该项目托管在 GitHub ,由以下代码仓库组成:

  • camkes-tool – seL4的 camkes 工具库,增加了支持 KataOS 服务的内容
  • capdl – seL4的 capdl 存储库,增加了对 KataOS 服务和 KataOS rootserver 的支持(用Rust 编写的 capdl-loader 应用的替代品,支持将系统资源移交给 KataOS MemoryManager 服务)
  • kernel – seL4的内核,带有 Sparrow 的 RISC-V 平台的驱动,支持回收 KataOS rootserver 使用的内存
  • 用于Rust 开发的 Kata 框架,以及(最终) KataOS 系统服务
  • kernel – 支持包括build-sparrow.sh 在内的脚本

该公司对此也做了详细地解释,Sparrow 包含了一个基于 RISC-V 架构、OpenTitan 构建的逻辑安全信任根,但他们在初始版本中使用的是 QEMU 64 位 Arm 平台。KataOS 和 Sparrow 目前还在开发中,他们的目标是为该项目提供完全开源的硬件和软件设计。

其他信息也可以在 Google 的公告中找到。

感谢 Christian 的信息提示。

分享这篇文章
订阅评论
提醒
0 评论
内联反馈
查看所有评论