OpenSSL, and the other security problems lately, are just the top of a rabbit hole that is only ultimately resolved with isolated special hardware. Frankly we shouldn't trust our systems, open or proprietary, on the very simple basis they are too complex to verify.
Only by moving crypto functions to a separate user maintainable black box will this tide ever be stemmed. Of course, verifying that black box then becomes problematic, but it would be easier than the current situation.
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.
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.
Comments
OpenSSL, and the other security problems lately, are just the top of a rabbit hole that is only ultimately resolved with isolated special hardware. Frankly we shouldn't trust our systems, open or proprietary, on the very simple basis they are too complex to verify.
Only by moving crypto functions to a separate user maintainable black box will this tide ever be stemmed. Of course, verifying that black box then becomes problematic, but it would be easier than the current situation.
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.
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.
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.
True, but drawing from the CompCert anecdote, I suspect bugs in a verified implementation would be orders of magnitude less likely.