tag:blogger.com,1999:blog-245662015774143454.post146512151674253898..comments2022-11-17T09:36:53.104+00:00Comments on Coder in a World of Code: My Heart Bleeds for OpenSSLDan Turnerhttp://www.blogger.com/profile/06837452458119663813noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-245662015774143454.post-63784184276425664692014-04-09T17:33:08.045+01:002014-04-09T17:33:08.045+01:00Hello,
Frama-C has been used to verify the 1.1.x ...Hello,<br /><br />Frama-C has been used to verify the 1.1.x (legacy) branch of PolarSSL, an other SSL implementation, in a minimal but realistic configuration. Bugs found have been reported and fixed by Paul Bakker. For those 1.1.x bugs that were still present in more recent versions, this includes fixing them in newer versions too.<br /><br />Preliminary experiments suggest that it is possible to follow the release of new versions and to re-use the work that has been done on the 1.1.x branch to re-check newer PolarSSL releases, and to identify undefined-behavior bugs in them as they are introduced.<br /><br />The report describing the PolarSSL configuration and the justifications for all remaining (false) alarms is commercially available : http://trust-in-soft.com/no-more-heartbleed/<br /><br />Search for “TrustInSoft” in PolarSSL's Changelog to get an idea how many undefined-behavior bugs can be expected to be found in an already robust C implementation of SSL: https://github.com/polarssl/polarssl/blob/development/ChangeLog<br /><br />In short, the formal verification of a C SSL implementation is doable. It is a lot of work, but it is completely doable.<br /><br />Disclaimer: I work on Frama-C and I am a founder of TrustInSoft.<br />pascal_cuoqhttps://www.blogger.com/profile/16863430576950446222noreply@blogger.comtag:blogger.com,1999:blog-245662015774143454.post-88440421444268294502014-04-09T10:04:08.869+01:002014-04-09T10:04:08.869+01:00This comment has been removed by a blog administrator.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-245662015774143454.post-64748288198425033782014-04-09T05:46:42.439+01:002014-04-09T05:46:42.439+01:00This comment has been removed by the author.Mathttps://www.blogger.com/profile/16422227513816380228noreply@blogger.com