[langsec-discuss] LZO, subtle bugs, theorem provers
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
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.
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?
> 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
> > verifiable in the general case? That is, we know C gives you more than
> > 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
> > 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss