Lets see the verified code go a few years without finds. On Tuesday, July 8, 2014, Andrew <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 <javascript:;> > > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org <javascript:;> > 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
