[리버싱] prob-3

문제를 보며 다음과 같다.

 

사용자로부터 16자리 문자열을 입력받는다.

 

그리고 if문을 통해서 입력값을 특정한 방법(+,  -, *)으로 검증한다.

만약 모든 조건을 만족시키는 입력값이라면 Correct!를 출력하고, 아니라면 Wrong...을 출력한다.

즉, 우리가 구해야하는 flag는 모든 조건을 만족시키는 입력값이다.

 

저 많은 조건들에 맞는 값을 하나하나 계산하는 것은 매우 비효율적이고 어려운 일이다.

따라서 컴퓨터가 알아서 조건을 만족시키는 값을 계산하도록 코드를 짜야한다.

 

이를 파이썬의 z3모듈을 이용해서 구현하면,

from z3 import *
FLAG = [Int("FLAG_%d" %i) for i in range(16)]

solver =Solver()
solver.add(FLAG[0] * FLAG[0] == 5776 )
solver.add( FLAG[0] + FLAG[1] == 131 )
solver.add( FLAG[0] - FLAG[2] == -47 )
solver.add( FLAG[0] - FLAG[3] == 7 )
solver.add( FLAG[0] * FLAG[4] == 6840 )
solver.add( FLAG[0] * FLAG[5] == 7220 )
solver.add( FLAG[0] - FLAG[6] == -4 )
solver.add( FLAG[0] + FLAG[7] == 158 )
solver.add( FLAG[0] + FLAG[8] == 155 )
solver.add( FLAG[0] - FLAG[9] == 10 )
solver.add( FLAG[0] * FLAG[10] == 7220 )
solver.add( FLAG[0] * FLAG[11] == 6308 )
solver.add( FLAG[0] - FLAG[12] == -3 )
solver.add( FLAG[0] * FLAG[13] == 5776 )
solver.add( FLAG[0] + FLAG[14] == 109 )
solver.add( FLAG[0] - FLAG[15] == -49)

if solver.check() == CheckSatResult(True):
  m = solver.model()
  for i in FLAG:
        print(chr(m[i].as_long()), end="")
  #print(m)
else:
  print("unsat")

위와 같다.

 

문자는 아스키 코드에 맞는 정수로 표현할 수 있기 때문에 int형 배열로 구현하였고, 마지막에 출력할 때 정수값에 해당하는 문자를 출력하도록 하였다.

 

 

실행시키면,

flag가 출력되는 것을 확인할 수 있다.