[리버싱] prob-4

문제를 보면,

위와 같다.

 

사용자로부터 최대 길이 32인 문자열을 입력받는다.

그리고 if문에서 이를 특정한 방법으로 검증하고, 모든 조건을 만족시키는 값이라면 Correct! 가 출력되고 아니라면 Wrong...이 출력된다.

 

(그동안의 문제를 보면, 아마도 flag의 길이가 32일 것이라고 추측할 수 있다. 물론 32라고 확답할 수 없기 때문에 문제를 풀 때 별로 도움이 되지는 않는다. 하지만, if문을 보면 data[0], data[1], data[2], data[3] 4개를 검증한다는 것을 알 수 있다.

이는 flag를 네 부분으로 나눠서 검증한다고 볼 수 있다)

 

 

모든 조건을 만족시키는 값을 일일이 구할 수는 없으니 파이썬의 z3 모듈을 사용해서 코드르 짜야한다.

if문을 보면 data[0], data[1], data[2], data[3] 4개를 검증하고 있으므로, 이를 참고해서 코드를 짜면,

from z3 import *
FLAG = [BitVec("FLAG_%d" %i, 64) for i in range(4)]

solver = Solver()
solver.add((FLAG[0] ^ 0x0DD8E7527EE669B1) == 0x5487A31B3A9D5EFD ) 
solver.add((FLAG[0] ^ FLAG[1]) == 0x1C0B170809246203 ) 
solver.add((FLAG[0] ^ FLAG[2]) == 0x151017167721681E ) 
solver.add((FLAG[0] ^ FLAG[3]) == 0x24080B1E7B29721A ) 
solver.add((FLAG[1] ^ FLAG[2]) == 0x091B001E7E050A1D ) 
solver.add((FLAG[1] ^ FLAG[3]) == 0x38031C16720D1019 ) 
solver.add((FLAG[2] ^ FLAG[3]) == 0x31181C080C081A04)
if solver.check() == CheckSatResult(True):
  m = solver.model()
  #print(m)
  for i in FLAG: 
    print(m[i].as_long().to_bytes(64, "little").decode(), end="")
else:
  print("unsat")

 위와 같다.

 

 

실행시키면,

모든 조건을 만족시키는 값, 즉 flag가 출력되는 것을 확인할 수 있다.