Hacker News Reader

Comment by zahllos | Hacker News Reader

Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

> and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel changes here: https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v anywhere inside AmbiML.

I mean, it does also claim to be "almost entirely written in Rust", which is true if you ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

View on HN

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.

Okay, then you should fix your mistake and edit the post or issue a new post that does not call or imply that “KataOS provides a verifiably-secure platform” since it does not. You have achieved that when any new readers of the post do not mistakenly believe that it is currently verifiably-secure.

Don't sweat it, this is just a blip. I for one have wanted an SEL4 + Rust based OS for a long time, really cool that someone is finally doing it. It's clear what the aspiration is, just keep working toward it.

Reply on news.ycombinator.com