Reverse Warmup 문제로 나온 문제다.

main 코드를 보면 연산하고 memcmp로 비교한다. 분기들을 다 만족 시켜주면 된다.

if ( a1 == 2 )
  {
    s = a2[1];
    if ( strlen(a2[1]) != 39 )
    {
      puts("incorrect");
      exit(0);
    }
    if ( memcmp(s, "TWCTF{", 6uLL) || s[38] != 125 )
    {
      puts("incorrect");
      exit(0);
    }
  • 우선 argv로 입력받은 값은 39글자인지 비교한다.
  • 입력 받은 값이 TWCTF{ 로 시작하고 뒤에 } 붙여야한다.


		s1 = 0LL;
    v38 = 0LL;
    v39 = 0LL;
    v40 = 0LL;
    v41 = 0LL;
    v42 = 0LL;
    v43 = 0LL;
    v44 = 0LL;
    v46 = 3978425819141910832LL;
    v47 = 7378413942531504440LL;
    for ( i = 0; i <= 15; ++i )
    {
      for ( j = strchr(s, *(&v46 + i)); j; j = strchr(j + 1, *(&v46 + i)) )
        ++*(&s1 + i);
    }
    if ( memcmp(&s1, &unk_400F00, 0x40uLL) )
    {
      puts("incorrect");
      exit(0);
    }
  • { }사이는 “0123456789abcdef” 만 들어간다. 16진수 값만 들어간다고 한다. 각각 개수는 3, 2, 2, 0, 3, 2, 1, 3, 3, 1, 1, 3, 1, 2, 2, 3 를 만족해야한다.


for ( k = 0; k <= 7; ++k )
    {
      v10 = 0;
      v11 = 0;
      for ( l = 0; l <= 3; ++l )
      {
        v5 = s[4 * k + 6 + l];
        v10 += v5;
        v11 ^= v5;
      }
      *(&v21 + k) = v10;
      *(&v25 + k) = v11;
    }

if ( memcmp(&v21, &unk_400F40, 0x20uLL) || memcmp(&v25, &unk_400F60, 0x20uLL) )
    {
      puts("incorrect");
      exit(0);
    }
  • s[4 * k + 6 + l] 값들을 xor 연산과 덧셈연산 한 값들이 테이블 값들이 같도록 해야한다.


for ( m = 0; m <= 7; ++m )
    {
      v14 = 0;
      v15 = 0;
      for ( n = 0; n <= 3; ++n )
      {
        v6 = s[8 * n + 6 + m];
        v14 += v6;
        v15 ^= v6;
      }
      *(&v29 + m) = v14;
      *(&v33 + m) = v15;
    }

if ( memcmp(&v29, &unk_400FA0, 0x20uLL) || memcmp(&v33, &unk_400F80, 0x20uLL) )
    {
      puts("incorrect");
      exit(0);
    }
  • s[8 * n + 6 + m] 값들을 xor 연산과 덧셈연산 한 값들이 테이블 값들이 같도록 해야한다.


for ( ii = 0; ii <= 31; ++ii )
    {
      v7 = s[ii + 6];
      if ( v7 <= 47 || v7 > 57 )
      {
        if ( v7 <= 96 || v7 > 102 )
          v45[ii] = 0;
        else
          v45[ii] = 128;
      }
      else
      {
        v45[ii] = 255;
      }
    }
    if ( memcmp(v45, &unk_400FC0, 0x80uLL) )
    {
      puts("incorrect");
      exit(0);
    }
  • 이곳은 s의 문자열 범위 지정해준다.


v18 = 0;
    for ( jj = 0; jj <= 15; ++jj )
      v18 += s[2 * (jj + 3)];
    if ( v18 != 1160 )
    {
      puts("incorrect");
      exit(0);
    }
  • s[2 * (jj + 3)]의 값들의 합이 1160이면 된다.


if ( s[37] != 53 || s[7] != 102 || s[11] != 56 || s[12] != 55 || s[23] != 50 || s[31] != 52 )
    {
      puts("incorrect");
      exit(0);
    }
  • 각각 인덱스의 값을 만족시키면 된다.


from z3 import * 

s = Solver()

a1 = [BitVec('a%i'%i,8) for i in range(39)]

s.add(a1[0] == ord('T'))
s.add(a1[1] == ord('W'))
s.add(a1[2] == ord('C'))
s.add(a1[3] == ord('T'))
s.add(a1[4] == ord('F'))
s.add(a1[5] == ord('{'))
s.add(a1[38] == ord('}'))
s.add(a1[37] == 53 , a1[7] == 102 , a1[11] == 56 , a1[12] == 55 , a1[23] == 50 , a1[31] == 52)

v45 = [0x30,0x31,0x32,0x33,0x34,0x35,0x36,0x37,0x38,0x39,0x61,0x62,0x63,0x64,0x65,0x66]
# 0 1 2 3 4 5 6 7 8 9 a b c d e f 
tb1 = [3, 2, 2, 0, 3, 2, 1, 3, 3, 1, 1, 3, 1, 2, 2, 3]
tb2 = [0x015E, 0x00DA, 0x012F, 0x0131, 0x0100, 0x0131, 0x00FB, 0x0102]
tb3 = [82, 12, 1, 15, 92, 5, 83, 88]
tb4 = [1, 87, 7, 13, 13, 83, 81, 81]
tb5 = [0x0129, 0x0103, 0x012B, 0x0131, 0x0135, 0x010B, 0x00FF, 0x00FF]
tb6 = [128, 128, 255, 128, 255, 255, 255, 255, 128, 255, 255, 128, 128, 255, 255, 128, 255, 255, 128, 255, 128, 128, 255, 255, 255, 255, 128, 255, 255, 255, 128, 255]

for k in range(8):
	v10 = 0
	v11 = 0
	for l in range(4):
		v5 = a1[4 * k + 6 + l]
		v10 += v5
		v11 ^= v5
	s.add(tb2[k] == v10)
	s.add(tb3[k] == v11)

for m in range(8):
	v14 = 0
	v15 = 0
	for n in range(4):
		v6 = a1[8 * n + 6 + m]
		v14 += v6
		v15 ^= v6
	s.add(tb5[m] == v14)
	s.add(tb4[m] == v15)


v18 = 0
for jj in range(16):
	v18 += a1[2 * (jj + 3)]
s.add(v18 == 1160)

for i in range(32):
    if(tb6[i]==128):
        s.add(a1[i+6]>=97)
        s.add(a1[i+6]<=102)
    else:
        s.add(a1[i+6]>=48)
        s.add(a1[i+6]<=57)


for i,ch in enumerate("0123456789abcdef"):
	cnt = 0
	for x in a1:
		cnt += If(x == ord(ch),1,0)
	s.add(cnt == tb1[i])
if s.check() == sat:
	m = s.model()
	print ''.join(chr(int(str(m.evaluate(a1[i]))))for i in range(39))

FLAG : TWCTF{df2b4877e71bd91c02f8ef6004b584a5}

+ Recent posts