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

Dan Kaminsky dan at doxpara.com
Wed Jul 9 21:48:21 UTC 2014


Hell, I'd probably get White Ops to pay a bounty.

I'd *love* to see libtiff (in particular, we're using that for another
project) proven secure.


On Wed, Jul 9, 2014 at 9:30 AM, Thomas Dullien <thomasdullien at google.com>
wrote:

> Go ahead and verify any critical open-source library, without making
> gigantic changes. Examples
> that you may want to try:
>
>   1) zlib
>   2) libtiff
>   3) libpng
>
> Or any ASN1 parser. If you succeed, I will tip my hat to you.
> Alternatively, you may wish
> to talk to someone that has worked on avionics systems that have been
> formally verified
> (A380 avionics + ASTREE). They will be of the same opinion I voiced above.
>
> Cheers,
> Thomas
>
>
> On Wed, Jul 9, 2014 at 9:26 AM, Sven Kieske <svenkieske at gmail.com> wrote:
>
>> -----BEGIN PGP SIGNED MESSAGE-----
>> Hash: SHA1
>>
>> On 09.07.2014 03:00, Thomas Dullien wrote:
>> > 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.
>>
>> Nice theory, but do you have any evidence?
>> Furthermore: What is the
>> definition of legacy code, and what is the definition
>> of rewritten/new code?
>>
>> If the definition of "legacy code" is:
>> legacy code == not checkable code
>> you have won, but I guess that would be a catch 22.
>>
>> kind regards
>>
>> Sven
>> -----BEGIN PGP SIGNATURE-----
>> Version: GnuPG v2.0.22 (MingW32)
>>
>> iQGcBAEBAgAGBQJTvW1NAAoJEAq0kGAWDrqlqFkL/1B16L6O8EB2Z+1LdnLUBnRg
>> 5va43169YjWO7GpQo5TdnxZYO1fZb3mq1paTmMGxsEWBeAD/q4g6pw3U7H1AowZQ
>> PzrLpsDdbRBHd77NGYaDXmQlWiE+ZJqMiwxQM8dtmI7GktAmXWPj1+UX9rQC7Rdw
>> IOJhyM7aMTqx2V20ueJXJZecW6fyOBIIkfK5akNJxdBZkrPeUATnffSzbLPz56EK
>> nfC46sw5YyAzHLoEj2btbTqqA1yvI84Y+SKeO5Q2DaNI0SMfkANqpv0pwcQY8WpF
>> aw6lL4da5MGevmSfvvDdCS2v6X/I6qVOGSsAJSwaZ/xqDmCVyISBGTf/bxGEF8aj
>> YjhuEGJrlzW8RskqhBi/hljSXI06GWJrfXAABCC5NpUVhLqAQZP7vYDyCT+oquKq
>> wpYHXxSfVa88gJAoXs+WNIIzchvRMatpuLjI4024YcIBc2lQ2BwIOvt+g4adgVOV
>> xiDMu0lUqwzEFtxNgDsuDKWIOk+JekIUCwLoaoyx+g==
>> =L0RQ
>> -----END PGP SIGNATURE-----
>> _______________________________________________
>> 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/20140709/d2b4a2a2/attachment-0001.html>


More information about the langsec-discuss mailing list