Splatter calc tamuctf2020, reverse engineering writeup

Apr. 9, 2020

This was originally published on sousse.love

Introduction

We played tamuctf 2020, it was a 10-day-long beginner to intermediate level ctf, 20 teams solved all the problems, we didn’t solve all the problems unfortunately, and we ended in rank 25.

The reverse problems were simple/okay-ish, most of them are in rust.

The challenge

This writeup is about a problem called splatter calc, it’s a rust binary that asks for an initial rng

kali@kali:/mnt/shared/ctfs/tamuctf20/rev$ ./splatter-calc
Please enter an initial rng: 1
Oops, you didn't guess the right number. You got 13896084676171490950 with final state 62298657904
71643905

Analysis of the binary

Here is what the CFG looks like:

This looks really simple for a rust binary.

What interests us in the node in grey.

The code looks like this:

.text:0000555555559945                 mov     eax, ebx
.text:0000555555559947                 and     eax, 7
.text:000055555555994A                 shl     rax, 4
.text:000055555555994E                 mov     rdi, [rsp+rax+138h+var_B0]
.text:0000555555559956                 mov     rax, [rsp+rax+138h+var_A8]
.text:000055555555995E                 mov     esi, 0CAFEBABEh
.text:0000555555559963                 mov     rdx, rbx
.text:0000555555559966                 call    qword ptr [rax+18h]
.text:0000555555559969                 mov     r13, 83F66D0E3h
.text:0000555555559973                 imul    rbx, r13
.text:0000555555559977                 mov     rbp, 24A452F8Eh
.text:0000555555559981                 add     rbx, rbp
.text:0000555555559984                 mov     ecx, ebx
.text:0000555555559986                 and     ecx, 7
.text:0000555555559989                 shl     rcx, 4
.text:000055555555998D                 mov     rdi, [rsp+rcx+138h+var_B0]
.text:0000555555559995                 mov     rcx, [rsp+rcx+138h+var_A8]
.text:000055555555999D                 mov     rsi, rax
.text:00005555555599A0                 mov     rdx, rbx
.text:00005555555599A3                 call    qword ptr [rcx+18h]
.text:00005555555599A6                 imul    rbx, r13
.text:00005555555599AA                 add     rbx, rbp
.text:00005555555599AD                 mov     ecx, ebx
...

Functions are stored in a jump table, they are offsted ecx & 7:

.text:0000555555559966                 call    qword ptr [rax+18h]

I extracted all the functions:

func_0:
mov     rax, rsi
retn

func_1:
lea     rax, [rsi+rdx]
retn

func_2:
mov     rax, rsi
sub     rax, rdx
retn

func_3:
mov     rax, rsi
imul    rax, rdx
retn

func_4:
mov     rax, rsi
imul    rax, rsi
retn

func_5:
mov     rcx, rdx
mov     rax, rsi
shl     rax, cl
retn

func_6:
mov     rcx, rdx
mov     rax, rsi
shr     rax, cl
retn

func_7:
mov     rax, rsi
xor     rax, rdx
retn

Finally the generated value needs to satisfy these constraints:

The algorithm is simple, so I rewrote it in python, if there was some delicate stuff that I couldn’t implement correctly, I could have a used a symbolic execution framework like angr or triton for this.

import z3

s = z3.Solver()

def do_operation(i, rsi, rdx):
    return z3.If((i & 7) == 0,
	       rsi,
	       z3.If((i & 7) == 1,
		     rsi + rdx,
		     z3.If((i & 7) == 2,
			   rsi - rdx,
			   z3.If((i & 7) == 3,
				 rsi * rdx,
				 z3.If((i & 7) == 4,
				       rsi * rsi,
				       z3.If((i & 7) == 5,
					     rsi << (rdx & 8),
					     z3.If((i & 7) == 6,
						   rsi >> (rdx & 8),
						   rsi ^ rdx)))))))

rbx = z3.BitVec("input", 64)
r13 = 0x83F66D0E3
rbp = 0x24A452F8E
rsi = 0xCAFEBABE

for _ in range(8):
    rdx = rbx
    rax = do_operation(rbx, rsi, rdx)
    rbx = rbx * r13
    rbx = rbx + rbp
    ecx = (rbx & 0xffffffff)
    rsi = rax

s.add(0x471DE8678AE30BA1  == rbx)
s.add(0x0ACDEE2ED87A5D886 == rax)

print(s.check())
print(s.model())

And we get the value to use on the remote server

(hacking3) kali@kali:/mnt/shared/ctfs/tamuctf20/rev$ python solver.py
sat
[input = 982730589345]