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

Thomas Dullien thomasdullien at google.com
Wed Jul 9 16:30:55 UTC 2014


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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140709/63f884c3/attachment.html>


More information about the langsec-discuss mailing list