I'd like to get a copy of their "PolarSSL Verification Kit" but it seems to be hidden behind a "pay us" link. However, what I am able to read from the authors so far the answers seems to be:
a. all of it b. none of it I'd love to see more information of course and ideally see the analysis run myself. It definitely sounded like they spent a lot of work doing modeling / precondition specification as well as analysis tuning to verify PolarSSL, which sounds like a lot of work. However, they did it, and apparently without re-writing PolarSSL, so... On 07/08/2014 09:00 PM, Thomas Dullien wrote: > Please check up on a) how much of the code is formally verified and b) > how much > of the code was rewritten to make that feasible :-) > > Nobody is saying you can't write checkable code. All I am saying that > for most / all > of our legacy code, making it checkable is equivalent to rewriting it. > > Cheers, > Thomas/Halvar > > > On Tue, Jul 8, 2014 at 5:49 PM, Andrew <mu...@mimisbrunnr.net > <mailto:mu...@mimisbrunnr.net>> wrote: > > How does all of this pessimism about the application of static analysis > and formal methods applied to legacy code square with the existence of a > formally verified SSL/TLS stack written in C? > > http://www.pl-enthusiast.net/?p=184#comment-96 > > http://trust-in-soft.com/polarssl-verification-kit/ > > On 07/08/2014 12:26 AM, Peter Johnson wrote: > >> It seems likely then that verification only works on the subset of > >> expressiveness that can be cowritten in the free and the constrained > >> language. i.e. we aren't verifying c at all. > > > > Isn't this a direct consequence of C being Turing-complete and > therefore not > > verifiable in the general case? That is, we know C gives you more > than enough > > rope to hang yourself with and therefore we want to encourage > people to use C > > in ways that are explicitly verifiable. To me, you've concisely > summed up > > exactly what (I think) LangSec is all about! > > > > pete > > > > _______________________________________________ > > langsec-discuss mailing list > > langsec-discuss@mail.langsec.org > <mailto:langsec-discuss@mail.langsec.org> > > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org > <mailto:langsec-discuss@mail.langsec.org> > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > > _______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
