problem

int __cdecl main(int argc, const char **argv, const char **envp):
{
  char ord(s[0]) // [rsp+20h] [rbp-10h]
  int v5 // [rsp+2Ch] [rbp-4h]

  v5 = 1
if ( argc == 2 ):
  {
    s = argv[1]
  if ( strlen(s): == 42 ):
    {
    if ( ord(s[7]) + ord(s[13]) + ord(s[8]) != 269 ):
        v5 = 0
    if ( ord(s[0]) - ord(s[1]) + ord(s[14]) + ord(s[0]) != 165 ):
        v5 = 0
    if ( ord(s[34]) + ord(s[16]) * ord(s[21]) + ord(s[38]) != 9482 ):
        v5 = 0
    if ( ord(s[41]) + ord(s[8]) * ord(s[6]) + ord(s[23]) != 5500 ):
        v5 = 0
    if ( -ord(s[41]) - ord(s[21]) != -223 ):
        v5 = 0
    if ( ord(s[11]) * ord(s[4]) * ord(s[18]) + ord(s[19]) != 639710 ):
        v5 = 0
    if ( ord(s[23]) + ord(s[33]) * ord(s[34]) != 6403 ):
        v5 = 0
    if ( ord(s[18]) * ord(s[14]) - ord(s[33]) != 5072 ):
        v5 = 0
    if ( ord(s[24]) - ord(s[39]) - ord(s[30]) - ord(s[22]) != -110 ):
        v5 = 0
    if ( ord(s[10]) + ord(s[30]) - ord(s[19]) + ord(s[1]) != 110 ):
        v5 = 0
    if ( ord(s[15]) - ord(s[20]) - ord(s[41]) != -169 ):
        v5 = 0
    if ( ord(s[15]) * ord(s[35]) - ord(s[41]) * ord(s[8]) != -10231 ):
        v5 = 0
    if ( ord(s[36]) + ord(s[31]) * ord(s[11]) - ord(s[32]) != 8428 ):
        v5 = 0
    if ( ord(s[29]) + ord(s[25]) + ord(s[40]) != 289 ):
        v5 = 0
    if ( ord(s[7]) - ord(s[12]) + ord(s[24]) != 100 ):
        v5 = 0
    if ( ord(s[21]) * ord(s[30]) - ord(s[6]) != 9262 ):
        v5 = 0
    if ( ord(s[38]) * ord(s[33]) * ord(s[3]) != 480244 ):
        v5 = 0
    if ( ord(s[20]) - ord(s[31]) * ord(s[0]) - ord(s[2]) != -5954 ):
        v5 = 0
    if ( ord(s[27]) + ord(s[12]) * ord(s[21]) != 5095 ):
        v5 = 0
    if ( ord(s[6]) + ord(s[11]) * ord(s[8]) - ord(s[8]) != 10938 ):
        v5 = 0
    if ( ord(s[34]) - ord(s[5]) + ord(s[7]) * ord(s[24]) != 5014 ):
        v5 = 0
    if ( ord(s[40]) - ord(s[18]) - ord(s[2]) != -83 ):
        v5 = 0
    if ( ord(s[11]) - ord(s[31]) + ord(s[9]) * ord(s[24]) != 10114 ):
        v5 = 0
    if ( ord(s[41]) != 125 ): ------ solved
        v5 = 0
    if ( ord(s[28]) + ord(s[30]) - ord(s[3]) * ord(s[16]) != -6543 ):
        v5 = 0
    if ( ord(s[18]) * ord(s[25]) - ord(s[11]) != 5828 ):
        v5 = 0
    if ( ord(s[8]) * ord(s[9]) * ord(s[11]) != 1089000 ):
        v5 = 0
    if ( ord(s[3]) * ord(s[25]) - ord(s[29]) * ord(s[6]) != 2286 ):
        v5 = 0
    if ( ord(s[36]) - ord(s[7]) * ord(s[33]) != -3642 ):
        v5 = 0
    if ( ord(s[32]) - ord(s[1]) + ord(s[20]) != 73 ):
        v5 = 0
    if ( ord(s[39]) + ord(s[5]) * ord(s[4]) != 8307 ):
        v5 = 0
    if ( ord(s[0]) * ord(s[39]) * ord(s[8]) != 515460 ):
        v5 = 0
    if ( ord(s[12]) - ord(s[13]) + ord(s[31]) != 25 ):
        v5 = 0
    if ( ord(s[18]) + ord(s[10]) + ord(s[41]) + ord(s[41]) != 351 ):
        v5 = 0
    if ( ord(s[7]) + ord(s[14]) * ord(s[1]) + ord(s[22]) != 7624 ):
        v5 = 0
    if ( ord(s[27]) + ord(s[24]) * ord(s[18]) + ord(s[14]) != 5500 ):
        v5 = 0
    if ( ord(s[20]) - ord(s[41]) * ord(s[6]) + ord(s[18]) != -5853 ):
        v5 = 0
    if ( ord(s[33]) - ord(s[2]) - ord(s[25]) * ord(s[31]) != -9585 ):
        v5 = 0
    if ( ord(s[18]) * ord(s[11]) * ord(s[37]) != 353600 ):
        v5 = 0
    if ( ord(s[17]) + ord(s[8]) + ord(s[7]) - ord(s[39]) != 192 ):
        v5 = 0
    if ( ord(s[11]) - ord(s[35]) - ord(s[9]) * ord(s[31]) != -8285 ):
        v5 = 0
    if ( ord(s[23]) - ord(s[29]) + ord(s[39]) != 40 ):
        v5 = 0
    if ( ord(s[28]) + ord(s[10]) * ord(s[25]) * ord(s[20]) != 530777 ):
        v5 = 0
    if ( ord(s[32]) * ord(s[29]) * ord(s[3]) != 463914 ):
        v5 = 0
    if ( ord(s[32]) - ord(s[22]) + ord(s[30]) != 98 ):
        v5 = 0
    if ( ord(s[0]) - ord(s[13]) + ord(s[40]) - ord(s[38]) != -74 ):
        v5 = 0
    if ( ord(s[17]) + ord(s[21]) - ord(s[38]) != 108 ):
        v5 = 0
    if ( ord(s[0]) - ord(s[41]) * ord(s[23]) != -11804 ):
        v5 = 0
    if ( ord(s[2]) * ord(s[29]) * ord(s[27]) != 997645 ):
        v5 = 0
    if ( ord(s[25]) - ord(s[19]) * ord(s[35]) != -7476 ):
        v5 = 0
    if ( ord(s[16]) - ord(s[19]) * ord(s[7]) != -5295 ):
        v5 = 0
    if ( ord(s[33]) + ord(s[12]) * ord(s[26]) + ord(s[22]) != 2728 ):
        v5 = 0
    if ( ord(s[41]) + ord(s[24]) + ord(s[32]) != 281 ):
        v5 = 0
    if ( ord(s[23]) * ord(s[31]) * ord(s[14]) != 790020 ):
        v5 = 0
    if ( ord(s[35]) - ord(s[35]) * ord(s[6]) - ord(s[14]) != -3342 ):
        v5 = 0
    if ( ord(s[31]) + ord(s[40]) - ord(s[17]) * ord(s[25]) != -11148 ):
        v5 = 0
    if ( ord(s[36]) * ord(s[18]) + ord(s[13]) * ord(s[19]) != 16364 ):
        v5 = 0
    if ( ord(s[40]) - ord(s[5]) + ord(s[2]) * ord(s[18]) != 4407 ):
        v5 = 0
    if ( ord(s[21]) - ord(s[25]) + ord(s[3]) != 55 ):
        v5 = 0
    if ( ord(s[14]) + ord(s[14]) + ord(s[13]) - ord(s[2]) != 223 ):
        v5 = 0
    if ( ord(s[36]) * ord(s[35]) - ord(s[5]) * ord(s[29]) != -2449 ):
        v5 = 0
    if ( ord(s[41]) - ord(s[39]) + ord(s[1]) != 135 ):
        v5 = 0
    if ( ord(s[35]) - ord(s[0]) * ord(s[35]) + ord(s[0]) != -4759 ):
        v5 = 0
    if ( ord(s[8]) - ord(s[10]) * ord(s[21]) - ord(s[31]) != -4776 ):
        v5 = 0
    if ( ord(s[29]) - ord(s[24]) + ord(s[28]) != 126 ):
        v5 = 0
    if ( ord(s[0]) * ord(s[10]) - ord(s[32]) - ord(s[8]) != 3315 ):
        v5 = 0
    if ( ord(s[28]) * ord(s[32]) + ord(s[41]) != 5903 ):
        v5 = 0
    if ( ord(s[37]) - ord(s[24]) + ord(s[32]) != 20 ):
        v5 = 0
    if ( ord(s[20]) * ord(s[10]) - ord(s[15]) + ord(s[31]) != 4688 ):
        v5 = 0
    if ( ord(s[36]) - ord(s[9]) - ord(s[18]) * ord(s[18]) != -2721 ):
        v5 = 0
    if ( ord(s[9]) * ord(s[7]) + ord(s[16]) * ord(s[30]) != 13876 ):
        v5 = 0
    if ( ord(s[18]) + ord(s[34]) + ord(s[24]) - ord(s[7]) != 188 ):
        v5 = 0
    if ( ord(s[16]) * ord(s[27]) + ord(s[20]) != 9310 ):
        v5 = 0
    if ( ord(s[22]) - ord(s[30]) - ord(s[37]) - ord(s[9]) != -211 ):
        v5 = 0
    if ( ord(s[4]) * ord(s[41]) * ord(s[27]) - ord(s[38]) != 1491286 ):
        v5 = 0
    if ( ord(s[35]) - ord(s[29]) * ord(s[8]) + ord(s[13]) != -13131 ):
        v5 = 0
    if ( ord(s[23]) - ord(s[7]) - ord(s[24]) - ord(s[22]) != -107 ):
        v5 = 0
    if ( ord(s[37]) * ord(s[4]) * ord(s[5]) != 560388 ):
        v5 = 0
    if ( ord(s[17]) * ord(s[32]) - ord(s[15]) != 5295 ):
        v5 = 0
    if ( ord(s[32]) + ord(s[23]) * ord(s[18]) - ord(s[5]) != 4927 ):
        v5 = 0
    if ( ord(s[3]) + ord(s[8]) * ord(s[39]) + ord(s[39]) != 7397 ):
        v5 = 0
    if ( ord(s[7]) * ord(s[25]) - ord(s[3]) + ord(s[36]) != 5597 ):
        v5 = 0
    if ( ord(s[9]) - ord(s[24]) - ord(s[33]) != -79 ):
        v5 = 0
    if ( ord(s[30]) + ord(s[14]) * ord(s[36]) != 8213 ):
        v5 = 0
    if ( v5 == 1 ):
        puts(":): CORRECT!"):
      else
        puts("( INCORRECT"):
      return 0
    }
    else
    {
      puts("( INCORRECT"):
      return -1
    }
  }
  else
  {
    puts("Usage: ./binary <key>"):
    return -1
  }
}

정말 더럽다;;

이런 문제들은 사람 손으로 직접 풀 수 있기도 하지만 z3 또는 angr와 같은 python api를 사용하면 좀 더 쉽게 해결할 수 있다.

문제 풀 당시에는 z3를 사용해본적도 없고 angr밖에 생각이 안나서 angr로 삽질하다가 안되서 때려치고 writeup을 보고 z3를 왜 까먹고 있었지 해서 내가 본 그대로의 사용법(틀린 정보일 수 있음)을 다음에 이 글을 보고 다시 사용하기 위해 정리한다.

z3 usage

z3 documentation

https://ericpony.github.io/z3py-tutorial/guide-examples.htm

example code

보통 ctf에서는 flag를 구하기 위해 사용하기 때문에 정수/상수를 구하는 BitVec을 사용한다. 따라서 BitVec부분 예제만 가져왔다. 전체적인 사용법을 보고 싶다면 위 documentation link를 타고 들어가 확인하면 된다.

x = BitVec('x', 8)

위 코드는 x라는 이름의 8비트 크기의 비트벡터를 생성한다. char형은 1byte이니 8비트로 생성해주면 된다. 그 외의 구해야 하는 값이 더 큰 값이라면 알아서 조정해주면 된다.

from z3 import *

x = Int('x')
y = Int('y')

s = Solver()
print(s)

s.add(x > 10, y == x + 2)
print(s)
print("Solving constraints in the solver s ...")
print(s.check())

print(s.model())

우선 먼저 Solver()를 선언해준다.

그 후 문제 해결에 필요한 식을 s.add(x + 1 == 2)과 같이 선언해주면 된다.

check()함수를 사용하면 해당 식의 풀이를 시작한다. 그 후 해가 만족스럽다면 sat(satisfiable), 만족스럽지 않다면 unsat(unsatisfiable)을 반환한다.

model()함수를 사용하면 z3 API에서 찾은 해를 출력한다.

그런데 여기서 해를 보면 알 수 있듯이 [x = 11, y = 13]이 출력되었다. 하지만 실제 x,y의 값은 [x = 12, y = 14]와 같이 여러가지가 있을 수 있다. 그렇기 때문에 정확한 해를 알고 싶다면 식은 많으면 많을 수록 좋을 것 같다고 생각한다.

solve code

우선 나는 angr만 삽질하느라 z3를 이용한 풀이로 제시간에 풀어내지 못했기 때문에 다른 사람의 writeup 링크를 첨부한다. 같이 확인해보면 좋을 것 같다.

reference

https://github.com/0xpurpler0se/CTF-Writeups/blob/main/FooBar CTF 2022/baby_rev.md

<!doctype html>

C언어와 어셈블리어로 스택 프레임 이해하기!

우선 더하기를 해주는 간단한 함수를 만들고 그 함수를 예제로 설명해보겠다.

#include <stdio.h>

int sum(int a, int b) {
return a + b;
}

int main(void) {
int c = sum(1, 2);
printf("%d\n",c);
return c;
}

위 함수는 두 인자 a, b 를 받아서 더한 값을 반환한뒤 그 값을 출력해주는 함수이다.

그럼 이제 어셈블리어로 살펴보자

위 사진은 앞서 보았던 함수의 main 부분이다. 순서대로 내려가 보면
push rbp      로 rbp를 깔아주고
mov rsp, rbp 로 rsp를 rbp 위치로 끌고온다.
sub 16, rsp   로 16만큼의 공간을 만들어주고
mov 2, esi    로 esi의 2라는 값을
mov 1, edi    로 edi의 1이라는 값을 넣어준다. 그 후
call sum       으로 sum 함수를 불러주게 된다.

sum 함수의 부분은 이렇게 생겼는데 앞서와 순서는 똑같다.
push rbp            로 rbp를 깔아주고
mov rsp, rbp       로 rsp레지스터를 rbp로 가져와 준다.
mov edi, -4rbp    로 rbp에서 4만큼의 할당받은 공간에 main함수에서 넣었던 edi, 즉, 1이라는 값을 넣어주고
mov esi, -8rbp    로 rbp에서 8만큼 할당받은 공간에 main함수에서 넣었던 esi, 2라는 값을 넣어준다
mov -4rbp, edx   로 연산을 위해 4만큼 할당받은 rbp에 있는 값 즉, 1을 edx레지스터에 넣어주고
mov -8rbp, eax   로 마찬가지로 eax에 2라는 값을 넣어준다.
add edx, eax      로 eax와 edx를 더하여 eax에 더한 3이라는 값을 저장해주고
pop rbp
ret                   으로 다시 main 함수로 return 돌아가준다. 이 때 eax는 반환값으로 가지고 돌아간다!

그럼 다시 main 함수 부분으로 돌아와서 그 후에 관한 내용은 아직 공부가 부족하기 때문에 후에 더 공부한 뒤 정리하도록 하겠다.

아무튼 그 후
call printf 로 printf 함수를 불러와 3을 출력해준뒤
leave
ret          으로 다시 main함수를 불러왔던 곳으로 되돌아가 준다.