Hacker News new | ask | show | jobs
by pascal_cuoq 4446 days ago
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.
1 comments
tptacek 4446 days ago
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.
link
pascal_cuoq 4446 days ago
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.

link