<p><q>For example I’d be happy to drop a proved-correct gzip into my Linux machine as long as it was respectably fast.</q></p>
<p>Okay John let us do this and see how far we can go.</p>
<p><ahref="https://blog.frama-c.com/admin/post.php?id=187&xconv=1">Convertir en XHTML</a></p>
<p>We'll start with <ahref="http://www.zlib.net">zlib</a> that we are going to approach like we did <ahref="/index.php?post/2011/04/05/QuickLZ-1">QuickLZ</a> by verifying that the decompression feature is resilient to malicious inputs. I have described the first potential issue on <ahref="http://codereview.stackexchange.com/q/19368/20072">this code review site</a>. If you have an opinion on this potential issue you can contribute by expressing it there (registering is a one-click process) or here in the comments if you prefer.</p>
<p>We'll start with <ahref="http://www.zlib.net">zlib</a> that we are going to approach like we did <ahref="/2011/04/05/Verifying-the-Compression-Library-QuickLZ.html">QuickLZ</a> by verifying that the decompression feature is resilient to malicious inputs. I have described the first potential issue on <ahref="http://codereview.stackexchange.com/q/19368/20072">this code review site</a>. If you have an opinion on this potential issue you can contribute by expressing it there (registering is a one-click process) or here in the comments if you prefer.</p>
<blockquote><p>Edited to add: too late Andrew Šveikauskas has already determined that our first alarm was a false positive as you can see on <ahref="http://codereview.stackexchange.com/q/19368/20072">codereview.stackexchange.com</a>. Ah well… It would have been nice if out first alarm were a true positive but that was unlikely.</p>
<p>
In case you regret missing out on the fun here is another one: when reaching line inffast.c:269 where <code>from</code> is computed as <code>out - dist</code> to be accessed next what prevents variable <code>out</code> to point one byte into the output buffer and <code>dist</code> to be 2 or 3 or 19? I expect the library must guard against this in the code above but this is the end of a long day and I did not find where. Also this would typically be the kind of relational information that the value analysis fails to remember so I am not promising there is a bug to find here.</p>