Rev Darthvader


Why Z3 when you can have to just bruteforce ~256 possiblities

Challenge files

Problem Statement

Simple input checker binary, but there’s suspicious logic in main. Breakpoints placed inside main are not hit, suggesting that some other code is running before main.

This leads to constructor array, especially the function _INIT_1. It contains the main logic for the challenge.

A stack array is constructed with specific values.

C
 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
  local_128[0] = 0x343b;
  local_128[1] = 0xa726;
  local_128[2] = 0x640e;
  local_128[3] = 0x2806;
  local_128[4] = 0x5003;
  local_128[5] = 0xa007;
  local_128[6] = 0x10d9b;
  local_128[7] = 0x4000;
  local_128[8] = 0x8000;
  local_128[9] = 0x10000;
  local_f8[0] = 0x12d;
  local_f8[1] = 200;
  local_f8[2] = 0x2c;
  local_f8[3] = 0x1ec;
  local_f8[4] = 0x17b;
  local_f8[5] = 0x1ea;
  local_f8[6] = 0xd4;
  local_f8[7] = 0x1bd;
  local_f8[8] = 0x66;
  local_f8[9] = 0x126;
  local_f8[10] = 0x27;
  local_f8[0xb] = 0x106;
  local_f8[0xc] = 0x125;
  local_f8[0xd] = 0x66;
  local_f8[0xe] = 0x194;
  local_f8[0xf] = 0x56;
  local_f8[0x10] = 0x172;
  local_f8[0x11] = 0x7e;
  local_f8[0x12] = 0x8a;
  local_f8[0x13] = 0x98;
  local_f8[0x14] = 0xc0;
  local_f8[0x15] = 0xd1;
  local_f8[0x16] = 0xd2;
  local_f8[0x17] = 399;
  local_f8[0x18] = 0x75;
  local_f8[0x19] = 0x1ee;
  local_f8[0x1a] = 0x134;
  local_f8[0x1b] = 0x124;
  local_f8[0x1c] = 0x143;
  local_f8[0x1d] = 0x1c6;
  local_f8[0x1e] = 0x16c;

Userinput is processed in a predicate pipeline that conditionaly increments a variable, and the variable must have final value 0x1e.

C
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
  while( true ) {
    if (0x1e < i) {
      puts("Correct flag!");
                    /* WARNING: Subroutine does not return */
      exit(0);
    }
    DAT_0040406c = i + local_128[i % 10];
    a = get_confusing_0040163d();
    b = get_confusing_0040163d();
    c = get_confusing_0040163d();
    if ((b + ((int)inp[i] ^ a) ^ c) != local_f8[i]) break;
    i = i + 1;
  }

i is incremented when (b + (inp[i] ^ a) ^ c) is equal to corresponding stack value. So we have to solve for inp[i]. This looks like it can be easily solved with a smt solver like z3, but It seems to not find the solution (for some reason I don’t understand)

So instead I write a bruteforce script in C, since inp[i] can have only 0xff values afterall, and value at each index is independent.

Sovle script

C
 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
#include <stdint.h>
#include <stdio.h>


uint32_t globall = -1;
uint32_t dwords[0x27] = {0};
uint32_t flg[0x40] = {0};

uint32_t roller(void)
{
  globall = globall * 0x41c64e6d + 0x3039;
  return globall >> 0x10 & 0xff;
}


int doo(i)
{
	globall = i + dwords[i % 10];
	uint32_t a = roller();
	uint32_t b = roller();
	uint32_t c = roller();

	if ((b + ((int)flg[i] ^ a) ^ c) != dwords[(long)i + 0xc])
		return 0;
    return 1;
}

int main(void)
{
  dwords[0] = 0x343b;
  dwords[1] = 0xa726;
  dwords[2] = 0x640e;
  dwords[3] = 0x2806;
  dwords[4] = 0x5003;
  dwords[5] = 0xa007;
  dwords[6] = 0x10d9b;
  dwords[7] = 0x4000;
  dwords[8] = 0x8000;
  dwords[9] = 0x10000;
  dwords[0xc] = 0x12d;
  dwords[0xd] = 200;
  dwords[0xe] = 0x2c;
  dwords[0xf] = 0x1ec;
  dwords[0x10] = 0x17b;
  dwords[0x11] = 0x1ea;
  dwords[0x12] = 0xd4;
  dwords[0x13] = 0x1bd;
  dwords[0x14] = 0x66;
  dwords[0x15] = 0x126;
  dwords[0x16] = 0x27;
  dwords[0x17] = 0x106;
  dwords[0x18] = 0x125;
  dwords[0x19] = 0x66;
  dwords[0x1a] = 0x194;
  dwords[0x1b] = 0x56;
  dwords[0x1c] = 0x172;
  dwords[0x1d] = 0x7e;
  dwords[0x1e] = 0x8a;
  dwords[0x1f] = 0x98;
  dwords[0x20] = 0xc0;
  dwords[0x21] = 0xd1;
  dwords[0x22] = 0xd2;
  dwords[0x23] = 399;
  dwords[0x24] = 0x75;
  dwords[0x25] = 0x1ee;
  dwords[0x26] = 0x134;

  for (int i = 0; i < 0x1f; i++) {
	  for (int j = 0 ; j < 256; j++) {
		  flg[i] = j;
		  if (doo(i) == 1) {
			  printf("%c", j);
		  }
	  }
  }
  puts("");


}

It outputs a partial flag, and we guess the rest of the flag charecters.

I could’ve automated it but I broke free of my OCD and decided to just guess it with the rest of my team :))

TEXT
outer-heaven :: inctf/foobar/arthvader ‹master*› » ./rev
inctf{w3lcom3_t0_the_d4rk_s�
outer-heaven :: inctf/foobar/arthvader ‹master*› » ./rev | xxd
00000000: 696e 6374 667b 7733 6c63 6f6d 335f 7430  inctf{w3lcom3_t0
00000010: 5f74 6865 5f64 3472 6b5f 73e0 f00a       _the_d4rk_s...
outer-heaven :: inctf/foobar/arthvader ‹master*› »