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

Robert Graham robert_david_graham at yahoo.com
Sat Jul 12 04:51:24 UTC 2014

That is, of course, what Microsoft ended up doing for its Office file format conversion utilities. After decades of being the most popular software, there exists a huge number of buggy files that none-the-less work with the existing code. The code couldn't follow the official file-format spec -- it had to be "bug complete" with the existing buffy files. The code has reached the state where it's untestable. Minor changes, no matter how benign, and no matter how well they pass the existing regression test, will result in some documents not converting properly. Thus, they sandbox the file conversion.

That shouldn't be a problem here. These file formats are standard with many implementations, so there's little need to be bug complete.

I'm not sure what you guys consider "major changes to the code". When you have a robust unit/regression test, then major refactorings of the code are fairly painless. You should therefore be able to make massive changes to a zlib/libtiff/libpng library to support verifiability, and be assured that your changes haven't broken the code. Conversely, one of these codebases doesn't have an extension unit/regression test that would support such refactoring, then that's a more urgent problem that needs to be fixed before making the code verifiable.

On Friday, July 11, 2014 1:05 PM, Andrew <munin at mimisbrunnr.net> wrote:

This has been done a few times, one recent example is Quark:

On 07/11/2014 01:02 PM, Sven Kieske wrote:
> On 11.07.2014 17:58, Matt DeMoss wrote:
>> 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.
> Well if your sandbox would be proven to be secure there is still
> the problem: How does the legacy code behave inside the sandbox? Is
> it acceptable that it maybe just breaks when the sandbox refuses to
> do $x ? So to my understanding you must not just prove the sandbox
> itself, rather show that the interaction between sandbox and legacy
> code are "ok".
> Without going into details or a specific example I still got the
> feeling this could be more complex than just proving the legacy
> code/rewrite that code.
> kind regards
> Sven _______________________________________________ 
> langsec-discuss mailing list langsec-discuss at mail.langsec.org 
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss

langsec-discuss mailing list
langsec-discuss at mail.langsec.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140711/0451852f/attachment-0001.html>

More information about the langsec-discuss mailing list