这是为嵌入式硬件构建的可验证的安全系统，Google Research 团队针对运行 ML 应用程序的嵌入式设备进行了优化：
现在已经为这个安全操作系统 KataOS 开源了几个组件，并与 Antmicro 合作开发了他们的Renode 模拟器和相关框架。作为这个新操作系统的基础，选择seL4作为微内核，因为它把安全放在首位；它在数学上被证明是安全的，具有保证的机密性、完整性和可用性。
通过 seL4 CAmkES 框架，还能够提供静态定义和可分析的系统组件。
KataOS 提供了一个可验证安全的平台来保护用户的隐私，因为应用程序在逻辑上不可能违反内核的硬件安全保护，并且系统组件是可验证安全的。
KataOS 也几乎完全用Rust实现，它为软件安全性提供了一个强有力的起点，因为它消除了整个类别的错误，例如一个错误和缓冲区溢出。
为了证明一个安全的环境系统，还为 KataOS 构建了一个名为 Sparrow 的参考实现，它将 KataOS 与一个安全的硬件平台相结合。