4 ms·
Still approx. zero, but seL4 kernel's written in C and proven correct preventing many security holes memory control prevents
by bear8642 5y ago
Still approx. zero, but seL4 kernel's written in C and proven correct preventing many security holes memory control prevents
- iamtedd 5y agoseL4 was released as open-source in 2014. I know of the helicopter drone; have any other projects made use of seL4? If not, why not? My naive guess is that it's too hard to build on the project without introducing vulnerabilities and therefore negating the benefits of the kernel, but I'd love to be shown otherwise.
- erik_seaberg 5y agoWasn’t that generated from Haskell source rather than handwritten, after years of formal verification of not only the source but also the C code generator and the final machine code?
- kobebrookskC3 5y agoafaik, the c is handwritten for performance reasons, and is manually proven to be a refinement of the executable haskell model. the haskell is then proven to be a refinement of an abstract, more succinct spec.
- nine_k 5y agoFine! Now we have a way to write guaranteed safe C code. It requires quite a lot of qualification from the development team, though.
- kobebrookskC3 5y agoif ur fine with writing 4 lines of code a day from an expert...i guess
- nine_k 5y agoWith endless bug-hunting in hastily-written C code, it could be fewer than 4 lines a day of completed code. (I hope nobody actually does so poorly, except while learning C.)
- kobebrookskC3 5y agoof course, with unverified code, "completed" means absence of evidence of bugs, not evidence of absence.
- tsimionescu 5y agoseL4 is absolutely tiny, not a good example - it's probably smaller than log4j. Plus, it took years of PhD time to develop.