[langsec-discuss] LZO, subtle bugs, theorem provers

Dan Kaminsky dan at doxpara.com
Wed Jul 9 16:28:32 UTC 2014


Lets see the verified code go a few years without finds.

On Tuesday, July 8, 2014, Andrew <munin at 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 at mail.langsec.org <javascript:;>
> > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> >
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org <javascript:;>
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140709/01f270a3/attachment.html>


More information about the langsec-discuss mailing list