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