Reverse Engineering for Beginners

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

};

By simple reducing, we finally see that it’s calculating the remainder, not thequotient:

uint64_t f(uint64_t input)

{

uint64_t rax, rbx, rcx, rdx, r8;

rax=input;

rax*=0x5D7E0D1F2E0F1F84;

rax=_lrotr(rax, rax&0xF); // rotate right

rax^=0x388D76AEE8CB1500;

rax=_lrotl(rax, rax&0xF); // rotate left

r8=rax+0xD2E9EE7E83C4285B;

return _lrotl (r8, r8 % 60); // rotate left

};

We end up with this fancy formatted source-code:

#include <stdio.h>

#include <stdint.h>

#include <stdbool.h>

#include <string.h>

#include <intrin.h>

#define C1 0x5D7E0D1F2E0F1F84

#define C2 0x388D76AEE8CB1500

#define C3 0xD2E9EE7E83C4285B

uint64_t hash(uint64_t v)

{

v*=C1;

v=_lrotr(v, v&0xF); // rotate right

v^=C2;

v=_lrotl(v, v&0xF); // rotate left

v+=C3;

v=_lrotl(v, v % 60); // rotate left

return v;

};

int main()

{

printf ("%llu\n", hash(...));

};

Since we are not cryptoanalysts we can’t find an easy way to generate the input value for some specific output value. The

rotate instruction’s coefficients look frightening—it’s a warranty that the function is not bijective, it has collisions, or, speaking

more simply, many inputs may be possible for one output.

Brute-force is not solution because values are 64-bit ones, that’s beyond reality.

77.2 Now let’s use the Z3 SMT solver.

Still, without any special cryptographic knowledge, we may try to break this algorithm using the excellent SMT solver from

Microsoft Research named Z3^1. It is in fact theorem prover, but we are going to use it as SMT solver. Simply said, we can

think about it as a system capable of solving huge equation systems.

Here is the Python source code:

1 from z3 import *
2
3 C1=0x5D7E0D1F2E0F1F84
4 C2=0x388D76AEE8CB1500
5 C3=0xD2E9EE7E83C4285B
6
7 inp, i1, i2, i3, i4, i5, i6, outp = BitVecs('inp i1 i2 i3 i4 i5 i6 outp', 64)

(^1) http://go.yurichev.com/17314