✧✦Catherine✦✧
finally solved a crackme that was rated "medium" by, i think, its author, by extracting a cryptographic algorithm from an embedded virtual machine i had to reverse-engineer the ISA spec for, reimplementing it in Amaranth and then feeding it into yosys-smtbmc to invert the fairly complex scrambling function with XOR diffusion, various permutations, etc
im terrified to consider what would be rated "hard"
✧✦Catherine✦✧
i spent two out of three days chasing down a single bit (i thought the comparison operation has "equal", "not equal", and "less than" flags, but it has "equal", "not equal and not less than", and "less than" flags). since the input to the scrambling function is 128-bit, every time i would feed the execution trace into the SMT solver it would attempt to enumerate every 128-bit integer to prove me wrong, which doesn't work
✧✦Catherine✦✧
i was emotionally obliterated when i thought that i'm insufficiently good at cryptanalyzing this scrambling function (with my approach being an SMT solver but it never terminating), i looked up how they broke MD4, and it was "hook it up to an SMT solver"
well, it turns out that works if you implement the ISA right
✧✦Catherine✦✧
reverse-engineering a VM implementation embedded in a Linux binary with anti-debug measures to extract its ISA spec: easy
correctly reading this code fragment on first, second, third, or fourth try: mission fucking impossible
i filed https://github.com/Vector35/binaryninja-api/issues/6674
✧✦Catherine✦✧
im also pleased to report that lifting the VM code to Amaranth and using SMTBMC went better than using angr or KLEE. i'm inexperienced with the latter two but someone else also tried it and didn't get far
yay for hardware tools?
✧✦Catherine✦✧
probably the single most "i am about to give up" moment was me concluding that i need to do a first preimage attack on a cryptographic function with nontrivial diffusion properties (flipping one bit anywhere changes basically the entire 16 byte output), i went to study and found out that basically no serious hash function has ever had a practical first preimage attack executed on it
✧✦Catherine✦✧
after that i considered brute-forcing it using a Kintex UltraScale FPGA that i had around (and i calculated that with the alphabet limited to 0-9 i could do it) but stopped because it felt unlikely that the intended solution to a "medium" crackme with "Level 1" in the title would involve $6000 worth of specialized hardware
this wouldn't have worked anyway because the function implements a bijection, and also because i misunderstood what the alphabet is and it wasn't 0-9
dram🎀
@whitequark i can't even read this right knowing the answer that's amazingly confusing
✧✦Catherine✦✧
@dramforever i had to write this gdb script (x: pc flag reg mem) and then make my emulator emit the same format of hexdump and diff it to figure out where the fuck it went wrong
✧✦Catherine✦✧
@dramforever and yes, you can make gdb execute a continue command when it hits a watchpoint
dram🎀
@whitequark cosim testing ❤
✧✦Catherine✦✧
@SDRHoernchen like what?
SDRHoernchen
@whitequark now do fpga stuff with klee/angr.
✧✦Catherine✦✧
i implemented a custom concolic execution engine[1] for this crackme, but it didn't work out: at the beginning of it, there is code that checks for an alphabet, smth like:
if x == '(': break
if x in 'a'..'z': break
goto fail
i split the solver state on each branch, which doesn't work out well for me: it means i will do a graph search of like 6**32 branches, which will take very long
state merging is hard
[1]: https://gist.github.com/whitequark/e8c7ffab0208d1b033aae715488881d6
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.