[langsec-discuss] LZO, subtle bugs, theorem provers
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?
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.
> 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
>> -----BEGIN PGP SIGNATURE-----
>> Version: GnuPG v2.0.22 (MingW32)
>> -----END PGP SIGNATURE-----
>> langsec-discuss mailing list
>> langsec-discuss at mail.langsec.org
More information about the langsec-discuss