3 ms·

> All the popular operating systems aren’t designed with security in mind Kaspy OS runs on a switch, and they're talking about popular operating systems, so in

by metafex 10y ago

> All the popular operating systems aren’t designed with security in mind Kaspy OS runs on a switch, and they're talking about popular operating systems, so in the same vein, OpenBSD wouldn't be a popular secure OS for e.g. routers? But hey, I'd be really happy if they based it on seL4 and formally verified their security concepts. That would be a real game-changer. OTOH I'm really sceptical until they provide any relevant details.

krylon 10y ago
Also, in a microkernel-based system, verifying the kernel itself is but a start. To make a verifiably secure system for network infrastructure and IoT-devices, you need, at the very least, a provably correct IP stack. Want a nice web interface? Now you need to verify the HTTP server, too. Want to talk to other devices? You probably want a DNS resolver. And so forth... Simply signing code and having the OS refuse to execute code without valid signatures is not going to be sufficient to convince a lot of people that it's a significant improvement security-wise. (If, on the other hand, they make it open source and provide proofs of correctness for all these components, that would indeed be a significant step forward.)
- petra 10y ago
  But isn't an isolation kernel enables you to limit spread of malware between modules and to detect when a module was compromised and reset it ? Isn't that a big improvement ?
  - krylon 10y ago
    It certainly is an improvement. But my point was that it still leaves a whole lot of attack surface. If you want a provably secure system, you basically need to verify much more than "just" the kernel. On the upside, if one did so, it would have benefits beyond security.
- nickpsecurity 10y ago
  You do. The good news is that it's not a lot of components. A good example would be what's going on in DO-178B space that requires strong verification albeit not necessarily formal. They subset things like networking standards then build partitioning and quite-static design into them. Resulting ones still have decent amount of features: http://www.lynx.com/lcs-lynx-certifiable-protocol-stack/ http://www.lynx.com/lcs-lynx-certifiable-protocol-stack/ The minimum I've seen are a few drivers, bootloader, partitioning filesystem/storage, partitioning networking, and language runtime (esp Ada or today Rust). That's not a lot to build given what's already available in FOSS or embedded. More than just a separation kernel but not much more.

by metafex 10y ago

krylon 10y ago

Also, in a microkernel-based system, verifying the kernel itself is but a start. To make a verifiably secure system for network infrastructure and IoT-devices, you need, at the very least, a provably correct IP stack. Want a nice web interface? Now you need to verify the HTTP server, too. Want to talk to other devices? You probably want a DNS resolver. And so forth... Simply signing code and having the OS refuse to execute code without valid signatures is not going to be sufficient to convince a lot of people that it's a significant improvement security-wise. (If, on the other hand, they make it open source and provide proofs of correctness for all these components, that would indeed be a significant step forward.)

petra 10y ago
But isn't an isolation kernel enables you to limit spread of malware between modules and to detect when a module was compromised and reset it ? Isn't that a big improvement ?
- krylon 10y ago
  It certainly is an improvement. But my point was that it still leaves a whole lot of attack surface. If you want a provably secure system, you basically need to verify much more than "just" the kernel. On the upside, if one did so, it would have benefits beyond security.
nickpsecurity 10y ago
You do. The good news is that it's not a lot of components. A good example would be what's going on in DO-178B space that requires strong verification albeit not necessarily formal. They subset things like networking standards then build partitioning and quite-static design into them. Resulting ones still have decent amount of features: http://www.lynx.com/lcs-lynx-certifiable-protocol-stack/ http://www.lynx.com/lcs-lynx-certifiable-protocol-stack/ The minimum I've seen are a few drivers, bootloader, partitioning filesystem/storage, partitioning networking, and language runtime (esp Ada or today Rust). That's not a lot to build given what's already available in FOSS or embedded. More than just a separation kernel but not much more.