Verifiably Correct Lifting of Position-Independent x86-64 Binaries (2024)

Real computer science is so cool.

What, you don't think npm's left-pad is cutting edge? :)

So it's a disassembler that preserves formally proven properties?

Usually when you disassemble a binary you can't just add instructions since it messes up the offsets of everything.

This disassembler tries to find all offsets and replace them with symbols that way if instructions are inserted or removed when it gets reassembled the correct offsets are used.

Where is the source code?

https://doi.org/10.5281/zenodo.12721325 Edit: alternatively, https://github.com/ssrg-vt/FoxDec