[seL4] Re: Project Sparrow / KataOS Initial Open Source Release

[elaborating] On Mon, Aug 22, 2022 at 9:21 AM June Tate-Gans (ジューン) wrote:

Ah, no, actually. That's just our simple heap memory allocator we needed for Rust TCBs.

The kata-os-allocator crate supports per-component heap allocation https://doc.rust-lang.org/stable/std/alloc/trait.GlobalAlloc.html.

What we changed was specifically designed to reclaim the pages allocated to the rootserver -- in our case, that's a Rust implemented equivalent to capDL-loader -- since once it has done it's job, the resources it takes up are effectively lost and it doesn't run any further. Since we expect KataOS to run in highly memory constrained systems with around 4MB of RAM to work with, every byte matters to us.

This is directly related to the tainting of untyped objects allocated by the seL4 kernel.

You'll want to have a look at these commits for more information on how we accomplished this: - In our KataOS rootserver: https://github.com/AmbiML/sparrow-kata/commit/6ced9974ee07ef1264540c7d69fd77... - In seL4 proper: - Allocate rootserver objects from untypeds: https://github.com/AmbiML/sparrow-kernel/commit/4220386c0cecdfac25efccdfa35b... - Taint rootserver allocated objects: https://github.com/AmbiML/sparrow-kernel/commit/98f239a2df758ff23a1f60ca61c3... - Adjust the aarch64 rootserver to use untypeds: https://github.com/AmbiML/sparrow-kernel/commit/5ccef2a45c03017ba867cc70c390...

Hopefully that helps. That's not an exhaustive list of changes, of course -- we have a few more in the CAmkES trees to help with the handover of these untypeds. There's a few other commits in there (like the describe untypeds syscall) that are required by other KataOS components, but we don't have anything pushed that uses it yet to demonstrate what it's for. We hope to get that out there soon.

The best overview of memory reclamation is in the comments at the top of kata-os-rootserver https://github.com/AmbiML/sparrow-capdl/blob/sparrow/kata-os-rootserver/src/.... The necessary kernel support is only done for our platform (riscv32) and aarch64 (rapis3b) so getting it upstream (if there is interest) would require folks to pitch in for unsupported platforms. .

On Sun, Aug 21, 2022 at 10:46 AM Hugo V.C. wrote:

...

Hi June!

Writing all OS stuff in Rust sounds very good to me. Regarding this: "and the kernel modifications that enable reclaiming the memory used by the rootserver."

Do you mean seL4 modifications...? Is this to make this work:

https://github.com/AmbiML/sparrow-kata/blob/main/apps/system/components/kata...

??

Best,

El sáb, 20 ago 2022 a las 17:36, June Tate-Gans (ジューン) via Devel () escribió:

...

Hey guys!

Sam and I have been hard at work at releasing our source code for the Project Sparrow work we've been working on for the last year or so, and we just managed to get our first release up at < https://github.com/AmbiML/sparrow-manifest>. So, we thought we'd announce it to the devel list!

A bit of background: Sparrow is a project to build an open source low-power secure embedded platform for Ambient ML applications. Our target platform leverages RISC-V and OpenTitan, and all our contributions are licensed under the Apache-2 open source license.

The Sparrow software includes a home-grown operating system named KataOS, that runs on top of seL4 and is written almost entirely in Rust.

We’ve pushed some foundational pieces of KataOS to GitHub together with build glue to run seL4 CAmkES test applications on a 64-bit ARM platform (running in simulation on qemu). These are intended to show the direction we’re headed and enable anyone to start building their own systems in Rust on top of seL4.

This initial tranche of code includes: frameworks (e.g. the sel4-sys crate that provides seL4 syscall apis), an alternate rootserver (needed for dynamic system-wide memory management), and the kernel modifications that enable reclaiming the memory used by the rootserver.

This push does not, as yet, include the CAmkES services that support dynamic loading+running of applications–that will be published as we deem it ready for sharing until eventually all of Sparrow (software and hardware designs) will be available.

While we are developing for an experimental 32-bit RISC-V platform, we intend to push code that runs on aarch64 platforms. Help is welcome to make the code base run on more platforms.

In the long run, we're planning on opening up everything we can, so please watch this space!

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google