diasurgical / diasurgical/devilution
RFC: Verifying the accuracy of decompiled code
- Dominant language
- C++
- Stars
- 9k
- Forks
- 920
- PR merge metrics
- No merged PRs in 30d
Description
One of the issues with the decompiled code (besides the fact that it looks like an IOCCC entry) is that sometimes the decompilation is not accurate.
The current approaches to verification are roughly these I think:
* Stare at it & the disassembly for a long time, tweak it and run it until it looks like the original (I guess the most common so far).
* (side question: is anyone using a debugger on the original code to discover how it works?)
* Tweak it iteratively until the output of VC6 starts to resemble the original assembly (eg. @seritools' PRs)
I have been thinking about more "automated" approaches to this, here's dump of my thoughts on how to do it:
## Proving the new assembly matched the original assembly
Could theoretically use a automated theorem prover / model checker eg. Z3 to prove two pieces of assembly equivalent.
Requires translating x86 assembly to something a theorem prover understands (this has been done).
Might not work for more complicated code. Modeling memory reads/writes is still an open research question.
_Plausibility_: Low, unless you are looking to get a PhD in this field. Nice to dream about.
## Testing the new code and original code
### "Golden" "unit" tests
Write some "unit tests" on parts of the code that are "pure" (do not interact with the outside world), eg. dungeon generation or rendering. (the unit tests would need some "partial initialization" procedures to set up the state of the necessary global variables)
Steps:
* Execute these tests on both the original and new binary.
* Dump the "results".
* Use the original's result as the "golden" reference for comparison.
The input parameters (seeds etc.) could be randomly generated, similar to QuickCheck. Combined with code coverage checking, this could achieve a pretty high level of confidence in the equivalence of the code.
This needs the ability to call into the original binary *and* being able to inspect its global variables.
This could be done by:
* Modifying the original EXE to be a DLL and generating a corresponding import library & headers. (bonus point: allows using a debugger to step through the original code)
* Using a custom PE loader to just load it into the address space and calling it directly.
(note: the new EXE needs a different base virtual address since the original EXE would occupy the default 0x00400000 address)
### Run-time equivalence checking
This is a bit more advanced:
* For the same "pure" parts of the code, execute both in parallel.
* Verify that the state of the world is equal after "leaving" the pure parts.
What's the state of the world? Well, roughly any memory the code can touch, meaning global variables and any heap-allocated blocks.
Matching up / aligning two different "worlds" for comparison might be tricky, so ideally it would execute two different pieces of code on the *same* global state.
To do make the old and new binary operate on the same state, there are two symmetric options:
1. Make the new code's globals be located at the *same* addresses as the original code's.
Problems:
* The decompiled globals do not have the original addresses attached to it in most cases (solvable)
* The compiler places globals however it desires.
This can be worked around though, eg. GCC supports "linker scripts" to manually lay out sections at certain addresses, or we could just directly generate eg. a "stub" assembly file that lays out the global symbols at the original offsets.
2. Make the old code use the new code's offsets.
Approaches:
1) Can dump assembly out of IDA and re-assemble / re-link it with the new code.
2) Run the code using an x86 emulator library and redirect memory accesses to the right place.
(bonus: allows to safely run any code, since it can just stop simulation if it tries to access "off-limits" memory or call something that would have a side effect).
There's also the "minor" problem of undoing the memory writes of eg. the old code after it has executed:
* On Unix, can just `fork()`. Unfortunately, this does not run on Unix currently.
* Copy all the memory to a backup location, then copy it back.
* If using the emulator, can just log all the writes and undo then.
## Summary
As you can see, all of these approaches require a 1:1 mapping between old and new procedures & global variables.
I think an interesting approach to take would be to add a "pseudo-annotation" to the current headers with the address of it in the original code (that can then be extracted by automated tools).
Something like this:
`annotations.h`:
```
#define ADDR(x) // dummy, only used by tools
```
`example.h`:
```
extern int pSomeVar ADDR(0x123456);
void __cdecl SomeFunc(int a1) ADDR(0x123456);
```
This would also allow automatically generating the IDA scripts that are in the `scalpel` repository and make sure they do not get out-dated as we eg. add names to more variables.
Contributor guide
Assessment
This issue has not been assessed yet.