[seL4] Re: KataOS modifications to seL4

On Mar 22, 2023, at 11:56 AM, June Tate-Gans wrote:

 The plan is to ultimately verify these changes longer term, along with the Rust work we're doing in the userland, but as you said, verification is a monumental task and this is a small research project with two people staffing it at the moment, so it may take us a while to get there.

We'd appreciate a second look on it and any constructive comments you might have, or any patches to help us out -- it's one of the reasons we pushed to get it all out in the open, in fact. If you know of a better way of doing things, we'd absolutely love to hear it, but bear in mind this is most definitely a research project and not something we expect to be used in production without additional work.

All in all, most of the changes we have in the kernel repository are focused on the boot process, devicetree and PLIC/timer drivers for our specific platform. We've made one change to provide a way to reclaim rootserver resources, and if you look at the archives of this mailing list, you'll find requests from us about how to go about this problem appropriately. Before we made this change, we worked with core developers both on and off this list to make sure we could thread the needle here.

Nice! I’m glad this has been thought about. While I don’t doubt you or your colleagues’ competence as individuals, I had worried the profit incentive from Google (especially the desire for a return on investment) could lead to hasty decisions that would lead to fatal flaws that would be expensive to fix. Hopefully more eyes on this will be helpful too! Also, KataOS seems like it would provide a useful starting point for tinkering with embedded devices running seL4, which is something I’ve thought about but been hesitant about because of my lack of experience in this field. I’ll definitely be looking closer at it. Thanks, Isaac Beckett