Enable safely using doo files that were verified against other doo files

[keyboardDrummer]

If I have project A, A*, B and C, where B depends on A, C depends on B, and A and A* have the same type signature. Then if I build a.doo and a*.doo, then b.doo (passing in a.doo), and then c.doo (passing in b.doo, and a*.doo), then I can get Dafny to tell me everything verifies successfully, even though the verification done was not sound because a and a* may have different behavior.

Solution

• When building a doo file, store a checksum of its sources in the output file.
• When building a doo file, for each doo file passed to library, store a checksum of that dependency in the output in a list of dependency checksums.
• When building a doo file, ensure that for each doo file passed to library, and each dependency checksum mentioned by that doo file, another doo passed to --library has that checksum.

[robin-aws]

This is a good thing to be concerned about in general.

For the record some language ecosystems deal with this program at a higher-level of tooling instead. For example, .jar files don't include anything like this, and they are roughly equivalent to .doo files, but instead Maven/Gradle maintains checksums on packages.

I do think given Dafny's focus on verified correctness, and the fact that the solution looks cheap, this is worth implementing in the lower-level tooling, even if it ends up duplicative later on.

Note there's also a similar issue when you add translation to the dependency graph:

1. Build A.doo to A.jar
2. Build A*.doo to A*.jar
3. Build B.doo to B.jar, assuming you provided --library A.doo when building B.doo
4. Execute B.jar and A*.jar together, and get crashes/undefined behavior.

The solution to that may look similar, or it may be largely independent. It might be worth splitting it out as a separate issue.

When building a doo file, for each doo file passed to library, store a checksum of that dependency in the output in a list of dependency checksums.

I wonder if it would be more flexible to calculate and check this per module, so it's independent of the .doo bundling. That way you could change how libraries are grouped into .doo files without having to reverify/rebuild consuming libraries.

[keyboardDrummer]

Thanks for the reply!

I wonder if it would be more flexible to calculate and check this per module, so it's independent of the .doo bundling. That way you could change how libraries are grouped into .doo files without having to reverify/rebuild consuming libraries.

Interesting idea. I'll mull it over.

[robin-aws]

Note the solution to the translation integrity version of the problem can probably leverage the .dtr translation record concept we proposed on #5140 as well - if those files also include checksums on the translated code, we just need some extension to the target language environment to trigger checking them at loading/linking time.

[keyboardDrummer]

Note there's also a similar issue when you add translation to the dependency graph

Good point!

I'm thinking of also adding a checksum of the input used to translation records generated when calling dafny translate, and then when you ingest a translation record using --translation-record, Dafny will verify that the same inputs are specified in --library, something like that.

Then when you do dafny translate java bSources --library A.doo --translation-record A.dtr it only works if you provide A.dtr, not if you provide A*.dtr, so it's slightly less like that you would then combine B.jar with A*.jar