jtgans

Something else. We are actually sandboxing dynamically loaded applications in a hybrid CAmkES environment, while using CAmkES as a way to help statically analyze and componentize the rest of the userland services.

TL from the project here: you are absolutely correct. KataOS is for embedded systems research, whereas Fuchsia is more of a batteries included system designed for consumer devices.

This is an unrelated research project, separate from Fuchsia.

Ahh, if only. No, nobody got promoted for this. This was me and Sam working hard to get this resesrch project out as open source.

Yeahh, sorry! We had a short timeframe and wanted to get something out for something most folks had, so the Pi seemed like an obvious target.

That being said, seL4 has a hard requirement for an MMU, so I'm not sure an STM32 would work (based upon my admittedly very quick review of their product line for a side project of mine -- happy to be proven wrong!)

Actually, it is a coincidince. Picking names is hard, and I actually had no idea this project existed before I named ours.

Well, as the TL for this engineer-driven research prject, I have to say it's quite demotivating to read these sorts of comments.

As an engineer, I don't get much say in what other parts of the company do, but unfortunately, I have to bear the brunt of the blowback every time it happens, in social forums like this one, and in B2B interactions. It's quite frustrating, actually.

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.

We do not have our changes formally verified yet, but that is definitely on our roadmap -- otherwise, what's the point of starting from this set of options? Likewise, this is why we chose Rust -- there are several projects already in progress to produce formal verification tools for Rust, so we can hopefully use those as additional proofs.

Actually, this is an engineer-driven project in research, not a PM driven project. The team and I have quite a lot of passion for this project and are doing everything we can to fight that kind of thing from happening, which is why we open sourced it.

Please bear with us.

Ahh, that's unfortunate. Naming things is hard. If I had realized that was onenof the projects' prior names, I probably wouldn't have gone with that name. TBH, I have huge respect for LoseTHos / SparrowOS / TempleOS's creator Terry. He accomplished something very unique and made it flourish in the hardest of situations.

Actually, yes. We ported the seL4 crate to the latest kernel and modified it to better fit our needs. It's part of the OSS release, and we're hoping we can contribute it back to that project once we've done some more polishing to it.

Ah, darn. Sorry -- picking names is hard.

TL from the project here: yeah, I should have done more work on the wording -- we locked the content too fast, and I pushed a tad too hard at getting the post out. :P

Side-channel attacks are out of scope for the security model of both seL4 and our KataOS project, so bear that in mind for sure.

TL from the project here: you're right, the changes to the kernel are not yet formally verified, but that's on the roadmap -- there's quite a lot of work that has been done here, and tons more to come. The vast majority of changes we have made have involved lots of conversations with folks on the seL4 mailing list including Gernot Heiser and video conferences to work out the best way to do what we're doing.

I realize the blog post comes out pretty strongly on this topic, and that's my oversight -- I let my aspirations leak out instead of tempering them (this is not your typical PM-driven project) properly.

Please understand that this is an engineer-driven project in Research with a very small team where we're doing our hardest to do the right thing, so please bear with us.

TL for KataOS here. Yes, the actual point of the announcement is to get the word out about the project. We want to make it as open as possible, and while we have some hurdles with getting the entire system out in a collaborative fashion, we're doing our darndest to do so. This release actually reflects the hard-won efforts of several engineers on the team to get this out.