6 ms·
> too complex to verify 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
by mehrdada 13y ago
> too complex to verify
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.
- pjreddie 13y agoseL4 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.
- mehrdada 13y ago> 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.
- deleted 13y ago[deleted]