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

Sergey Bratus sergey at cs.dartmouth.edu
Wed Jul 9 18:05:43 UTC 2014


    Such a challenge would be great to pose for the next year's LangSec
Wokrshop/Conference. Volunteers to work on formulating it?

    Thanks,

--Sergey

On Wed, 9 Jul 2014, Thomas Dullien 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
>>
>


More information about the langsec-discuss mailing list