[리버싱] prob-1

사용자로부터 입력을 받고, if문들을 통해서 특정 조건을 만족시키는 값인지 확인하다.

모든 if문이 참이 되는 값이라면 Correct!를 출력하고 아니라면 Wrong...을 출력한다.

 

if문을 보면 v4, v5 변수만 다룬다.

v4와 v5가 flag 값의 앞쪽 반과 뒤쪽 반을 담당한다.

 

if문의 조건들을 일일이 손으로 해보는 것은 미친짓이다...

따라서 파이썬의 z3모듈을 이용해서 컴퓨터가 조건에 맞는 값을 대신 구하도록 해야된다.

 

if문을 보면 숫자 뒤에 LL이 붙어있는데, 이는 파이썬에서는 의미가 없으므로 때어버리면 된다.

 

코드로 구현하면 아래와 같다.

from z3 import *

v4 = BitVec('v4', 64)
v5 = BitVec('v5', 64)

solver = Solver()
solver.add( ((((((((((((((((((((((((((((((((v4 + 618) ^ 0x521C7AB5077FEA22) - 884) ^ 0x34AEFEFFD2BE41D3) + 811) ^ 0xFFA20399E857DAFC)
                               + 356) ^ 0xD811EABA884C68)
                             + 1252) ^ 0xD0EC8D350D9AA905)
                           + 555) ^ 0xC4E4D2A7E6B35F57)
                         + 1358) ^ 0xC31407FF9686D40D)
                       + 605) ^ 0xDF4136F72FB0D862)
                     - 108) ^ 0x6AB43A5BDB709612)
                   + 129) ^ 0x5FD86CD843B30CF3)
                 + 541) ^ 0x211A872767CC609C)
               - 128) ^ 0xA32ADE5A42DE6A34)
             + 1585) ^ 0xB45B1F28E6FE94F1)
           - 85) ^ 0x2DEA5C9A8BE9E966)    
         - 896) ^ 0x24A62556A3898AF8)
       + 345) ^ 0xCC77A4E422F59608) == 0x8FB6A12D3C02D8E )

solver.add(((((((((((((((((((((((((((((((((v5 - 804) ^ 0xA6F61960DF964F7) - 163) ^ 0x4AAE46A712CA8B43) + 137) ^ 0x40A136AAFEAA901B)
                               - 1442) ^ 0xA4E32F4CFD49668B)
                             + 1872) ^ 0x45B1883BCFC7E2D)
                           - 1250) ^ 0x38DCC9F569D48A08)
                         + 1812) ^ 0xE1A9C472A31D85)
                       - 1842) ^ 0x789735E924D46067)
                     + 1884) ^ 0x9D37986D93C1416D)
                   + 2044) ^ 0x892E142ECD21BF58)
                 + 1732) ^ 0xF756FB4FD96102)
               - 1936) ^ 0x6C7535646EFC1951)
             - 1691) ^ 0x4F66B0F05114A5A3)
           - 227) ^ 0x8B0E8EBA60979122)
         - 1777) ^ 0x246657EC1EA71A77)
       - 379) ^ 0x1577B13C72C502C7) == 0x10AF1199F2ECA8A1)

solver.check()
m = solver.model()
print(m[v4].as_long().to_bytes(8, "little").decode(), end = "")
print(m[v5].as_long().to_bytes(8, "little").decode())

 

실행시키면,

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