3 ms·

Eh, seL4 has a suite of tools that turn their pile of C and ASM into an obscure intermediate language that has some formally verifiable properties. IMO this is

by px43 3y ago

Eh, seL4 has a suite of tools that turn their pile of C and ASM into an obscure intermediate language that has some formally verifiable properties. IMO this is just shifting the compiler problem somewhere else, into a dark corner where no one is looking. I highly doubt that it will ever have a practical use beyond teaching kids in the classroom that formal verification is fun, and maybe nerd-sniping some defense weirdos to win some obscene DOD contracts. Some day I would love to read a report where some criminal got somewhere they shouldn't, and the fact that they landed on an seL4 system stopped them in their tracks. If something like that exists, let me know, but until then I'm putting my chips on technologies that are well known to be battle tested in the field. Maestro seems a lot more promising in that regard.

snvzz 3y ago
>(Eh, ) I highly doubt that it will ever have a practical use beyond teaching kids in the classroom that formal verification is fun, and maybe nerd-sniping some defense weirdos to win some obscene DOD contracts. Uh, perhaps take a look at the seL4 foundation's members[0], who are using it in the wild in very serious scenarios. You can learn more about them as well as ongoing development work in seL4 Summit[1]. 0. https://sel4.systems/Foundation/Membership/home.pml https://sel4.systems/Foundation/Membership/home.pml 1. https://sel4.systems/Foundation/Summit/home.pml https://sel4.systems/Foundation/Summit/home.pml
lifthrasiir 3y ago
seL4 actually has an end-to-end proof, which proves that the final compiled binary matches up with the formal specification. There are not many places that bugs can be shifted---probably the largest one at this point is the CPU itself.
- hnfong 3y ago
  The bugs are shifted into the spec, or the proof.
  - snvzz 3y ago
    Not really shifted. If you think about it, a bug in the proof will require a bug in the code. This visibility is a good thing. Overall, note that the critical code, such as the microkernel itself, is small (kLoC wise) to begin with, which minimizes the odds a bug will go undetected for long.
justneedaname 3y ago
See here[0] one of Gernot Heiser's comments (part of the seL4 foundation) talking about how "there are seL4-based devices in regular use in several defence forces. And it's being built in to various products, including civilian, eg critical infrastructure protection". There is also an interesting case study[1][2] where seL4 was shown to prevent malicious access to a drone. Using seL4 doesn't necessarily make an entire system safe but for high security applications you have to build from the ground up and having a formally proven kernel is the first step in doing that. I have been fortunate enough to play a small role in developing some stuff to be used with seL4 and it's obvious that the team are passionate about what they've got and I wish them the best of luck 0 - https://news.ycombinator.com/item?id=25552222 https://news.ycombinator.com/item?id=25552222 1 - https://www.youtube.com/watch?v=TH0tDGk19_c https://www.youtube.com/watch?v=TH0tDGk19_c 2 - http://loonwerks.com/publications/pdf/Steal-This-Drone-README.pdf http://loonwerks.com/publications/pdf/Steal-This-Drone-READM...

by px43 3y ago

snvzz 3y ago

>(Eh, ) I highly doubt that it will ever have a practical use beyond teaching kids in the classroom that formal verification is fun, and maybe nerd-sniping some defense weirdos to win some obscene DOD contracts. Uh, perhaps take a look at the seL4 foundation's members[0], who are using it in the wild in very serious scenarios. You can learn more about them as well as ongoing development work in seL4 Summit[1]. 0. https://sel4.systems/Foundation/Membership/home.pml https://sel4.systems/Foundation/Membership/home.pml 1. https://sel4.systems/Foundation/Summit/home.pml https://sel4.systems/Foundation/Summit/home.pml

lifthrasiir 3y ago

seL4 actually has an end-to-end proof, which proves that the final compiled binary matches up with the formal specification. There are not many places that bugs can be shifted---probably the largest one at this point is the CPU itself.

hnfong 3y ago
The bugs are shifted into the spec, or the proof.
- snvzz 3y ago
  Not really shifted. If you think about it, a bug in the proof will require a bug in the code. This visibility is a good thing. Overall, note that the critical code, such as the microkernel itself, is small (kLoC wise) to begin with, which minimizes the odds a bug will go undetected for long.

justneedaname 3y ago

See here[0] one of Gernot Heiser's comments (part of the seL4 foundation) talking about how "there are seL4-based devices in regular use in several defence forces. And it's being built in to various products, including civilian, eg critical infrastructure protection". There is also an interesting case study[1][2] where seL4 was shown to prevent malicious access to a drone. Using seL4 doesn't necessarily make an entire system safe but for high security applications you have to build from the ground up and having a formally proven kernel is the first step in doing that. I have been fortunate enough to play a small role in developing some stuff to be used with seL4 and it's obvious that the team are passionate about what they've got and I wish them the best of luck 0 - https://news.ycombinator.com/item?id=25552222 https://news.ycombinator.com/item?id=25552222 1 - https://www.youtube.com/watch?v=TH0tDGk19_c https://www.youtube.com/watch?v=TH0tDGk19_c 2 - http://loonwerks.com/publications/pdf/Steal-This-Drone-README.pdf http://loonwerks.com/publications/pdf/Steal-This-Drone-READM...