Hacker News Reader

Comment by adrianN | Hacker News Reader

There are approximately zero codebases of nontrivial size that are written in memory unsafe languages and free of serious security holes that would be impossible in safer languages. That is pretty good evidence that the measures you suggest are not very effective.

View on HN

Still approx. zero, but seL4 kernel's written in C and proven correct preventing many security holes memory control prevents

seL4 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.

Wasn’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?

afaik, 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.

Fine! Now we have a way to write guaranteed safe C code.

It requires quite a lot of qualification from the development team, though.

if ur fine with writing 4 lines of code a day from an expert...i guess

With 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.)

of course, with unverified code, "completed" means absence of evidence of bugs, not evidence of absence.

seL4 is absolutely tiny, not a good example - it's probably smaller than log4j. Plus, it took years of PhD time to develop.

Doesn't OpenBSD have a decent track record?

Reply on news.ycombinator.com