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

Thomas Dullien thomasdullien at google.com
Wed Jul 9 01:00:36 UTC 2014


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 <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
> > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> >
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
> 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/20140708/6f12a4cc/attachment.html>


More information about the langsec-discuss mailing list