There are always assumptions in all verification projects, presumably the report spells them out.
It is interesting that PolarSSL still get vulnerabilities from time to time, e.g. a buffer overflow https://polarssl.org/tech-updates/security-advisories/polarssl-security-advisory-2013-04 despite claiming being "immune to CWE 119". Regards, Vitaly On Wed, Jul 9, 2014 at 11:06 AM, Andrew <mu...@mimisbrunnr.net> wrote: > 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 _______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
