This is really cool work. The particular spec structure/methodology does seem awkward though:
1. Prove the ASan-instrumented binary doesn't crash
2. Prove the non-instrumented binary doesn't crash
3. Prove the instrumented and non-instrumented binaries have the same behaviour (under a particular model of a Linux process's behaviour)
This is a clever hack for automatically generating a formal spec for an existing program, but the fact that you need ASan in there makes it seem like this is less general than it sounds. Could the agents directly prove that out of bounds memory accesses don't occur on the original binary and skip ASan altogether? It's convenient to let the spec just be "it doesn't crash", and ASan provides a crash when the other bad things you care about happen (i.e. out of bounds memory accesses), but I wonder if modelling the memory accesses directly would simplify things.
What does "out of bounds" mean at the ISA level? By the time you have a binary, you've lost all the information about which memory is which.
But you're right that don't need ASan at all if you've encoded semantically meaningful properties. E.g., if you assert(decompress(compress(x)) == x), proving that you don't crash requires proving that compression round-trips. (Similarly if you have a reference implementation.)
The upshot is that the spec doesn't need to be written in a proof assistant and can instead be encoded as an end-to-end test.
1. Prove the ASan-instrumented binary doesn't crash
2. Prove the non-instrumented binary doesn't crash
3. Prove the instrumented and non-instrumented binaries have the same behaviour (under a particular model of a Linux process's behaviour)
This is a clever hack for automatically generating a formal spec for an existing program, but the fact that you need ASan in there makes it seem like this is less general than it sounds. Could the agents directly prove that out of bounds memory accesses don't occur on the original binary and skip ASan altogether? It's convenient to let the spec just be "it doesn't crash", and ASan provides a crash when the other bad things you care about happen (i.e. out of bounds memory accesses), but I wonder if modelling the memory accesses directly would simplify things.