[michaelmior]

I don't think you can ever prove that you've found the required files for an arbitrary binary. (I especially have a hard time believing that such a proof would involve fuzzing, which is random.) However, it seems reasonable that you would be able to achieve a high enough level of confidence that this technique would be viable.

[TheLoneWolfling]

You cannot. It reduces to the halting problem, relatively trivially:

    <arbitrary code that cannot open foo.txt>
    do something with foo.txt

This will use foo.txt iff said code halts.

You can, however, prove that you've found a superset of the required files for an arbitrary binary. Or prove that you've found the required files for some, but not all, arbitrary binaries.

[TheDong]

You're wrong.

You cannot say you haven't found all the dependencies, but you can say you have found all the dependencies (given the constraints I placed above).

The halting problem only says that you cannot prove that a given program will halt.

However, you can prove a specific program halts if, in fact, that program halts.

The original question was not "can prove that I can find the dependencies for an arbitrary binary", but "can you prove that all the dependencies were found for a single specific binary".

For some program that has an infinite loop you can say "I don't know if I've found everything", but if you have shown that you have hit every code branch, as I said above, then clearly this program both halts and has had all dependencies found, excepting different behavior for user input within those already explored branches.