[langsec-discuss] LZO, subtle bugs, theorem provers
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>
> 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
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss