[리버싱] VM Problem:prob-begin, prob-1

Layer7 과제/리버싱

[리버싱] VM Problem:prob-begin, prob-1

kms0204 2022. 8. 24. 01:35

prob-begin:

문제파일을 디컴파일하면 아래와 같다.

사용자로부터 최대 길이 16만큼의 문자열을 입력받아 v5에 저장한다.

initcpu(v4, v5)는 아래와 같다.

즉, 사용자의 입력을(v5에 있는 값) v4에 복사한다.

runcpu(v4)의 내용은 아래와 같다.

a1은 v4, 즉 사용자의 입력을 뜻하는 매개변수이고, stub의 값에 따라서 switch-case 문으로 4가지 경우로 분류된다.

4가지 경우는 각각 mov, add, sub, xor을 담당한다.

배열 stub를 확인해보면,

Export data의 Preview에 출력되는 값들을 원소로 갖는 배열이라는 것을 알 수 있다.

main 함수로 돌아와서, 맨 아래 부분을 확인해보면 아래와 같다.

이 내용을 이해하기 전에, 앞에 나왔던 내용을 살펴보자.

앞서 runcpu 함수에서 stub의 값에 따라서 switch-case문으로 4가지의 상황을 분류하고, 각 상황에서 사용자의 입력과 stub 원소를 이용해서 특정한 연산을 했다.

이를 파이썬으로 해석하면,

data = [
  0x46, 0x04, 0xCD, 0x04, 0xD4, 0x0A, 0x45, 0x00, 0x04, 0x46, 
  0x04, 0xAB, 0xBF, 0xD1, 0x30, 0x5A, 0x00, 0x04, 0x46, 0x04, 
  0xB2, 0x83, 0x9E, 0x51, 0x5A, 0x00, 0x04, 0x46, 0x05, 0xBB, 
  0x80, 0x7C, 0x4F, 0x5A, 0x01, 0x05, 0x46, 0x05, 0x63, 0x1C, 
  0x0D, 0x76, 0x55, 0x01, 0x05, 0x46, 0x05, 0x93, 0xC3, 0x31, 
  0x94, 0x5A, 0x01, 0x05, 0x46, 0x06, 0xFB, 0xB2, 0xB9, 0xE8, 
  0x55, 0x02, 0x06, 0x46, 0x06, 0x29, 0xD7, 0x71, 0x9A, 0x45, 
  0x02, 0x06, 0x46, 0x06, 0x75, 0x6D, 0x06, 0x00, 0x5A, 0x02, 
  0x06, 0x46, 0x07, 0x72, 0xA2, 0x6E, 0x3E, 0x5A, 0x03, 0x07, 
  0x46, 0x07, 0x74, 0xAC, 0x11, 0xD4, 0x5A, 0x03, 0x07, 0x46, 
  0x07, 0x43, 0x5C, 0x5E, 0x97, 0x5A, 0x03, 0x07, 0x5A, 0x07, 
  0x07, 0x50, 0x07, 0x00, 0x50, 0x07, 0x01, 0x50, 0x07, 0x02, 
  0x50, 0x07, 0x03, 0xCC, 0xDB, 0x26, 0x5A, 0x02, 0xDD, 0x8F, 
  0x4F, 0x10, 0xD9 
]
cur = 0

while True:
    s = data[cur]
    if s == 0x46: 
        print('REG[%d] = 0x%08X' % (data[cur+1], int.from_bytes(data[cur+2:cur+6], 'little')))
        print('REG[%d] &= 0xffffffff' % (data[cur+1]))
        cur += 5
    elif s == 0x45: 
        print('REG[%d] += REG[%d]' % (data[cur+1], data[cur+2]))
        print('REG[%d] &= 0xffffffff' % (data[cur+1]))
        cur += 2
    elif s == 0x55: 
        print('REG[%d] -= REG[%d]' % (data[cur+1],data[cur+2]))
        print('REG[%d] &= 0xffffffff' %(data[cur+1]))
        cur += 2
    elif s == 0x5A: 
        print('REG[%d] ^= REG[%d]' % (data[cur+1], data[cur+2]))
        print('REG[%d] &= 0xffffffff' % (data[cur+1]))
        cur += 2
    elif s == 0x50: 
        print('REG[%d] |= REG[%d]' % (data[cur+1], data[cur+2]))
        print('REG[%d] &= 0xffffffff' % (data[cur+1]))
        cur += 2
    elif s == 0xCC:
        break
    cur += 1

위와 같다. 실행결과는 아래와 같다.

<실행결과>

REG[4] = 0x0AD404CD
REG[4] &= 0xffffffff
REG[0] += REG[4]
REG[0] &= 0xffffffff
REG[4] = 0x30D1BFAB
REG[4] &= 0xffffffff
REG[0] ^= REG[4]
REG[0] &= 0xffffffff
REG[4] = 0x519E83B2
REG[4] &= 0xffffffff
REG[0] ^= REG[4]
REG[0] &= 0xffffffff
REG[5] = 0x4F7C80BB
REG[5] &= 0xffffffff
REG[1] ^= REG[5]
REG[1] &= 0xffffffff
REG[5] = 0x760D1C63
REG[5] &= 0xffffffff
REG[1] -= REG[5]
REG[1] &= 0xffffffff
REG[5] = 0x9431C393
REG[5] &= 0xffffffff
REG[1] ^= REG[5]
REG[1] &= 0xffffffff
REG[6] = 0xE8B9B2FB
REG[6] &= 0xffffffff
REG[2] -= REG[6]
REG[2] &= 0xffffffff
REG[6] = 0x9A71D729
REG[6] &= 0xffffffff
REG[2] += REG[6]
REG[2] &= 0xffffffff
REG[6] = 0x00066D75
REG[6] &= 0xffffffff
REG[2] ^= REG[6]
REG[2] &= 0xffffffff
REG[7] = 0x3E6EA272
REG[7] &= 0xffffffff
REG[3] ^= REG[7]
REG[3] &= 0xffffffff
REG[7] = 0xD411AC74
REG[7] &= 0xffffffff
REG[3] ^= REG[7]
REG[3] &= 0xffffffff
REG[7] = 0x975E5C43
REG[7] &= 0xffffffff
REG[3] ^= REG[7]
REG[3] &= 0xffffffff
REG[7] ^= REG[7]
REG[7] &= 0xffffffff
REG[7] |= REG[0]
REG[7] &= 0xffffffff
REG[7] |= REG[1]
REG[7] &= 0xffffffff
REG[7] |= REG[2]
REG[7] &= 0xffffffff
REG[7] |= REG[3]
REG[7] &= 0xffffffff

즉, 특정한 연산이 수행된 후, v4[7]의 값이 0이 아닌 수라면 if문이 참이 되므로 Wrong...이 출력되고 0이라면 Correct!가 출력한다는 뜻이다.

따라서 우리가 구해야할 flag는 if문이 거짓이 되는 값, 즉 특정한 연산을 수행한 후에 v4[7]의 값이 0이 되는 입력이다.

즉, z3 모듈을 사용해야 한다는 것을 짐작할 수 있다.

파이썬에서 z3 모듈을 사용해서 v4[7]가 0이 되는 값을 구하는 코드를 짜면 아래와 같다.

from z3 import *
FLAG = [BitVec("FLAG_%d" %x, 32) for x in range(4)]
REG = [x for x in FLAG] + [0] * 4

REG[4] = 0x0AD404CD
REG[4] &= 0xFFFFFFFF
REG[0] += REG[4]
REG[0] &= 0xFFFFFFFF
REG[4] = 0x30D1BFAB
REG[4] &= 0xFFFFFFFF
REG[0] ^= REG[4]
REG[0] &= 0xFFFFFFFF
REG[4] = 0x519E83B2
REG[4] &= 0xFFFFFFFF
REG[0] ^= REG[4]
REG[0] &= 0xFFFFFFFF
REG[5] = 0x4F7C80BB
REG[5] &= 0xFFFFFFFF
REG[1] ^= REG[5]
REG[1] &= 0xFFFFFFFF
REG[5] = 0x760D1C63
REG[5] &= 0xFFFFFFFF
REG[1] -= REG[5]
REG[1] &= 0xFFFFFFFF
REG[5] = 0x9431C393
REG[5] &= 0xFFFFFFFF
REG[1] ^= REG[5]
REG[1] &= 0xFFFFFFFF
REG[6] = 0xE8B9B2FB
REG[6] &= 0xFFFFFFFF
REG[2] -= REG[6]
REG[2] &= 0xFFFFFFFF
REG[6] = 0x9A71D729
REG[6] &= 0xFFFFFFFF
REG[2] += REG[6]
REG[2] &= 0xFFFFFFFF
REG[6] = 0x00066D75
REG[6] &= 0xFFFFFFFF
REG[2] ^= REG[6]
REG[2] &= 0xFFFFFFFF
REG[7] = 0x3E6EA272
REG[7] &= 0xFFFFFFFF
REG[3] ^= REG[7]
REG[3] &= 0xFFFFFFFF
REG[7] = 0xD411AC74
REG[7] &= 0xFFFFFFFF
REG[3] ^= REG[7]
REG[3] &= 0xFFFFFFFF
REG[7] = 0x975E5C43
REG[7] &= 0xFFFFFFFF
REG[3] ^= REG[7]
REG[3] &= 0xFFFFFFFF
REG[7] ^= REG[7]
REG[7] &= 0xFFFFFFFF
REG[7] |= REG[0]
REG[7] &= 0xFFFFFFFF
REG[7] |= REG[1]
REG[7] &= 0xFFFFFFFF
REG[7] |= REG[2]
REG[7] &= 0xFFFFFFFF
REG[7] |= REG[3]
REG[7] &= 0xFFFFFFFF
solver = Solver()
solver.add(REG[7] == 0)

print(solver.check())
m = solver.model()
#print(m)


if solver.check() == CheckSatResult(True):
  for i in FLAG: 
    print(m[i].as_long().to_bytes(4, "little").decode(), end="")
else:
  print("unsat")

L7{VM_BEGINNER!}

prob-1: (prob-begine과 같은 유형의 문제이므로, prob-begin을 참고하면 도움이 된다)

prob-1을 디컴파일하면 다음과 같다.

사용자로부터 최대 길이 48만큼의 문자열을 입력받고, 입력값을 v5에 나눠서 넣어주고 있다. (run_cpu 함수 전까지 내용)

마지막 if문을 보면 v5[15]가 0이 되느냐, 0이 아닌 숫자가 되느냐에 따라서 flag인지 아닌지가 결정된다.

우린 if문이 거짓이 될 때의 입력값, 즉 v5[15]가 0이 되는 입력값을(flag) 구해야 한다.

이 문제도 flag를 구하려면 run_cpu의 결과가 필요하므로, 가장 중요한 부분이 되는 run_cpu 함수를 분석해보자.

(매개변수는 사용자의 입력값이다)

run_cpu의 내용은 다음과 같다.

__int64 __fastcall run_cpu(__int64 a1)
{
  int v1; // eax
  __int64 result; // rax
  int v3; // eax
  int v4; // eax
  int v5; // eax
  int v6; // eax
  int v7; // eax
  int v8; // eax
  int v9; // [rsp+14h] [rbp-4h]
  int v10; // [rsp+14h] [rbp-4h]
  int v11; // [rsp+14h] [rbp-4h]
  int v12; // [rsp+14h] [rbp-4h]
  int v13; // [rsp+14h] [rbp-4h]
  int v14; // [rsp+14h] [rbp-4h]
  int v15; // [rsp+14h] [rbp-4h]
  int v16; // [rsp+14h] [rbp-4h]

  v9 = 0;
  while ( 1 )
  {
    v1 = v9;
    v10 = v9 + 1;
    result = stub[v1];
    if ( (_BYTE)result == 0xCC )
      break;
    switch ( (_BYTE)result )
    {
      case 0xBA:
        v3 = v10;
        v11 = v10 + 1;
        result = stub[v3];
        if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v11]) = *(unsigned int *)&stub[v11 + 1];
            v9 = v11 + 5;
          }
          else
          {
            if ( (_BYTE)result != 2 )
              return result;
            *(_QWORD *)(a1 + 8LL * stub[v11]) = *(_QWORD *)&stub[v11 + 1];
            v9 = v11 + 9;
          }
        }
        else
        {
          *(_QWORD *)(a1 + 8LL * stub[v11]) = *(_QWORD *)(a1 + 8LL * stub[v11 + 1]);
          v9 = v11 + 2;
        }
        break;
      case 0x76:
        v4 = v10;
        v12 = v10 + 1;
        result = stub[v4];
        if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v12]) += *(unsigned int *)&stub[v12 + 1];
            v9 = v12 + 5;
          }
          else
          {
            if ( (_BYTE)result != 2 )
              return result;
            *(_QWORD *)(a1 + 8LL * stub[v12]) += *(_QWORD *)&stub[v12 + 1];
            v9 = v12 + 9;
          }
        }
        else
        {
          *(_QWORD *)(a1 + 8LL * stub[v12]) += *(_QWORD *)(a1 + 8LL * stub[v12 + 1]);
          v9 = v12 + 2;
        }
        break;
      case 0x90:
        v5 = v10;
        v13 = v10 + 1;
        result = stub[v5];
        if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v13]) -= *(unsigned int *)&stub[v13 + 1];
            v9 = v13 + 5;
          }
          else
          {
            if ( (_BYTE)result != 2 )
              return result;
            *(_QWORD *)(a1 + 8LL * stub[v13]) -= *(_QWORD *)&stub[v13 + 1];
            v9 = v13 + 9;
          }
        }
        else
        {
          *(_QWORD *)(a1 + 8LL * stub[v13]) -= *(_QWORD *)(a1 + 8LL * stub[v13 + 1]);
          v9 = v13 + 2;
        }
        break;
      case 0x83:
        v6 = v10;
        v14 = v10 + 1;
        result = stub[v6];
        if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v14]) &= *(unsigned int *)&stub[v14 + 1];
            v9 = v14 + 5;
          }
          else
          {
            if ( (_BYTE)result != 2 )
              return result;
            *(_QWORD *)(a1 + 8LL * stub[v14]) &= *(_QWORD *)&stub[v14 + 1];
            v9 = v14 + 9;
          }
        }
        else
        {
          *(_QWORD *)(a1 + 8LL * stub[v14]) &= *(_QWORD *)(a1 + 8LL * stub[v14 + 1]);
          v9 = v14 + 2;
        }
        break;
      case 0x91:
        v7 = v10;
        v15 = v10 + 1;
        result = stub[v7];
        if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v15]) |= *(unsigned int *)&stub[v15 + 1];
            v9 = v15 + 5;
          }
          else
          {
            if ( (_BYTE)result != 2 )
              return result;
            *(_QWORD *)(a1 + 8LL * stub[v15]) |= *(_QWORD *)&stub[v15 + 1];
            v9 = v15 + 9;
          }
        }
        else
        {
          *(_QWORD *)(a1 + 8LL * stub[v15]) |= *(_QWORD *)(a1 + 8LL * stub[v15 + 1]);
          v9 = v15 + 2;
        }
        break;
      case 0xEF:
        *(_QWORD *)(a1 + 8LL * stub[v10]) = ~*(_QWORD *)(a1 + 8LL * stub[v10]);
        v9 = v10 + 1;
        break;
      case 0x2E:
        v8 = v10;
        v16 = v10 + 1;
        result = stub[v8];
        if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v16]) ^= *(unsigned int *)&stub[v16 + 1];
            v9 = v16 + 5;
          }
          else
          {
            if ( (_BYTE)result != 2 )
              return result;
            *(_QWORD *)(a1 + 8LL * stub[v16]) ^= *(_QWORD *)&stub[v16 + 1];
            v9 = v16 + 9;
          }
        }
        else
        {
          *(_QWORD *)(a1 + 8LL * stub[v16]) ^= *(_QWORD *)(a1 + 8LL * stub[v16 + 1]);
          v9 = v16 + 2;
        }
        break;
      default:
        return result;
    }
  }
  return result;
}

prob-begin과 마찬가지로 stub라는 배열에 따라서 switch-case문으로 경우를 나누고 각각 처리한다.

prob-begin과 같은 맥락으로, 이것도 파이썬으로 구현해야 한다.

디컴파일한 코드를 보면 변수를 여러개 선언해서 값을 계속 바꾸기 때문에 헷갈려 보이지만,

변수를 줄이고 수식이나 코드로 표현된 것 중에서 연산할 수 있는 것들을 계산해서 다시 쓰면 코드가 간결해진다.

첫 번째 case의 if문을 보면 v1, v3, v9, v10, v11을 보면, 결국 v11이 인덱스를 의미하는 변수이고 나머지 변수들의 사용은

그저 그 과정이다. 뿐만 아니라 밑에 나오는 v14, v16 등도 코드를 확인해보면 다른 부분도 같은 맥락이라는 것을

알 수 있다.

그러므로 이를 파이썬으로 옮길 때, 간결화시키기 위해 인덱스를 의미하는 변수를 하나로 통일하고(변수 cur),

vNUM 변수들이 연산을 보면, 각 case의 if문의 마지막에서 변수의 값을 증가시키는 부분이 2 + 숫자를 의마한다는 것을

이용해서 그냥 그 결과값을 더해주도록 만들었다.

예를 들어서,

if ( (_BYTE)result )
        {
          if ( (_BYTE)result == 1 )
          {
            *(_QWORD *)(a1 + 8LL * stub[v16]) ^= *(unsigned int *)&stub[v16 + 1];
            v9 = v16 + 5;
          }

위 코드의 마지막인 v9 = v16 + 5가 사실은 v9 = 2 + 5와 같은 의미이므로 v9 = 7로 계산하겠다는 의미이다.

하지만, 인덱스를 의미하는 변수를 cur로 통일했으므로 파이썬으로 고치면 cur += 7 이 되겠다.

run_cpu의 결과를 구하기 위해, 디컴파일 한 코드를 파이썬으로 구현하면 아래와 같은데, 추가적으로 덧붙일 내용이 있다.

IDA로 디컴파일하면서 Shift + E 단축키를 이용해서 stub의 원소들을 복사해서 data에 저장했다.

단, 원소들이 unsigned char 형태이기 때문에 1바이트들이다.

하지만 문제에서는 stub의 원소들을 DWORD와 QWORD 만큼 참조했기 때문에, DWORD는 4바이트, QWORD는 8바이트이라는 것과 리틀 엔디안이라는 것과 16진수 데이터라는 것을 고려해서, 제일 뒤에 있는 값의 가중치가 16^(2*데이터 개수 - 2)로 가장 크고 앞에 있는 값으로 갈수록 가중치가 16 ^ (2 * 데이터의 개수 - 2 * n)으로 작아지다가, 제일 앞에 있는 값의 가중치가 16 ^ 0으로 가장 작도록 계산하여 그 값들을 모두 더했다.

그리고 DWORD와 QWORD에 따라서 데이터가 4개 필요할지 8개 필요할지가 달라지므로 DWORD는 fourbits라는 함수를 정의해서 사용했고, QWORD는 eightbits라는 함수를 정의해서 사용했다.

그리고 DA에서 C언어를 기준으로 디컴파일했기 때문에 파이썬 문법에 맞게 고쳐주었다. (예를 들어서, 파이썬에는 switch case문이 없으므로 if문으로 대체했고, 또 괄호를 사용하지 않으므로 들여쓰기로 대체했다)

data =[
  0x2E, 0x02, 0x00, 0x5E, 0xCC, 0xEA, 0x30, 0x26, 0x1B, 0xA0, 
  0x89, 0x76, 0x02, 0x00, 0x44, 0xDC, 0xF6, 0x05, 0x40, 0xA2, 
  0x41, 0xF2, 0x2E, 0x02, 0x00, 0xE9, 0xA5, 0x55, 0x6C, 0x5D, 
  0x94, 0x54, 0xE7, 0xEF, 0x00, 0x2E, 0x02, 0x00, 0xB1, 0xA5, 
  0xEE, 0x14, 0xE4, 0x5A, 0x46, 0xBB, 0x76, 0x02, 0x00, 0x11, 
  0xD4, 0xE9, 0x0D, 0xAD, 0x51, 0xC5, 0x93, 0xEF, 0x00, 0x90, 
  0x02, 0x00, 0xFD, 0x02, 0x4A, 0xF4, 0x62, 0xD6, 0x5E, 0x01, 
  0x2E, 0x02, 0x01, 0x84, 0x6F, 0x8C, 0xF9, 0x0E, 0xC4, 0x4A, 
  0xCF, 0x76, 0x02, 0x01, 0x9B, 0xB5, 0xE5, 0x8C, 0xAA, 0xD9, 
  0x4A, 0x58, 0x2E, 0x02, 0x01, 0x0A, 0x9D, 0xF0, 0x60, 0x76, 
  0x00, 0x73, 0x23, 0xEF, 0x01, 0x2E, 0x02, 0x01, 0x75, 0x27, 
  0xEC, 0x1B, 0x4E, 0x9D, 0x07, 0x97, 0x76, 0x02, 0x01, 0xF4, 
  0xE0, 0xA2, 0x83, 0xD6, 0xBF, 0x63, 0xD2, 0xEF, 0x01, 0x90, 
  0x02, 0x01, 0x24, 0x7D, 0x00, 0xAF, 0xED, 0x38, 0xCB, 0x88, 
  0x2E, 0x02, 0x02, 0x6B, 0xB6, 0x75, 0xCE, 0x4B, 0xCE, 0xEA, 
  0xD4, 0x76, 0x02, 0x02, 0x54, 0xE8, 0x89, 0xAF, 0xEE, 0x61, 
  0x99, 0xD4, 0x2E, 0x02, 0x02, 0xA8, 0x85, 0x51, 0x18, 0x3D, 
  0x9F, 0x88, 0xC8, 0xEF, 0x02, 0x2E, 0x02, 0x02, 0xAB, 0x96, 
  0x1D, 0x6C, 0x9C, 0x46, 0xB7, 0xBC, 0x76, 0x02, 0x02, 0xB1, 
  0x8F, 0x1A, 0x1F, 0xB8, 0x50, 0xCA, 0x71, 0xEF, 0x02, 0x90, 
  0x02, 0x02, 0xDD, 0x3C, 0xE0, 0x19, 0xEA, 0xE2, 0x36, 0xBD, 
  0x2E, 0x02, 0x03, 0xD4, 0xE8, 0xD8, 0x1F, 0xBA, 0x3F, 0x4C, 
  0x5B, 0x76, 0x02, 0x03, 0xA6, 0x6A, 0xA3, 0xD6, 0xE8, 0x3E, 
  0xCF, 0xEB, 0x2E, 0x02, 0x03, 0x4F, 0x0D, 0x75, 0xCE, 0xBD, 
  0x9F, 0x75, 0x03, 0xEF, 0x03, 0x2E, 0x02, 0x03, 0x3B, 0xF0, 
  0x03, 0x72, 0x37, 0xF9, 0xF1, 0x60, 0x76, 0x02, 0x03, 0xA2, 
  0x7C, 0xC1, 0x60, 0xAB, 0xE7, 0x63, 0x16, 0xEF, 0x03, 0x90, 
  0x02, 0x03, 0xA3, 0x57, 0x82, 0x37, 0xB2, 0xE7, 0xF4, 0x4A, 
  0x2E, 0x02, 0x04, 0x8F, 0xE5, 0x0F, 0xF2, 0x7E, 0x5E, 0xD3, 
  0x23, 0x76, 0x02, 0x04, 0x77, 0xA5, 0x07, 0x6F, 0xA4, 0x7E, 
  0x6C, 0xD6, 0x2E, 0x02, 0x04, 0xB0, 0xED, 0x3E, 0x38, 0xC3, 
  0x6A, 0x69, 0x8D, 0xEF, 0x04, 0x2E, 0x02, 0x04, 0x5B, 0x9E, 
  0x4A, 0xCB, 0x1D, 0xDE, 0xA9, 0xAD, 0x76, 0x02, 0x04, 0x77, 
  0xC4, 0xD0, 0x41, 0xB0, 0x03, 0x34, 0xED, 0xEF, 0x04, 0x90, 
  0x02, 0x04, 0x35, 0x79, 0x51, 0x91, 0x55, 0x1D, 0x95, 0x30, 
  0x2E, 0x02, 0x05, 0xD4, 0xB8, 0x1D, 0x54, 0x3E, 0x40, 0x71, 
  0x55, 0x76, 0x02, 0x05, 0x22, 0x2F, 0x06, 0x80, 0xBA, 0xD3, 
  0x1D, 0xAF, 0x2E, 0x02, 0x05, 0x17, 0xF0, 0x22, 0xD9, 0x74, 
  0x4B, 0x19, 0x55, 0xEF, 0x05, 0x2E, 0x02, 0x05, 0x07, 0x84, 
  0x1D, 0xB1, 0xBB, 0x1F, 0xF0, 0x92, 0x76, 0x02, 0x05, 0x4A, 
  0x0B, 0x34, 0xE7, 0x25, 0x30, 0x36, 0xDB, 0xEF, 0x05, 0x90, 
  0x02, 0x05, 0xD3, 0x75, 0xE8, 0xD4, 0x11, 0x17, 0x30, 0xE8, 
  0x91, 0x00, 0x0F, 0x00, 0x91, 0x00, 0x0F, 0x01, 0x91, 0x00, 
  0x0F, 0x02, 0x91, 0x00, 0x0F, 0x03, 0x91, 0x00, 0x0F, 0x04, 
  0x91, 0x00, 0x0F, 0x05, 0xCC
]


def fourbits(num1, num2,num3,num4):
    return (num4) * 16 ** 6 + (num3) * 16 ** 4 + (num2) * 16 ** 2 + (num1) 

def eightbits(num1, num2,num3,num4, num5,num6,num7, num8):
    return (num8) * 16 ** 14 + (num7) * 16 ** 12 + (num6) * 16 ** 10 + (num5) * 16 ** 8 + (num4) * 16 ** 6 + (num3) * 16 ** 4 + (num2) * 16 ** 2 + (num1) 


result = 0
cur = 0
while True:
    result = data[cur]
    if result == 0xcc:
        break
    if result == 0xba:
        result = data[cur+1]
        if result: 
            if result == 1:
                print("REG[%d] = %d" % (data[cur+2], fourbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 7
            else: 
                print("REG[%d] = %d" % (data[cur+2], eightbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6], data[cur+7], data[cur+8], data[cur+9], data[cur+10])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 11
        else:
            print("REG[%d] = REG[%d]" % (data[cur+2], data[cur+3]))  
            print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
            cur += 4
    elif result == 0x76:
        result = data[cur+1]
        result = data[cur+1]
        if result: 
            if result == 1:
                print("REG[%d] += %d" % (data[cur+2], fourbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 7
            else:
                print("REG[%d] += %d" % (data[cur+2], eightbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6], data[cur+7], data[cur+8], data[cur+9], data[cur+10])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 11
        else:
            print("REG[%d] += REG[%d]" % (data[cur+2], data[cur+3]))
            print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
            cur += 4
    elif result == 0x90:
        result = data[cur+1]
        if result: 
            if result == 1:
                print("REG[%d] -= %d" % (data[cur+2], fourbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 7
            else: 
                print("REG[%d] -= %d" % (data[cur+2], eightbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6], data[cur+7], data[cur+8], data[cur+9], data[cur+10])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 11
        else:
            print("REG[%d] -= REG[%d]" % (data[cur+2], data[cur+3]))
            print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
            cur += 4
    elif result == 0x83:
        result = data[cur+1]
        if result: 
            if result == 1:
                print("REG[%d] &= %d" % (data[cur+2], fourbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 7
            else:
                print("REG[%d] &= %d" % (data[cur+2], eightbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6], data[cur+7], data[cur+8], data[cur+9], data[cur+10])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 11
        else:
            print("REG[%d] &= REG[%d]" % (data[cur+2], data[cur+3]))
            print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
            cur += 4
    elif result == 0x91:
        result = data[cur+1]
        if result: 
            if result == 1:
                print("REG[%d] |= %d" % (data[cur+2], fourbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 7
            else: 
                print("REG[%d] |= %d" % (data[cur+2], eightbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6], data[cur+7], data[cur+8], data[cur+9], data[cur+10])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 11
        else:
            print("REG[%d] |= REG[%d]" % (data[cur+2], data[cur+3]))
            print("REG[%d] &= 0xffffffffffffffff"% data[cur+2])
            cur += 4
    elif result == 0xef:
        print("REG[%d] = ~REG[%d]" % (data[cur+1], data[cur+1]))
        cur += 2
    elif result == 0x2e:
        result = data[cur+1]
        result = data[cur+1]
        if result: 
            if result == 1:
                print("REG[%d] ^= %d" % (data[cur+2], fourbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 7
            else: 
                print("REG[%d] ^= %d" % (data[cur+2], eightbits(data[cur+3], data[cur+4], data[cur+5], data[cur+6], data[cur+7], data[cur+8], data[cur+9], data[cur+10])))
                print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
                cur += 11
        else:
            print("REG[%d] ^= REG[%d]" % (data[cur+2], data[cur+3]))
            print("REG[%d] &= 0xffffffffffffffff" % data[cur+2])
            cur += 4

실행결과는 아래와 같다.

<실행결과>

REG[0] ^= 9916956230313233502
REG[0] &= 0xffffffffffffffff
REG[0] += 17456412026526424132
REG[0] &= 0xffffffffffffffff
REG[0] ^= 16669111249775470057
REG[0] &= 0xffffffffffffffff
REG[0] = ~REG[0]
REG[0] ^= 13494573269112497585
REG[0] &= 0xffffffffffffffff
REG[0] += 10648006697692025873
REG[0] &= 0xffffffffffffffff
REG[0] = ~REG[0]
REG[0] -= 98751962342359805
REG[0] &= 0xffffffffffffffff
REG[1] ^= 14936966682722987908
REG[1] &= 0xffffffffffffffff
REG[1] += 6362136750145779099
REG[1] &= 0xffffffffffffffff
REG[1] ^= 2554385922081725706
REG[1] &= 0xffffffffffffffff
REG[1] = ~REG[1]
REG[1] ^= 10882839983365564277
REG[1] &= 0xffffffffffffffff
REG[1] += 15160171698711617780
REG[1] &= 0xffffffffffffffff
REG[1] = ~REG[1]
REG[1] -= 9857034802924911908
REG[1] &= 0xffffffffffffffff
REG[2] ^= 15342301905572705899
REG[2] &= 0xffffffffffffffff
REG[2] += 15319383285252614228
REG[2] &= 0xffffffffffffffff
REG[2] ^= 14449974489168053672
REG[2] &= 0xffffffffffffffff
REG[2] = ~REG[2]
REG[2] ^= 13598415237511222955
REG[2] &= 0xffffffffffffffff
REG[2] += 8199454823307448241
REG[2] &= 0xffffffffffffffff
REG[2] = ~REG[2]
REG[2] -= 13634334416995106013
REG[2] &= 0xffffffffffffffff
REG[3] ^= 6578703224312228052
REG[3] &= 0xffffffffffffffff
REG[3] += 16991869088846539430
REG[3] &= 0xffffffffffffffff
REG[3] ^= 249280991950343503
REG[3] &= 0xffffffffffffffff
REG[3] = ~REG[3]
REG[3] ^= 6985638513559728187
REG[3] &= 0xffffffffffffffff
REG[3] += 1613387814777486498
REG[3] &= 0xffffffffffffffff
REG[3] = ~REG[3]
REG[3] -= 5401196605745551267
REG[3] &= 0xffffffffffffffff
REG[4] ^= 2581510910733444495
REG[4] &= 0xffffffffffffffff
REG[4] += 15450863666303837559
REG[4] &= 0xffffffffffffffff
REG[4] ^= 10189793018597273008
REG[4] &= 0xffffffffffffffff
REG[4] = ~REG[4]
REG[4] ^= 12513777259171716699
REG[4] &= 0xffffffffffffffff
REG[4] += 17092290541331203191
REG[4] &= 0xffffffffffffffff
REG[4] = ~REG[4]
REG[4] -= 3500736538697890101
REG[4] &= 0xffffffffffffffff
REG[5] ^= 6156772802035562708
REG[5] &= 0xffffffffffffffff
REG[5] += 12618474528927264546
REG[5] &= 0xffffffffffffffff
REG[5] ^= 6132015332872876055
REG[5] &= 0xffffffffffffffff
REG[5] = ~REG[5]
REG[5] ^= 10587997614938883079
REG[5] &= 0xffffffffffffffff
REG[5] += 15795865682399464266
REG[5] &= 0xffffffffffffffff
REG[5] = ~REG[5]
REG[5] -= 16730897981035279827
REG[5] &= 0xffffffffffffffff
REG[15] |= REG[0]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[1]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[2]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[3]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[4]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[5]
REG[15] &= 0xffffffffffffffff

prob-begin과 마찬가지로 z3 모듈을 이용해서 v5[15]가 0일 때의 값을 찾는 코드를 작성해야 한다.

파이썬으로 작성한 것은 아래와 같다.

from z3 import *

FLAG = [BitVec('FLAG_%d' %x, 64) for x in range(6)]
REG = FLAG + [0] * 10

solver = Solver()

REG[0] ^= 9916956230313233502
REG[0] &= 0xffffffffffffffff
REG[0] += 17456412026526424132
REG[0] &= 0xffffffffffffffff
REG[0] ^= 16669111249775470057
REG[0] &= 0xffffffffffffffff
REG[0] = ~REG[0]
REG[0] ^= 13494573269112497585
REG[0] &= 0xffffffffffffffff
REG[0] += 10648006697692025873
REG[0] &= 0xffffffffffffffff
REG[0] = ~REG[0]
REG[0] -= 98751962342359805
REG[0] &= 0xffffffffffffffff
REG[1] ^= 14936966682722987908
REG[1] &= 0xffffffffffffffff
REG[1] += 6362136750145779099
REG[1] &= 0xffffffffffffffff
REG[1] ^= 2554385922081725706
REG[1] &= 0xffffffffffffffff
REG[1] = ~REG[1]
REG[1] ^= 10882839983365564277
REG[1] &= 0xffffffffffffffff
REG[1] += 15160171698711617780
REG[1] &= 0xffffffffffffffff
REG[1] = ~REG[1]
REG[1] -= 9857034802924911908
REG[1] &= 0xffffffffffffffff
REG[2] ^= 15342301905572705899
REG[2] &= 0xffffffffffffffff
REG[2] += 15319383285252614228
REG[2] &= 0xffffffffffffffff
REG[2] ^= 14449974489168053672
REG[2] &= 0xffffffffffffffff
REG[2] = ~REG[2]
REG[2] ^= 13598415237511222955
REG[2] &= 0xffffffffffffffff
REG[2] += 8199454823307448241
REG[2] &= 0xffffffffffffffff
REG[2] = ~REG[2]
REG[2] -= 13634334416995106013
REG[2] &= 0xffffffffffffffff
REG[3] ^= 6578703224312228052
REG[3] &= 0xffffffffffffffff
REG[3] += 16991869088846539430
REG[3] &= 0xffffffffffffffff
REG[3] ^= 249280991950343503
REG[3] &= 0xffffffffffffffff
REG[3] = ~REG[3]
REG[3] ^= 6985638513559728187
REG[3] &= 0xffffffffffffffff
REG[3] += 1613387814777486498
REG[3] &= 0xffffffffffffffff
REG[3] = ~REG[3]
REG[3] -= 5401196605745551267
REG[3] &= 0xffffffffffffffff
REG[4] ^= 2581510910733444495
REG[4] &= 0xffffffffffffffff
REG[4] += 15450863666303837559
REG[4] &= 0xffffffffffffffff
REG[4] ^= 10189793018597273008
REG[4] &= 0xffffffffffffffff
REG[4] = ~REG[4]
REG[4] ^= 12513777259171716699
REG[4] &= 0xffffffffffffffff
REG[4] += 17092290541331203191
REG[4] &= 0xffffffffffffffff
REG[4] = ~REG[4]
REG[4] -= 3500736538697890101
REG[4] &= 0xffffffffffffffff
REG[5] ^= 6156772802035562708
REG[5] &= 0xffffffffffffffff
REG[5] += 12618474528927264546
REG[5] &= 0xffffffffffffffff
REG[5] ^= 6132015332872876055
REG[5] &= 0xffffffffffffffff
REG[5] = ~REG[5]
REG[5] ^= 10587997614938883079
REG[5] &= 0xffffffffffffffff
REG[5] += 15795865682399464266
REG[5] &= 0xffffffffffffffff
REG[5] = ~REG[5]
REG[5] -= 16730897981035279827
REG[5] &= 0xffffffffffffffff
REG[15] |= REG[0]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[1]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[2]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[3]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[4]
REG[15] &= 0xffffffffffffffff
REG[15] |= REG[5]
REG[15] &= 0xffffffffffffffff

solver.add(REG[15] == 0)
solver.check()
model = solver.model()

#for i in FLAG:
#    print(i)

for i in FLAG:
    print(model[i].as_long().to_bytes(8, "little").decode(), end="")

L7{DO_U_HAVE_HEXRAYS_FOR_VIRTUAL_MACHINE?}

도움:

#https://msh1307.tistory.com/85

'Layer7 과제 > 리버싱' 카테고리의 다른 글

[VM problem] prob-3, prob-4 (0)	2022.09.02
[리버싱] prob-4 (0)	2022.08.16
[리버싱] prob-3 (0)	2022.08.16
[리버싱] prob-1 (0)	2022.08.16
[리버싱] prob-begin (0)	2022.08.16

현재글[리버싱] VM Problem:prob-begin, prob-1

kms0204

파이썬, 구현, 브루트 포스 알고리즘, 키워드 필터링 우회, brute force algorithm, 메모아이제이션, 리버싱, 문제풀이, null byte injection, XSS filtering bypass, 정렬, Greedy Algorithm, 브루트포스 알고리즘, pwndbg 명령어, 알고리즘, 그리디 알고리즘, 많은 조건 분기, 널 바이트 인젝션, 라이트업, 시간복잡도,

Today :
Yesterday :

kms0204