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 <mu...@mimisbrunnr.net> wrote:
This has been done a few times, one recent example is Quark:
http://goto.ucsd.edu/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@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
