CHAPTER 77. HAND DECOMPILING + Z3 SMT SOLVER CHAPTER 77. HAND DECOMPILING + Z3 SMT SOLVER

Chapter 77

Hand decompiling + Z3 SMT solver

Amateur cryptography is usually (unintentionally) very weak and can be broken easily—for cryptographers, of course.

But let’s pretend we are not among these crypto-professionals.

Here is one-way hash function (read more about them:34 on page 437), that converted a 64-bit value to another and we
need to try to reverse its flow back.

77.1 Hand decompiling.

Here its assembly language listing inIDA:

sub_401510 proc near
; ECX = input
mov rdx, 5D7E0D1F2E0F1F84h
mov rax, rcx ; input
imul rax, rdx
mov rdx, 388D76AEE8CB1500h
mov ecx, eax
and ecx, 0Fh
ror rax, cl
xor rax, rdx
mov rdx, 0D2E9EE7E83C4285Bh
mov ecx, eax
and ecx, 0Fh
rol rax, cl
lea r8, [rax+rdx]
mov rdx, 8888888888888889h
mov rax, r8
mul rdx
shr rdx, 5
mov rax, rdx
lea rcx, [r8+rdx*4]
shl rax, 6
sub rcx, rax
mov rax, r8
rol rax, cl
; EAX = output
retn
sub_401510 endp

The example was compiled by GCC, so the first argument is passed inECX.

If you don’t have Hex-Rays or if you distrust to it, you can try to reverse this code manually. One method is to represent the
CPUregisters as local C variables and replace each instruction by a one-line equivalent expression, like:

uint64_t f(uint64_t input)
{
uint64_t rax, rbx, rcx, rdx, r8;

ecx=input;

rdx=0x5D7E0D1F2E0F1F84;