BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage News Google Open-Sources Secure ML Operating System KataOS

Google Open-Sources Secure ML Operating System KataOS

Bookmarks

Google's AmbiML team recently open-sourced KataOS, a provably secure operating system for embedded ML hardware. KataOS is based on the seL4 microkernel and is implemented in Rust. Along with KataOS, Google is releasing Sparrow, a reference implementation of the operating system targeted for a secure hardware platform based on the RISC-V architecture.

The release was announced on the Google Open Source blog. The AmbiML team, which builds tools for ML on secure embedded environments, developed KataOS to address challenges associated with managing the privacy and security of data collected by smart devices. The foundation of this solution is seL4, a microkernel that is mathematically proven to be secure. Additional components are written in Rust, which the team chose in part because of its memory safety. KataOS is built using the CAmkES build system and can target either the RISC-V or ARM architecture. According to the AmbiML team:

Our goal is to open source all of Sparrow, including all hardware and software designs. For now, we're just getting started with an early release of KataOS on GitHub. So this is just the beginning, and we hope you will join us in building a future where intelligent ambient ML systems are always trustworthy.

Always-on or ambient smart devices have become more common in recent years, and their collection and use of personal data for machine learning has raised concerns about privacy. Although companies like Google have developed technologies such as federated learning to help preserve privacy in ML datasets, there is still a risk to privacy from a compromised or hacked device.

As a foundation for improving the security of these devices, Google recently partnered with Antmicro to develop Renode simulation support for RISC-V vector instructions. This effort was part of Google's development of Springbok, an ML hardware accelerator based on RISC-V. The Renode simulation environment allowed the Google team to co-develop the hardware and the software for a secure embedded ML platform.

The Google team continued their collaboration with Antmicro in developing KataOS. The teams added Rust support for the seL4 microkernel by developing a seL4-sys crate. They also contributed to the RISC-V target implementation of the microkernel and added sel4-specific debugging capability to Renode.

On Twitter, several users wondered if the release of KataOS signaled that Google would sunset Fuschia, an embedded OS developed by Google and used by Nest devices. Software developer Danny Thompson pointed out:

From my understanding that is still going on as well. Fuschia being an OS for Android and other systems, I think the intention for KataOS will be more for embedded devices.

The KataOS project team lead June Tate-Gans joined a Hacker News discussion to answer user questions. When one user pointed out that provably secure hardware and software are "table stakes" for more secure systems, Tate-Gans replied:

Absolutely, and this is specifically why I chose to start with seL4 and use Rust for the userland we built. seL4 has a verification framework already in place, so we can use it to ensure our system design and implementation is good. We've spent this time working with the seL4 guys to find a good middle ground in these changes, and we're going to see about verifying the design as we go, but we wanted to get these things out sooner rather than waiting because it affords more chances for feedback and collaboration. My only regret is not being able to open the entire source tree at once yet. We'll get there, but this is a good start in the meantime.

The KataOS source code is available on GitHub.

About the Author

Rate this Article

Adoption
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

BT