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

Peter Johnson pete at cs.dartmouth.edu
Tue Jul 8 04:26:31 UTC 2014


> 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



More information about the langsec-discuss mailing list