This should be the major argument against GnuTSL and OpenSSL. PolarSSL is symbolically verified!

You can see some screenshots at http://blog.frama-c.com/ but unfortunately their frama-c annotations for polarssl are not open source. It would help a lot if such annotations could be used for similar crypto APIs also.

There are many more such symbolic verifiers and bugfinders out there (using solvers), but Frama-C was one the first and is still one of the best.

I wonder how to reconcile the symbolic verification of PolarSSL with FRAMA-C with the top comment on this thread, where someone evaluating PolarSSL found a memory corruption flaw within a day of looking at it.

The most likely explanation is that the memory corruption flaw was found in a different PolarSSL version than the one the verification kit applies to. The PolarSSL verification kit is a recent development. The available verification kit applies to version 1.1.8 with patches that have not been released yet. Another verification kit is being finalized for the 1.3.x branch.

Another possibility is that the person who found the memory corruption was not using PolarSSL in the same configuration as the one described in the verification kit. PolarSSL allows to select sub-components at compile-time, and to select between implementation options within these components. Finally, there is always the possibility that a bug remains for compilation parameters other than the ones the verification was configured for. If I did not do too bad a job, this comment should make it clear what kind of differences could explain a bug remaining: https://news.ycombinator.com/item?id=7573483

There is always the possibility of a bug in Frama-C having for consequence a bug in PolarSSL not being found. This is far less likely than the previous commenter referring to a version that was not verified.

It should be pretty easy to verify which case it is: acquire the verified version of PolarSSL and check to see if the memory corruption bug, found 2 days ago and reported publicly, is in that codebase.

Oh, there is a link for the bug. Sorry, my bad.

Yes, Privacy Enhanced Mail is not part of the verified PolarSSL configuration. And the bug at https://github.com/polarssl/polarssl/issues/83 is definitely the sort of bug Frama-C would “not shut up” about, as Regehr puts it. The warning will only occur where the buffer overflow eventually happens, and it may be more or less pleasant to go back from the site of the buffer overflow to the bug in the fashion of http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5... , but Frama-C's value analysis is designed to reliably find this bug and not shut up about it.

Can you explain what that means?

Looks like a fork that's gone through static analysis.

It is not really a fork: all the necessary bugfixes to make the chosen PolarSSL version free of undefined behavior have been contributed back and either have been released or are pending release.

It is more a choice of version, choice of compilation platform (some bugs only occur with 64-bit pointers or unsigned chars —the verification in question has been done with 32-bit pointers and signed chars, no guarantee is given for other parameters) and description of a library configuration.

The PolarSSL Verification Kit takes the form of a 8-page description of the above parameters and a 100-page technical annex with all the formal specifications and justifications. You only need to read the second part if you don't trust the kit's authors. Like similar documents are, the technical annex is intended to be audited by picking a piece at random and checking the reasoning locally and how it relates to the other pieces.