8 ms·

>As the foundation for this new operating system, we chose seL4 as the microkernel because it puts security front and center; it is mathematically proven secure

>As the foundation for this new operating system, we chose seL4 as the microkernel because it puts security front and center; it is mathematically proven secure, with guaranteed confidentiality, integrity, and availability. >KataOS provides a verifiably-secure platform that protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure. The wording seems quite confident, maybe it could use some additional "at least according to its specification". This approach doesn't protect against hardware bugs and side-channel attacks. Especially when one thinks of unexpected attacks like Rowhammer, there is probably no way to include them in a formal systems model beforehand.

zahllos 4y ago
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 https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v 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).
- jtgans 4y ago
  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.
  - Veserv 4y ago
    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.
  - SkyMarshal 4y ago
    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.
doublepg23 4y ago
“Beware of bugs in the above code; I have only proved it correct, not tried it.” - Knuth.
yjftsjthsd-h 4y ago
> protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure. Notice also that they're doing the traditional Google trick of pretending that it respects the user's privacy because it's secure, while ignoring the fact that most of the users privacy will be destroyed by things they designed the operating system to intentionally do in its security model.
- geofft 4y ago
  It protects the user's privacy against attackers other than Google. To be fair, this is an entirely reasonable threat model for a lot of people. For instance, if you're a reporter in an authoritarian country, Google is almost certainly not colluding with the attackers who are literally trying to kill you, and using a Chromebook and Gmail is probably the best option out there. Your threat model is "Don't die," not "Don't be subject to surveillance capitalism." But it's also something we should collectively be pushing back on. The motivating example for these products is "intelligent ambient systems," i.e., things like Nest hubs and doorbells that capture audio/video all the time. These products probably shouldn't exist at all, and to the extent they do, they should process data locally and discard it as soon as they can.
  - londons_explore 4y ago
    Google sucks up a lot of data, and is in a position to do a lot of bad stuff with it, but historically they have never told my spouse about my affair, my government about my accounts in the caymans, or leaked my nude pictures to my grandma. (I don't actually have any of these!) I really don't care how much data of mine they have while they limit their evil they use it for to deciding if they should show an ad for baseball or football shirts... And I trust them not to accidentally leak it far more than I trust my government or any smaller/less techy company.
    - water-your-self 4y ago
      Until governments approach them and demand that data or force Google to leave.
Zigurd 4y ago
It's either verifiably secure or it isn't, and that makes an enormous difference. Also, the issue of hardware bugs purports to be addressed by verifiably secure CPU designs. Of course that leaves the multitude of programmable peripheral devices. But starting with hardware and software that are implemented to be provably secure is a big change. It is table stakes for systems to be vastly harder to penetrate.
- jtgans 4y ago
  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.
- Sirened 4y ago
  are there any formally verified CPUs that support any of the constructs needed for anything more than microcontrollers? Like, I have not yet found a formally verified CPU which supports virtual memory or caching
RunSet 4y ago
Don't trust anything from the world's largest advertising corporation until you hear it from a competing source they don't own or subsidize.
29athrowaway 4y ago
Or just target the thing with a muon beam.
jtgans 4y ago
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.
- deleted 4y ago
  [deleted]
- ArtWomb 4y ago
  XMAS comes early as far as I'm concerned... A rust os & risc-v implementation is sorely needed & I expect to begin experimenting on private cloud frankenwulfs immediately. I can see why you rushed, this in my humble opinion is bigger than the release of the go programming lang ;)
- schelling42 4y ago
  Thank you very much for putting all the effort into this project. It is a great step towards more secure computing in general, and you earned respect for that.
riedel 4y ago
I do not quite get it: seL4 is verified. Is the rest of the code as well? I understand that verification of Rust is just starting to gain traction (compared to C, Java or Ada), or did they make major progress here?
Genbox 4y ago
I've always said that computer science has a PR problem. Formally verified applications is such a foreign concept to people that when you say "verified correct" they get skeptical and mistrust the whole concept. Saying something is "secure" when it has been formally verified will be received with a grain of salt, but it is much easier to say than: "we wrote a detailed specification that define the whole system via algebra, and then we let a theorem prover run all possible permutations of the specification It has now tested a billion edge-cases and we have reached a state where it no longer finds any deviation from the specification." At least it is provable better than someone saying "it is secure because we think it is".

zahllos 4y ago

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 https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v 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).

jtgans 4y ago
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.
- Veserv 4y ago
  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.
- SkyMarshal 4y ago
  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.

doublepg23 4y ago

“Beware of bugs in the above code; I have only proved it correct, not tried it.” - Knuth.

yjftsjthsd-h 4y ago

> protects the user's privacy because it is logically impossible for applications to breach the kernel's hardware security protections and the system components are verifiably secure. Notice also that they're doing the traditional Google trick of pretending that it respects the user's privacy because it's secure, while ignoring the fact that most of the users privacy will be destroyed by things they designed the operating system to intentionally do in its security model.

geofft 4y ago
It protects the user's privacy against attackers other than Google. To be fair, this is an entirely reasonable threat model for a lot of people. For instance, if you're a reporter in an authoritarian country, Google is almost certainly not colluding with the attackers who are literally trying to kill you, and using a Chromebook and Gmail is probably the best option out there. Your threat model is "Don't die," not "Don't be subject to surveillance capitalism." But it's also something we should collectively be pushing back on. The motivating example for these products is "intelligent ambient systems," i.e., things like Nest hubs and doorbells that capture audio/video all the time. These products probably shouldn't exist at all, and to the extent they do, they should process data locally and discard it as soon as they can.
- londons_explore 4y ago
  Google sucks up a lot of data, and is in a position to do a lot of bad stuff with it, but historically they have never told my spouse about my affair, my government about my accounts in the caymans, or leaked my nude pictures to my grandma. (I don't actually have any of these!) I really don't care how much data of mine they have while they limit their evil they use it for to deciding if they should show an ad for baseball or football shirts... And I trust them not to accidentally leak it far more than I trust my government or any smaller/less techy company.
  - water-your-self 4y ago
    Until governments approach them and demand that data or force Google to leave.

Zigurd 4y ago

It's either verifiably secure or it isn't, and that makes an enormous difference. Also, the issue of hardware bugs purports to be addressed by verifiably secure CPU designs. Of course that leaves the multitude of programmable peripheral devices. But starting with hardware and software that are implemented to be provably secure is a big change. It is table stakes for systems to be vastly harder to penetrate.

jtgans 4y ago
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.
Sirened 4y ago
are there any formally verified CPUs that support any of the constructs needed for anything more than microcontrollers? Like, I have not yet found a formally verified CPU which supports virtual memory or caching

RunSet 4y ago

Don't trust anything from the world's largest advertising corporation until you hear it from a competing source they don't own or subsidize.

29athrowaway 4y ago

Or just target the thing with a muon beam.

jtgans 4y ago

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.

deleted 4y ago
[deleted]
ArtWomb 4y ago
XMAS comes early as far as I'm concerned... A rust os & risc-v implementation is sorely needed & I expect to begin experimenting on private cloud frankenwulfs immediately. I can see why you rushed, this in my humble opinion is bigger than the release of the go programming lang ;)
schelling42 4y ago
Thank you very much for putting all the effort into this project. It is a great step towards more secure computing in general, and you earned respect for that.

riedel 4y ago

I do not quite get it: seL4 is verified. Is the rest of the code as well? I understand that verification of Rust is just starting to gain traction (compared to C, Java or Ada), or did they make major progress here?

Genbox 4y ago

I've always said that computer science has a PR problem. Formally verified applications is such a foreign concept to people that when you say "verified correct" they get skeptical and mistrust the whole concept. Saying something is "secure" when it has been formally verified will be received with a grain of salt, but it is much easier to say than: "we wrote a detailed specification that define the whole system via algebra, and then we let a theorem prover run all possible permutations of the specification It has now tested a billion edge-cases and we have reached a state where it no longer finds any deviation from the specification." At least it is provable better than someone saying "it is secure because we think it is".