For legacy code, what about sandboxing it and then proving something about the sandbox? Not sure if that's really in the spirit of verification you had in mind.
I think that approach should without much modification for libraries which take a file descriptor as input, return some output, don't touch the network, and don't need temporary files. On Wed, Jul 9, 2014 at 12:30 PM, Thomas Dullien <thomasdull...@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 <svenkie...@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@mail.langsec.org >> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss >> > > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > >
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
