tl;dr

  • This is a fairly simple Maze challenge
  • Challenge is written in rust

Challenge author: Freakston, silverf3lix

Descrption

Senpai plis find me a way.

Solution

This is a fairly simple maze challenge implemented in rust.

At the start of the main function of the challenge miz we can see there is a some sort of a initialization going on at a function named miz::bacharu::Kikai::new::h3a113b790cc2bb5c

We can see from here than this function takes care of initializing the maze. We can extract the maze bytes either directly from here or during runtime, which ever is preferred.

Moving forward we can see that the function is also getting our input, and sending it over to another function miz::bacharu::Kikai::run::h14398f1fc265e61e

The function miz::bacharu::Kikai::run takes care of the maze logic, the up, left, down and right.

  • Case “h”

We can see that the case “h” takes care of going left, which is by subtracting 1 from the y coordinate

  • Case “j”

Similarly, case “j” is to go up, it does this by subtracting 1 from the x coordinate.

  • Case “k”

Case “k” takes care of going down the maze, it adds 1 to the x coordinate

  • Case “l”

This case takes care of going right in the maze, it does so by adding 1 to the y coordinate

From this function we can also get the bounds of the maze which is 24 x 25, where there are 25 rows and 24 columns.

And the properties of the maze are,

  • “0” ⇒ Path to traverse
  • “1” ⇒ Walls
  • “2” ⇒ Final win position

We can also see that this is the function miz::bacharu::Kikai::Furagu_o_toru::hd3e3c2fb2ccf3552 is the win function, and this is called when we traverse till we reach the number 2 in the maze.

Constructing the maze should be easy since we have its bounds,

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
miz =       [[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
            ,[1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,0,1]
            ,[1,0,1,0,1,1,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,0,1,0,1]
            ,[1,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,1,0,0,0,1,0,0,0,1]
            ,[1,0,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,1,1,0,1,1,1,1,1]
            ,[1,0,0,0,0,0,0,0,1,0,1,0,0,0,1,0,0,0,0,0,1,0,0,0,1]
            ,[1,0,1,1,1,1,1,0,1,1,1,0,1,0,1,1,1,0,1,1,1,1,1,0,1]
            ,[1,0,0,0,1,0,1,0,0,0,0,0,1,0,0,0,1,0,0,0,1,0,0,0,1]
            ,[1,1,1,0,1,0,1,0,1,1,1,1,1,1,1,0,1,1,1,0,1,0,1,1,1]
            ,[1,0,1,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1]
            ,[1,0,1,0,1,1,1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1]
            ,[1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,1]
            ,[1,0,1,0,1,0,1,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,1,0,1]
            ,[1,0,0,0,1,0,0,0,1,0,0,0,1,0,1,0,0,0,1,0,0,0,1,0,1]
            ,[1,0,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,1,0,1]
            ,[1,0,0,0,1,0,0,0,0,0,0,0,1,0,1,0,0,0,1,0,0,0,0,0,1]
            ,[1,0,1,0,1,0,1,1,1,1,1,1,1,0,1,0,1,1,1,0,1,1,1,0,1]
            ,[1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,1,0,1,0,1]
            ,[1,0,1,1,1,1,1,0,1,1,1,1,1,1,1,1,1,0,1,0,1,0,1,0,1]
            ,[1,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,1,0,1]
            ,[1,0,1,1,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,0,1,0,1]
            ,[1,0,0,0,0,0,0,0,1,0,0,0,0,0,1,0,1,0,0,0,1,0,1,0,1]
            ,[1,1,1,0,1,0,1,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,1,0,1]
            ,[1,0,0,0,1,0,0,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,1,0,1]
            ,[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1]]

The start position can be retrieved while debugging and it is (0, 13). The end position is

(24, 19)

Final script

To solve this maze we can make use of the python library mazelib

Here is the script,

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
from mazelib import Maze
from mazelib.solve.BacktrackingSolver import BacktrackingSolver
import numpy as np
m = Maze()
m.solver = BacktrackingSolver()
miz =       [[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
            ,[1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,0,1]
            ,[1,0,1,0,1,1,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,0,1,0,1]
            ,[1,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,1,0,0,0,1,0,0,0,1]
            ,[1,0,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,1,1,0,1,1,1,1,1]
            ,[1,0,0,0,0,0,0,0,1,0,1,0,0,0,1,0,0,0,0,0,1,0,0,0,1]
            ,[1,0,1,1,1,1,1,0,1,1,1,0,1,0,1,1,1,0,1,1,1,1,1,0,1]
            ,[1,0,0,0,1,0,1,0,0,0,0,0,1,0,0,0,1,0,0,0,1,0,0,0,1]
            ,[1,1,1,0,1,0,1,0,1,1,1,1,1,1,1,0,1,1,1,0,1,0,1,1,1]
            ,[1,0,1,0,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1]
            ,[1,0,1,0,1,1,1,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,1]
            ,[1,0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,1]
            ,[1,0,1,0,1,0,1,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,1,0,1]
            ,[1,0,0,0,1,0,0,0,1,0,0,0,1,0,1,0,0,0,1,0,0,0,1,0,1]
            ,[1,0,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,1,0,1]
            ,[1,0,0,0,1,0,0,0,0,0,0,0,1,0,1,0,0,0,1,0,0,0,0,0,1]
            ,[1,0,1,0,1,0,1,1,1,1,1,1,1,0,1,0,1,1,1,0,1,1,1,0,1]
            ,[1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,1,0,1,0,1]
            ,[1,0,1,1,1,1,1,0,1,1,1,1,1,1,1,1,1,0,1,0,1,0,1,0,1]
            ,[1,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,1,0,1]
            ,[1,0,1,1,1,1,1,1,1,1,1,1,1,0,1,0,1,1,1,1,1,0,1,0,1]
            ,[1,0,0,0,0,0,0,0,1,0,0,0,0,0,1,0,1,0,0,0,1,0,1,0,1]
            ,[1,1,1,0,1,0,1,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,1,0,1]
            ,[1,0,0,0,1,0,0,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,1,0,1]
            ,[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]]
m.grid = np.array(miz)
m.start = (0,13)
m.end = (24,19)
m.solve()
sol = m.solutions[0]

for i in range(len(sol)-1):
    x = sol[i][0]
    y = sol[i][1]
    xn = sol[i+1][0]
    yn = sol[i+1][1]
    #print(f"x -> {x} y- >{y}  xn -> {xn} yn -> {yn}")
    if (x - xn) > 0:
        print("j",end="")
    elif (y - yn) > 0:
        print("h",end="")
    elif (yn - y) > 0:
        print("l",end="")
    elif (xn - x) > 0:
        print("k",end="")

The final moves to be sent as input comes out to be,

llkkhhhhkkkkhhhhjjhhhhhhkkllkkkkkkhhkkllkklljjlllllljjhhjjllllllkklljjllkklljjllkkkkhhhhkkkkllkkkkhh

Flag: inctf{mizes_are_fun_or_get}

InCTFi Linux Reversing Maze Rust

tl;dr

  • This is a simple stack based VM
  • 25-27 opcodes and 8 different constraints
  • Extract the constraints
  • Use z3 to find a satisfying model

Challenge Points: 245
Challenge Solves: 20
Challenge author: EvilMuffinHa
Solved by: AmunRha, Freakston, barlabhi

Description

Introduction

This is a simple VM which has around 25-27 opcodes with instructions simple enough to be emulated. This is a stack based VM.

The VM implements several constraints on the input bytes which can be solved using z3 SMT solver.

The VM implemented a puzzle called kenken

Solution

I chose python to write the disassembler in with several helper functions, at first I tried extracting the constrains one by one, which eventually worked, but then I was able to write a automatic extractor for the disassembly.

There were two files, one the binary and the data file in which the list of instructions contain.

This when fed to the z3 solution script will get us the required input.

Most of the operations take their operands from the stack, so there wasn’t much complexity in terms of implementation.

p.s. This will be a short write up

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
def disasm(op, c):
    if c > dump_len:
        return -1
    # print(f"\n[{hex(op):<3}]:[{hex(c):<3}]\t")
    # print("MOV dctr, ctr1+1")
    # print(op_desc[op]+'\n')
    extract(op,rsp,ctr1)

    dctr = ctr1 + 1
    if op == 0x1:
        rsp.append(rsp[-1])
        ctr1+=1
    elif op == 0x2:
        rsp = rsp[:-1]
        ctr1+=1   
    elif op == 0x3:
        if rsp[-1] == -1:
            rsp = rsp[:-1]
            ctr1+=1
        elif rsp[-1] != 0:
            print(f"[+] RETURN: {rsp[-1]}")
            return -1
        else:
            print("[+] READING FLAG FILE")
            return 1
    elif op == 0x10:
        rsp[-2] = rsp[-1] + rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1    
    elif op == 0x11:
        rsp[-2] = rsp[-1] - rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1   
    elif op == 0x12:
        rsp[-2] = rsp[-1] * rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1     
    elif op == 0x13:
        rsp[-2] = rsp[-1] // rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1    
    elif op == 0x14:
        rsp[-2] = rsp[-1] % rsp[-2]
        rsp = rsp[:-1]
        ctr1+=1   
    elif op == 0x15:
        tmp = rsp[-1]
        rsp.pop(-1)
        res = rsp[-2]*rsp[-1]%tmp
        rsp = rsp[:-2]
        rsp.append(res)
        ctr1 = dctr  
    elif op == 0x16:
        rsp[-2] = 1 if rsp[-1] == rsp[-2] else 0
        ctr1+=1
        rsp = rsp[:-1]    
    elif op == 0x17:
        if rsp[-1] < 0:
            rsp[-1] = -1
        elif rsp[-1] > 0:
            rsp[-1] = 1
        ctr1+=1   
    elif op == 0x20:
        rsp.append(inp[ii])
        ii+=1
        ctr1 = dctr  
    elif op == 0x21:
        v30 = rsp[-1]
        rsp = rsp[:-1]
        ctr1 = dctr
        print(chr(v30))
        output.append(v30) 
    elif op == 0x22:
        ctr1+=3
        rsp.append((f[dctr+1]<<8) | f[dctr]) 
    elif op == 0x30:
        v30 = rsp.pop(-1)
        ctr1 = abs(v30)  
    elif op == 0x31:
        if rsp[-2] != 0:    #  Adjust/Remove the condition in order to extract
            rsp = rsp[:-2]  #  all equations with test input
            ctr1+=1         #  Keep it if using valid input
        else:
            ctr1 = rsp[-1]
            rsp = rsp[:-2]   
    elif op == 0x32:
        if rsp[-2] != 0:     #  Adjust/Remove the condition in order to extract
            ctr1 = rsp[-1]   #  all equations with test input
            rsp = rsp[:-2]   #  Keep it if using valid input
        else:
            rsp = rsp[:-2]
            ctr1+=1   
    elif op == 0x33:
        if rsp[-2] < 0:
            ctr1 = rsp[-1]
            rsp = rsp[:-2]
        else:
            rsp = rsp[:-2]
            ctr1+=1    
    elif op == 0x34:
        if rsp[-2] <= 0:
            rsp = rsp[:-2]
            ctr1+=1
        else:
            ctr1 = rsp[-1]
            rsp = rsp[-2]   
    elif op == 0x35:
        if rsp[-2] > 0:
            rsp = rsp[:-2]
            ctr1+=1
        else:
            ctr1 = rsp[-1]
            rsp = rsp[-2]    
    elif op == 0x36:
        if rsp[-2] >= 0:
            ctr1 = rsp[-1]
            rsp = rsp[:-2]
        else:
            rsp = rsp[:-2]
            ctr1+=1    
    elif op == 0x40:
        v33 = rsp.pop(-1)
        data[v13] = v33
        ctr1 = dctr    
    elif op == 0x41:
        ctr1+=1
        rsp.append(data[v13])   
    elif op == 0x50:
        v13+=1
        ctr1+=1   
    elif op == 0x51:
        v13-=1
        ctr1+=1    
    elif op == 0x52:
        v13 = (rsp[-1]+v13) & 0xff
        ctr1+=1
        rsp = rsp[:-1]    
    elif op == 0x53:
        v13 = (v13 - rsp[-1]) & 0xff
        ctr1+=1
        rsp = rsp[:-1]            
    else:
        print(f"""[!] UNKNOWN OPCODE: {hex(op)}""", end='')
        return -1

    # print_stack(rsp)
    # print_data(data)
    # print_reg(v13,ctr1,dctr,ii)
    return ctr1

Commenting the lines specified can get us the extracted constrains.

I wrote a small parser on my disassembly which will get the proper constraints.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
equations = {"add_2":[], "add_3":[], "equate_3": [], "equate_4":[], "mod_equate_2":[], "sub_2":[], "equal_2":[]}
def parse(bbl, f):
    PUSH_OPERAND = [0x22, 0x52, 0x41]
    SUB_2 = (16,2)
    EQUATE_3 = (21,3)
    EQUATE_4 = (28,4) 
    ADD_2 = (13,2)
    ADD_3 = (19,3)
    MOD_EQUATE_2 = (64,2)
    EQUAL_2 = (7,2)

    for llist in bbl:
        eq = []
        bbl_len = len(llist)
        i = 1
        while True:
            if i+2 >= bbl_len:
                break
            if [llist[i][0],llist[i+1][0],llist[i+2][0]] == PUSH_OPERAND:
                ctr = llist[i][1]
                res = f[ctr+1]
                eq.append(res)
                i+=3
            i+=1
        ctr = llist[0][1]
        res = [f[ctr+1]]
        if bbl_len == SUB_2[0]:
            eq = eq[:SUB_2[1]] + res
            equations["sub_2"].append(eq)
        elif bbl_len == EQUATE_3[0]:
            eq = eq[:EQUATE_3[1]] + res
            equations["equate_3"].append(eq)
        elif bbl_len == EQUATE_4[0]:
            eq = eq[:EQUATE_4[1]] + res
            equations["equate_4"].append(eq)
        elif bbl_len == ADD_2[0]:
            eq = eq[:ADD_2[1]] + res
            equations["add_2"].append(eq)
        elif bbl_len == ADD_3[0]:
            eq = eq[:ADD_3[1]] + res
            equations["add_3"].append(eq)
        elif bbl_len == MOD_EQUATE_2[0]:
            eq = eq[:MOD_EQUATE_2[1]] + res
            equations["mod_equate_2"].append(eq)
        elif bbl_len == EQUAL_2[0]:
            eq = eq[:EQUAL_2[1]] + res
            equations["equal_2"].append(eq)
    return equations

There were in total 8 different constraints applied on the input bytes, which was added to z3. 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
def set_idx(set_to):
    for i in set_to:
        s.add(f[i[0]] == i[1])

def sub2(s_list):
    for i in s_list:
        s.add(f[i[1]] - f[i[0]] == i[2])

def add2(a2_list):
    for i in a2_list:
        s.add(f[i[0]]+f[i[1]] == i[2])

def add3(a3_list):
    for i in a3_list:
        s.add(f[i[0]]+f[i[1]]+f[i[2]] == i[3])

def equate3(e3_list):
    for i in e3_list:
        res = (f[i[2]]*f[i[1]])%0x7fff
        s.add((f[i[0]]*res)%0x7fff == i[3])

def equate4(e4_list):
    for i in e4_list:
        res = (f[i[3]]*f[i[2]])%0x7fff
        res = (f[i[1]]*res)%0x7fff
        s.add((f[i[0]]*res)%0x7fff == i[4])

def mod_equate2(m2_list):
    for i in m2_list:
        s.add((f[i[1]] % f[i[0]]) * (f[i[0]] % f[i[1]]) == 0)
        s.add(f[i[0]] != f[i[1]]) 
        s.add(UDiv((UDiv(f[i[1]], f[i[0]]) + UDiv(f[i[0]], f[i[1]])),1) == i[2])

def distinct_add():
    for i in off:
        s.add(f[i[0]] != f[i[1]])

Running the script gives us the disassembly, and the extracted constraints

and pasting the extracted constraints to z3, gives us the input to be given,

pB738150rHt60714NP501s92420G3xUY013;Wo{=69h42Ob736B1y{@?1047uw`6

Sending this over the given nc connection, gives us the flag,

Flag: flag{kenken_is_just_z3_064c4}

Links to required files,
2k Disassembler Script - 2k_disassembler.py
Helper Script - helper.py
z3 solver script - z3_solver.py

Linux VM Reversing

tl;dr

  • Challenge is a VM implemented over signals and ptrace
  • Reverse Instruction types and implementation
  • Use gdb scripting to find the executed code and get the pseudo VM code
  • Find out the algorithm (Max triangle sum) from VM instructions
  • Find an more optimized way to solve the problem (Or lazy solve it!).

Challenge Points: 769
Challenge Solves: 7
Solved by: R3x

Initial Analysis

Initial analysis shows us that there are minor changes between this binary and the signal_vm binary - in the way the VM works. Please refer to the writeup of signal_vm for learning about the VM structure.

VM structure

In the first stage of the challenge - we had access to all of the VM registers since they were all in the parent itself. Now in signal_vm_de1ta they are all in the memory space of the child - This makes it hard for us to track what is happening in the VM since we aren’t able to directly view its memory or registers.

The VM uses the same four signals (SIGTRAP, SIGILL, SIGSEGV and SIGFPE) to serve as instruction classes. However there are a few significant differences from the first stage.

The VM(parent) uses PTRACE_PEEKDATA and PTRACE_POKEDATA to read and write data into the child memory which contains the memory and the registers.

Retrieving VM instructions

We tweaked the script for the old challenge to work for this one. Since we don’t have the register and memory states this time as that happens in the child, we decided to go ahead and write our own code to parse the instructions. So we were able to predict the contents of the VM registers accurately which helped us in figuring out what the child did.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
import gdb
import struct

class Regs(object):
    reg = [0] * 10
    eflags = 0
    flag = [48] * 0x80 + [0] * 0x100 + [10] * 5050

    def __repr__(self):
        final = "-------------------\n"
        for i in range(len(self.reg)):
           final += "\tRegister "+str(i)+" : "+str(self.reg[i]) + " | " + hex(self.reg[i]) + "\n"
        final += "\tEflags = " + str(self.eflags) + " | " + hex(self.eflags) + "\n"
        final += "\tFLAG = [[ " + "".join(map(chr, self.flag[:102])) + "]]\n"
        final += "------------------\n"
        return final

    def copy_reg(self, i, j):
        if i < 10:
            self.reg[i] = self.reg[j]
        else:
            self.eflags = self.reg[j]

    def copy_val(self, i, data):
        if i < 10:
            self.reg[i] = data
        else:
            self.eflags = data
    
    def flag_to_reg(self, src, dest):
        self.reg[src] = self.flag[self.reg[dest]]

    def reg_to_flag(self, src, dest):
        self.flag[self.reg[src]] = self.reg[dest]
        
    def operation(self, src, op, dest):
        self.reg[src] = eval("%d %s %d" % (self.reg[src], op , dest))
   
    def operation_reg(self, src, op, dest):
        self.reg[src] = eval("%d %s %d" % (self.reg[src], op ,self.reg[dest]))

    def update_eflag(self, dest, const):
        self.eflags = self.reg[dest] - const        

    def update_eflag_reg(self, dest, othreg):
        self.eflags = self.reg[dest] - self.reg[othreg]

class Opcode:
    opcode = ""
    val1 = 0
    const = 0
    src = 0
    dest = 0
    final = 0
    final2 = 0
    
    def __init__(self, opcode):
        self.opcode = opcode
        test = struct.unpack("<Q", int(opcode, 16).to_bytes(8, byteorder='big'))[0]
        self.val1 = test >> 56
        self.const = (test >> 48) & 0xff
        self.src = (test >> 40) & 0xff
        self.dest = (test >> 32) & 0xff
        self.final = struct.unpack("<I", ((test & 0xffffffff00) >> 8).to_bytes(4, byteorder='big'))[0]      
        self.final2 = struct.unpack("<I", (test & 0xffffffff).to_bytes(4, byteorder='big'))[0]

    def __repr__(self):
        str_out = "-------------------\n"
        str_out += "OPCODE : %s  |  %d\n" % (self.opcode, int(self.opcode, 16) ) 
        str_out += "val1 = %d | const = %d | src = %d | dest = %d\n" % (self.val1, self.const, self.src, self.dest)
        str_out += "val1 = %s | const = %s | src = %s | dest = %s\n" % (hex(self.val1), hex(self.const), hex(self.src), hex(self.dest))
        str_out += "final = %d    |   final2 =  %d \n" % (self.final, self.final2)
        str_out += "-------------------\n"
        return str_out
        

sig = {4: "SIGILL", 5 : "SIGTRAP", 8: "SIGFPE", 0xb: "SIGSEGV" }
mov_ins = {0: "%d: mov r%d r%d\n",1: "%d: mov r%d 0x%x\n" ,2: "%d: mov r%d [r%d]\n", 32: "%d: mov [r%d] r%d\n"}
ops = ["add" , "sub" ,  "mul" , "div" , "mod" , "or" , "and" , "xor" , "lsh" , "rsh"]
op_sym = ["+", "-", "*", "/", "%", "|", "&", "^", "<<", ">>"]
str_ops = ["%d: %s r%d r%d\n", "%d: %s r%d 0x%x\n"]
jmp = ["", "eq", "neq", "le", "lt", "ge", "gt"]

f = open('ins.out', 'w')

gdb.execute("file signal_vm_de1ta")
gdb.execute("set pagination off")
gdb.execute("b * 0x400CB2")
gdb.execute("b * 0x0400CB9")
gdb.execute("b * 0x0400CEC")
gdb.execute("b * 0x401062")

gdb.execute("r")
regs = Regs()

for i in range(20000):
    opcode = gdb.execute("p/x $rax", to_string=True).split("=")[1].strip()
    gdb.execute("c")

    sig = gdb.execute("p/x $al", to_string=True).split("=")[1].strip()
    gdb.execute("c")

    op = Opcode(opcode)    
    print(op)

    if int(sig, 16) == 5:
        opcode = gdb.execute("p/x $rax", to_string=True).split("=")[1].strip()
        gdb.execute("c")
        new_op = Opcode(opcode)

        if new_op.const == 1:
            f.write(mov_ins[new_op.const] % (i, new_op.src, new_op.final))
        else:
            f.write(mov_ins[new_op.const] % (i, new_op.src, new_op.dest))

        if new_op.const == 1:
            regs.copy_val(new_op.src, new_op.final)
        elif new_op.const == 0:
            regs.copy_reg(new_op.src, new_op.dest)
        elif new_op.const == 2:
            regs.flag_to_reg(new_op.src, new_op.dest)
        elif new_op.const == 32:
            regs.reg_to_flag(new_op.src, new_op.dest)
        else:
            f.write("\n ############ERROR################ \n")

        #f.write(new_op.__repr__())

    elif int(sig, 16) == 4:
        opcode = gdb.execute("p/x $rax", to_string=True).split("=")[1].strip()
        gdb.execute("c")
        new_op = Opcode(opcode)

        if new_op.const == 1:
            f.write(str_ops[1] % (i, ops[new_op.val1], new_op.src, new_op.final))      
        else:
            f.write(str_ops[0] % (i, ops[new_op.val1], new_op.src, new_op.dest))      

        if new_op.const == 1:
            regs.operation(new_op.src, op_sym[new_op.val1], new_op.final)
        else:
            regs.operation_reg(new_op.src, op_sym[new_op.val1], new_op.dest)
        
        #f.write(new_op.__repr__())

    elif int(sig, 16) == 8: 
        if op.src == 1:
            f.write("%d: cmp r%d 0x%x\n" % (i, op.dest, op.final2))
        else:
            f.write("%d: cmp r%d r%d\n" % (i, op.dest, op.final2 & 0xff))

        if op.src == 1:
            regs.update_eflag(op.dest, op.final2)
        else:
            regs.update_eflag_reg(op.dest, op.final2 & 0xff)
        
        #f.write(op.__repr__())

    elif int(sig, 16) == 0xb:
        f.write("%d: jmp %s 0x%x\n" % (i, jmp[op.src], op.dest))
        
        #f.write(op.__repr__())

    else:
        print("Error")

    #f.write(regs.__repr__())

Reversing the VM instructions

This was probably the most complicated VM algorithm I have seen in CTFs. I have written the python version of the code below - you can take a look at it.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

bit_string = [48] * 100
random_array = [..] # Huge array in the memory
flag = [0] * 100
max_sum = 0
while True:
    y = 0
    temp_array = []
    
    # Find the sum of the random array based on the
    # bit string.
    for x in range(len(bit_string)):
        temp_array.append(random_array[y + (x * (x + 1) >> 1)])
        if bit_string[x] == 49:
            y = y + 1

    # If the sum is greater than the max sum then copy
    # it to the flag location. 
    if sum(temp_array) > max_sum:
        max_sum = bit_sum
        for i in range(len(temp_array)):
            flag[i] = temp_array[i]

    ctr = 0
    flag = True

    # Increment the bit string value
    while flag:
        if bit_string[ctr] == 48:
            flag = False
        bit_string[ctr] = bit_string[ctr] ^ 1

Looking a bit deeper into the algorithm we see that it is actually taking the numbers in a very specific order.

x z = ((x * (x + 1)) >> 1) range of y + z
0 0 0
1 1 1..2
2 3 3..5
3 6 6..9
4 10 10..14
… … …
100 5050 5050..5150

From this order we figured out that this was basically dividing the array in form of a triangle and then trying to find the path which has the maximum sum.

Now we know what the VM is trying to do and it is taking a long time since the VM is trying to bruteforce the path. Now all we need to do is to find a more efficient way to solve this.

lazy solve

Since it is copying the path that has the maximum sum. I printed out the entire array in the form of a triangle and then I searched for the flag format manually - that is de1ctf{ and then I followed it until I reached the end.

You can probably trace - ~triangle~is from the above screen shot. That was like a wrapper around the flag.

flag was de1ctf{no~n33d~70-c4lcul473~3v3ry~p47h}

Intended Solution

After talking to the admin at the end of the CTF I learned that this was a DP problem and the solution was pretty simple.

You can take a look at the problem statement and the solution techniques here.

Linux VM Reversing Automation

1 / 2