Re:Heartbleed and the misconceptions about Open Source
by pjreddie on Saturday April 12, 2014 @08:39PM
(#7579723)
seL4 is 9000 lines of C and took 11 person-years to verify. How big is OpenSSL?
Also, verification isn't a magic bullet, you need a good spec.
Re:Heartbleed and the misconceptions about Open Source
by mehrdada on Saturday April 12, 2014 @08:54PM
(#7579761)
> seL4 is 9000 lines of C and took 11 person-years to verify. How big is OpenSSL?
Total market cap of the top three tech companies is more than a trillion dollars. Even a hundred times more resources is affordable for them given the criticality of the project. The replacement does not have to be written in C, it can be written in ML-like languages and expose an external C interface.
> Also, verification isn't a magic bullet, you need a good spec.
True, but drawing from the CompCert anecdote, I suspect bugs in a verified implementation would be orders of magnitude less likely.
There is a verified optimizing C compiler, CompCert. Admittedly, it is not gcc, and it is not easy to do, but still. Writing a verified SSL implementation is probably not more difficult than that.