谷歌宣布发现了与 KataOS 项目相关的进展，旨在为嵌入式硬件创建安全操作系统。 KataOS系统组件采用Rust编写，运行在seL4微内核之上，并在RISC-V系统上提供了可靠性的数学证明，表明代码完全符合形式语言中指定的规范。 该项目代码在 Apache 2.0 许可证下开放。
该系统提供对基于RISC-V和ARM64架构的平台的支持。 为了在硬件之上模拟seL4和KataOS环境的运行，在开发过程中使用了Renode框架。 作为参考实现，提出了 Sparrow 软件和硬件复合体，将 KataOS 与基于 OpenTitan 平台的安全芯片相结合。 所提出的解决方案允许您将经过逻辑验证的操作系统内核与使用 OpenTitan 平台和 RISC-V 架构构建的值得信赖的硬件组件（RoT，信任根）相结合。 除了KataOS代码之外，未来还计划开放所有其他Sparrow组件，包括硬件组件。
该平台的开发着眼于专用芯片的应用，这些芯片旨在运行机器学习和处理机密信息的应用程序，这需要特殊级别的保护和确认不存在故障。 此类应用的示例包括操纵人物图像和录音的系统。 KataOS 采用可靠性验证，确保如果系统的某一部分出现故障，故障不会蔓延到系统的其余部分，特别是内核和关键部分。
seL4 架构的著名之处在于将管理内核资源的部分移至用户空间，并对此类资源应用与用户资源相同的访问控制工具。 微内核不提供用于管理文件、进程、网络连接等的现成的高级抽象；相反，它仅提供用于控制对物理地址空间、中断和处理器资源的访问的最小机制。 用于与硬件交互的高级抽象和驱动程序以用户级任务的形式在微内核之上单独实现。 此类任务对微内核可用资源的访问是通过规则的定义来组织的。
为了提供额外的保护，除了微内核之外的所有组件都是使用安全编程技术在 Rust 中原生开发的，可以最大限度地减少内存错误，这些错误会导致释放后内存访问、空指针取消引用和缓冲区溢出等问题。 seL4环境中的应用程序加载器、系统服务、应用程序开发框架、用于访问系统调用的API、进程管理器、动态内存分配机制等都是用Rust编写的。 验证的程序集使用由 seL4 项目开发的 CAmkES 工具包。 CAmkES 的组件也可以在 Rust 中创建。
Rust 通过引用检查、对象所有权和对象生命周期跟踪（范围）以及在运行时评估内存访问的正确性来强制编译时的内存安全。 Rust 还提供针对整数溢出的保护，要求变量值在使用前初始化，默认使用不可变引用和变量的概念，并提供强大的静态类型以最大限度地减少逻辑错误。
来源： opennet.ru