[langsec-discuss] LZO, subtle bugs, theorem provers
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?
> 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
> > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
> langsec-discuss mailing list
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss