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

Andrew munin at mimisbrunnr.net
Wed Jul 9 00:49:45 UTC 2014


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
> 


More information about the langsec-discuss mailing list