Layer7 - 리버싱 9차시 과제

 

prob-begin

 

int __cdecl main(int argc, const char **argv, const char **envp)
{
  char s[16]; // [rsp+0h] [rbp-210h] BYREF
  unsigned __int64 v5; // [rsp+208h] [rbp-8h]

  v5 = __readfsqword(0x28u);
  printf("Flag: ");
  __isoc99_scanf("%16s", s);
  if ( strlen(s) == 16
    && 378 * s[14]
     + 809 * s[13]
     + -967 * s[12]
     + 362 * s[11]
     + -404 * s[10]
     + 429 * s[9]
     + 463 * s[8]
     + -449 * s[7]
     + 851 * s[6]
     + 417 * s[5]
     + -778 * s[4]
     + 787 * s[3]
     + 857 * s[2]
     + -332 * s[1]
     + 580 * s[0]
     + 975 * s[15] == 387910
    && 600 * s[10]
     + 401 * s[9]
     + -619 * s[8]
     + 140 * s[7]
     + -167 * s[6]
     + 79 * s[5]
     + 395 * s[4]
     + -187 * s[3]
     + -794 * s[2]
     + 956 * s[1]
     + 558 * s[0]
     - 219 * s[11]
     - 60 * s[12]
     + 368 * s[13]
     + 11 * s[14]
     + 798 * s[15] == 165058
    && 375 * s[14]
     + 70 * s[13]
     + -396 * s[12]
     + 553 * s[11]
     + 420 * s[10]
     + 181 * s[9]
     + -484 * s[8]
     + 622 * s[7]
     + -817 * s[6]
     + -171 * s[5]
     + -122 * s[4]
     + -964 * s[3]
     + -951 * s[2]
     + -668 * s[1]
     + 897 * s[0]
     - 541 * s[15] == -178457
    && -623 * s[14]
     + -821 * s[11]
     + -251 * s[10]
     + 332 * s[9]
     + -791 * s[8]
     + 477 * s[7]
     + 88 * s[6]
     + 868 * s[5]
     + 764 * s[4]
     + 237 * s[3]
     + 739 * s[2]
     + 350 * s[1]
     + 853 * s[0]
     - 535 * s[12]
     + 160 * s[13]
     + 483 * s[15] == 256024
    && 860 * s[14]
     + -639 * s[13]
     + 882 * s[12]
     + -503 * s[11]
     + 279 * s[10]
     + 274 * s[9]
     + -285 * s[8]
     + 167 * s[7]
     + -34 * s[6]
     + -438 * s[5]
     + 578 * s[4]
     + -290 * s[3]
     + 684 * s[2]
     + 394 * s[1]
     + 79 * s[0]
     - 865 * s[15] == 38190
    && 452 * s[14]
     + 132 * s[13]
     + 523 * s[12]
     + -142 * s[11]
     + -957 * s[10]
     + 280 * s[9]
     + -141 * s[8]
     + -350 * s[7]
     + 904 * s[6]
     + -54 * s[5]
     + -648 * s[4]
     + 797 * s[3]
     + -993 * s[2]
     + 105 * s[1]
     + 803 * s[0]
     + 711 * s[15] == 55338
    && -671 * s[12]
     + 765 * s[11]
     + 331 * s[10]
     + -285 * s[9]
     + -872 * s[8]
     + 773 * s[5]
     + -356 * s[4]
     + 186 * s[3]
     + -786 * s[2]
     + 120 * s[1]
     + 209 * s[0]
     - 763 * s[6]
     - 768 * s[7]
     - 141 * s[13]
     + 127 * s[14]
     - 718 * s[15] == -251396
    && -599 * s[12]
     + 552 * s[11]
     + 492 * s[10]
     + -910 * s[9]
     + -566 * s[8]
     + 118 * s[7]
     + -35 * s[6]
     + 79 * s[5]
     + -716 * s[4]
     + 725 * s[3]
     + -53 * s[2]
     + 269 * s[1]
     + 349 * s[0]
     - 894 * s[13]
     + 80 * s[14]
     - 135 * s[15] == -156336
    && -936 * s[14]
     + 60 * s[13]
     + 211 * s[12]
     + -355 * s[11]
     + 186 * s[10]
     + 180 * s[9]
     + -157 * s[8]
     + -391 * s[7]
     + -67 * s[6]
     + -539 * s[5]
     + 925 * s[4]
     + -882 * s[3]
     + -300 * s[2]
     + 151 * s[1]
     + 810 * s[0]
     + 978 * s[15] == 87475
    && -897 * s[14]
     + 852 * s[13]
     + 456 * s[12]
     + -191 * s[11]
     + -39 * s[10]
     + 521 * s[9]
     + -408 * s[8]
     + 460 * s[7]
     + -172 * s[6]
     + -103 * s[5]
     + -356 * s[4]
     + -350 * s[3]
     + -583 * s[2]
     + 56 * s[0]
     + 7 * s[1]
     - 412 * s[15] == -116118
    && 852 * s[14]
     + 142 * s[13]
     + 109 * s[12]
     + -234 * s[11]
     + -843 * s[10]
     + -731 * s[9]
     + 153 * s[8]
     + 694 * s[7]
     + -806 * s[6]
     + 891 * s[5]
     + 321 * s[4]
     + -783 * s[3]
     + -298 * s[2]
     + 756 * s[1]
     + 215 * s[0]
     - 65 * s[15] == 3287
    && -753 * s[14]
     + 943 * s[13]
     + 982 * s[12]
     + -486 * s[11]
     + 968 * s[10]
     + -491 * s[9]
     + 978 * s[8]
     + 805 * s[7]
     + -245 * s[6]
     + -643 * s[5]
     + -840 * s[4]
     + 762 * s[3]
     + 711 * s[2]
     + 14 * s[1]
     + 104 * s[0]
     + 914 * s[15] == 266806
    && 984 * s[14]
     + -669 * s[11]
     + -166 * s[10]
     + 310 * s[9]
     + 510 * s[8]
     + -83 * s[7]
     + -586 * s[6]
     + -458 * s[5]
     + 732 * s[4]
     + -478 * s[3]
     + 322 * s[2]
     + -653 * s[1]
     + 363 * s[0]
     - 88 * s[12]
     - 60 * s[13]
     + 982 * s[15] == 178175
    && -677 * s[14]
     + -903 * s[13]
     + -265 * s[12]
     + -193 * s[11]
     + -408 * s[10]
     + 913 * s[9]
     + -556 * s[8]
     + -782 * s[7]
     + -151 * s[6]
     + 927 * s[5]
     + 789 * s[4]
     + 340 * s[3]
     + 581 * s[2]
     + 538 * s[1]
     + 702 * s[0]
     - 260 * s[15] == 122419
    && -259 * s[14]
     + 510 * s[13]
     + 176 * s[12]
     + -278 * s[11]
     + -738 * s[10]
     + 538 * s[9]
     + -481 * s[8]
     + 748 * s[7]
     + -852 * s[6]
     + 331 * s[5]
     + 468 * s[4]
     + 217 * s[1]
     + 486 * s[0]
     - 525 * s[2]
     + 24 * s[3]
     + 562 * s[15] == 112902
    && 392 * s[12]
     + 300 * s[11]
     + -59 * s[10]
     + -988 * s[9]
     + 761 * s[8]
     + -102 * s[7]
     + 295 * s[6]
     + 121 * s[5]
     + 924 * s[4]
     + -879 * s[3]
     + 448 * s[2]
     + -901 * s[1]
     + 759 * s[0]
     - 187 * s[13]
     - 224 * s[14]
     + 789 * s[15] == 194594 )
  {
    puts("Correct! Flag is ur input");
    return 0;
  }
  else
  {
    puts("Wrong");
    return 0;
  }
}

 

s가 우리의 인풋이 들어가는 배열이다. 변수가 따로따로 있길래 IDA에서 y를 눌러서 타입을 배열로 바꿔줬다. if문에 엄청난 조건식을 전부 만족하는 입력이 플래그이다. 따라서 우리는 방정식을 풀어줘야 하는데 z3 solver를 사용해서 아주 쉽게 방정식을 풀 수 있다.

 

from z3 import *

s = [BitVec('a%i'%i, 8) for i in range(16)]

sol = Solver()

sol.add(378 * s[14]
    + 809 * s[13]
    + -967 * s[12]
    + 362 * s[11]
    + -404 * s[10]
    + 429 * s[9]
    + 463 * s[8]
    + -449 * s[7]
    + 851 * s[6]
    + 417 * s[5]
    + -778 * s[4]
    + 787 * s[3]
    + 857 * s[2]
    + -332 * s[1]
    + 580 * s[0]
    + 975 * s[15] == 387910)
sol.add(600 * s[10]
    + 401 * s[9]
    + -619 * s[8]
    + 140 * s[7]
    + -167 * s[6]
    + 79 * s[5]
    + 395 * s[4]
    + -187 * s[3]
    + -794 * s[2]
    + 956 * s[1]
    + 558 * s[0]
    - 219 * s[11]
    - 60 * s[12]
    + 368 * s[13]
    + 11 * s[14]
    + 798 * s[15] == 165058)
sol.add(375 * s[14]
    + 70 * s[13]
    + -396 * s[12]
    + 553 * s[11]
    + 420 * s[10]
    + 181 * s[9]
    + -484 * s[8]
    + 622 * s[7]
    + -817 * s[6]
    + -171 * s[5]
    + -122 * s[4]
    + -964 * s[3]
    + -951 * s[2]
    + -668 * s[1]
    + 897 * s[0]
    - 541 * s[15] == -178457)
sol.add(-623 * s[14]
     + -821 * s[11]
     + -251 * s[10]
     + 332 * s[9]
     + -791 * s[8]
     + 477 * s[7]
     + 88 * s[6]
     + 868 * s[5]
     + 764 * s[4]
     + 237 * s[3]
     + 739 * s[2]
     + 350 * s[1]
     + 853 * s[0]
     - 535 * s[12]
     + 160 * s[13]
     + 483 * s[15] == 256024)
sol.add(860 * s[14]
     + -639 * s[13]
     + 882 * s[12]
     + -503 * s[11]
     + 279 * s[10]
     + 274 * s[9]
     + -285 * s[8]
     + 167 * s[7]
     + -34 * s[6]
     + -438 * s[5]
     + 578 * s[4]
     + -290 * s[3]
     + 684 * s[2]
     + 394 * s[1]
     + 79 * s[0]
     - 865 * s[15] == 38190)
sol.add(452 * s[14]
     + 132 * s[13]
     + 523 * s[12]
     + -142 * s[11]
     + -957 * s[10]
     + 280 * s[9]
     + -141 * s[8]
     + -350 * s[7]
     + 904 * s[6]
     + -54 * s[5]
     + -648 * s[4]
     + 797 * s[3]
     + -993 * s[2]
     + 105 * s[1]
     + 803 * s[0]
     + 711 * s[15] == 55338)
sol.add(-671 * s[12]
     + 765 * s[11]
     + 331 * s[10]
     + -285 * s[9]
     + -872 * s[8]
     + 773 * s[5]
     + -356 * s[4]
     + 186 * s[3]
     + -786 * s[2]
     + 120 * s[1]
     + 209 * s[0]
     - 763 * s[6]
     - 768 * s[7]
     - 141 * s[13]
     + 127 * s[14]
     - 718 * s[15] == -251396)
sol.add(-599 * s[12]
     + 552 * s[11]
     + 492 * s[10]
     + -910 * s[9]
     + -566 * s[8]
     + 118 * s[7]
     + -35 * s[6]
     + 79 * s[5]
     + -716 * s[4]
     + 725 * s[3]
     + -53 * s[2]
     + 269 * s[1]
     + 349 * s[0]
     - 894 * s[13]
     + 80 * s[14]
     - 135 * s[15] == -156336)
sol.add(-936 * s[14]
     + 60 * s[13]
     + 211 * s[12]
     + -355 * s[11]
     + 186 * s[10]
     + 180 * s[9]
     + -157 * s[8]
     + -391 * s[7]
     + -67 * s[6]
     + -539 * s[5]
     + 925 * s[4]
     + -882 * s[3]
     + -300 * s[2]
     + 151 * s[1]
     + 810 * s[0]
     + 978 * s[15] == 87475)
sol.add(-897 * s[14]
     + 852 * s[13]
     + 456 * s[12]
     + -191 * s[11]
     + -39 * s[10]
     + 521 * s[9]
     + -408 * s[8]
     + 460 * s[7]
     + -172 * s[6]
     + -103 * s[5]
     + -356 * s[4]
     + -350 * s[3]
     + -583 * s[2]
     + 56 * s[0]
     + 7 * s[1]
     - 412 * s[15] == -116118)
sol.add(852 * s[14]
     + 142 * s[13]
     + 109 * s[12]
     + -234 * s[11]
     + -843 * s[10]
     + -731 * s[9]
     + 153 * s[8]
     + 694 * s[7]
     + -806 * s[6]
     + 891 * s[5]
     + 321 * s[4]
     + -783 * s[3]
     + -298 * s[2]
     + 756 * s[1]
     + 215 * s[0]
     - 65 * s[15] == 3287)
sol.add(-753 * s[14]
     + 943 * s[13]
     + 982 * s[12]
     + -486 * s[11]
     + 968 * s[10]
     + -491 * s[9]
     + 978 * s[8]
     + 805 * s[7]
     + -245 * s[6]
     + -643 * s[5]
     + -840 * s[4]
     + 762 * s[3]
     + 711 * s[2]
     + 14 * s[1]
     + 104 * s[0]
     + 914 * s[15] == 266806)
sol.add(984 * s[14]
     + -669 * s[11]
     + -166 * s[10]
     + 310 * s[9]
     + 510 * s[8]
     + -83 * s[7]
     + -586 * s[6]
     + -458 * s[5]
     + 732 * s[4]
     + -478 * s[3]
     + 322 * s[2]
     + -653 * s[1]
     + 363 * s[0]
     - 88 * s[12]
     - 60 * s[13]
     + 982 * s[15] == 178175)
sol.add(-677 * s[14]
     + -903 * s[13]
     + -265 * s[12]
     + -193 * s[11]
     + -408 * s[10]
     + 913 * s[9]
     + -556 * s[8]
     + -782 * s[7]
     + -151 * s[6]
     + 927 * s[5]
     + 789 * s[4]
     + 340 * s[3]
     + 581 * s[2]
     + 538 * s[1]
     + 702 * s[0]
     - 260 * s[15] == 122419)
sol.add(-259 * s[14]
     + 510 * s[13]
     + 176 * s[12]
     + -278 * s[11]
     + -738 * s[10]
     + 538 * s[9]
     + -481 * s[8]
     + 748 * s[7]
     + -852 * s[6]
     + 331 * s[5]
     + 468 * s[4]
     + 217 * s[1]
     + 486 * s[0]
     - 525 * s[2]
     + 24 * s[3]
     + 562 * s[15] == 112902)
sol.add(392 * s[12]
     + 300 * s[11]
     + -59 * s[10]
     + -988 * s[9]
     + 761 * s[8]
     + -102 * s[7]
     + 295 * s[6]
     + 121 * s[5]
     + 924 * s[4]
     + -879 * s[3]
     + 448 * s[2]
     + -901 * s[1]
     + 759 * s[0]
     - 187 * s[13]
     - 224 * s[14]
     + 789 * s[15] == 194594)

if sol.check() == sat:
    res = sol.model()
    for i in s:
        print(chr(int(str(res[i]))), end='')

 

z3 solver에 그대로 때려박으면 풀리는 ezpz한 문제이다.

 

 

prob-1

 

 

int __cdecl main(int argc, const char **argv, const char **envp)
{
  __int64 v4; // [rsp+100h] [rbp-20h] BYREF
  __int64 v5; // [rsp+108h] [rbp-18h]
  __int64 v6; // [rsp+110h] [rbp-10h]
  unsigned __int64 v7; // [rsp+118h] [rbp-8h]

  v7 = __readfsqword(0x28u);
  v4 = 0LL;
  v5 = 0LL;
  v6 = 0LL;
  printf("Flag: ");
  __isoc99_scanf("%16s", &v4);
  if ( ((((((((((((((((((((((((((((((((v4 + 618) ^ 0x521C7AB5077FEA22LL) - 884) ^ 0x34AEFEFFD2BE41D3LL) + 811) ^ 0xFFA20399E857DAFCLL)
                               + 356) ^ 0xD811EABA884C68LL)
                             + 1252) ^ 0xD0EC8D350D9AA905LL)
                           + 555) ^ 0xC4E4D2A7E6B35F57LL)
                         + 1358) ^ 0xC31407FF9686D40DLL)
                       + 605) ^ 0xDF4136F72FB0D862LL)
                     - 108) ^ 0x6AB43A5BDB709612LL)
                   + 129) ^ 0x5FD86CD843B30CF3LL)
                 + 541) ^ 0x211A872767CC609CLL)
               - 128) ^ 0xA32ADE5A42DE6A34LL)
             + 1585) ^ 0xB45B1F28E6FE94F1LL)
           - 85) ^ 0x2DEA5C9A8BE9E966LL)
         - 896) ^ 0x24A62556A3898AF8LL)
       + 345) ^ 0xCC77A4E422F59608LL) == 0x8FB6A12D3C02D8ELL
    && ((((((((((((((((((((((((((((((((v5 - 804) ^ 0xA6F61960DF964F7LL) - 163) ^ 0x4AAE46A712CA8B43LL) + 137) ^ 0x40A136AAFEAA901BLL)
                               - 1442) ^ 0xA4E32F4CFD49668BLL)
                             + 1872) ^ 0x45B1883BCFC7E2DLL)
                           - 1250) ^ 0x38DCC9F569D48A08LL)
                         + 1812) ^ 0xE1A9C472A31D85LL)
                       - 1842) ^ 0x789735E924D46067LL)
                     + 1884) ^ 0x9D37986D93C1416DLL)
                   + 2044) ^ 0x892E142ECD21BF58LL)
                 + 1732) ^ 0xF756FB4FD96102LL)
               - 1936) ^ 0x6C7535646EFC1951LL)
             - 1691) ^ 0x4F66B0F05114A5A3LL)
           - 227) ^ 0x8B0E8EBA60979122LL)
         - 1777) ^ 0x246657EC1EA71A77LL)
       - 379) ^ 0x1577B13C72C502C7LL) == 0x10AF1199F2ECA8A1LL )
  {
    puts("Correct!");
  }
  else
  {
    puts("Wrong...");
  }
  return 0;
}

 

이번에도 아까와 같이 방정식을 푸는 문제이다. 주의할점은 8바이트씩 연산을 진행한다는 것이다. 따라서 64비트짜리 BitVec를 2개 만들고 z3 solver돌리면 해가 나올 것이다. 이거를 리틀 엔디안 고려해서 문자열로 바꿔주면 된다.

 

from z3 import *
from pwn import *

v = [BitVec('a%i'%i, 64) for i in range(2)]

s = Solver()

s.add(((((((((((((((((((((((((((((((((v[0] + 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)
s.add(((((((((((((((((((((((((((((((((v[1] - 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)

if s.check() == sat:
    res = s.model()
    for i in v:
        print(p64(int(str(res[i]))).decode(), end='')

 

리틀 엔디안으로 바꿔서 출력해줄땐 struct.pack을 사용해도 되지만 간단하게 pwntools의 p64함수를 사용해줬다.

 

 

prob-3

 

#include <stdio.h>
#include <stdlib.h>

int main()
{
    char data[16 + 1] = {0};
    printf("Flag: ");
    scanf("%16s", data);

    if (data[0] * data[0] == 5776 && data[0] + data[1] == 131 && data[0] - data[2] == -47 && data[0] - data[3] == 7 && data[0] * data[4] == 6840 && data[0] * data[5] == 7220 && data[0] - data[6] == -4 && data[0] + data[7] == 158 && data[0] + data[8] == 155 && data[0] - data[9] == 10 && data[0] * data[10] == 7220 && data[0] * data[11] == 6308 && data[0] - data[12] == -3 && data[0] * data[13] == 5776 && data[0] + data[14] == 109 && data[0] - data[15] == -49)
        printf("Correct!\n");
    else
        printf("Wrong...\n");

    return 0;
}

 

이제는 ELF가 아닌 C언어로 준다. 갑자기 C로 바뀐거에 대해서는 사연이 있는데.. 큼.. 말을 아끼도록 하겠다. 아무튼 이것도 방정식 푸는 문제이다.

 

from z3 import *

data = [BitVec('data%i'%i, 8) for i in range(16)]

s = Solver()

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

if s.check() == sat:
    res = s.model()
    for i in range(len(res)):
        print(chr(int(str(res[data[i]]))&0xff), end='')

 

그냥 이렇게 때려박으면 풀리는 ezpzzzlol한 문제이다. 라고 할 뻔 했지만

 

 

...?????

 

[data15 = 5,
 data14 = 153,
 data12 = 215,
 data9 = 202,
 data8 = 199,
 data7 = 202,
 data6 = 216,
 data3 = 205,
 data2 = 3,
 data1 = 175,
 data5 = 57,
 data0 = 212,
 data11 = 37,
 data13 = 20,
 data4 = 54,
 data10 = 57]

 

해의 상태가 너무 이상하다.

 

from z3 import *

data = [Int('data%i'%i) for i in range(16)]

s = Solver()

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

s.check()
print(s.model())

 

BitVec를 Int로 바꾸고 다시 시도 해봤더니

 

[data1 = 207,
 data7 = 234,
 data8 = 231,
 data14 = 185,
 data2 = -29,
 data15 = -27,
 data10 = -95,
 data5 = -95,
 data4 = -90,
 data11 = -83,
 data6 = -72,
 data12 = -73,
 data3 = -83,
 data0 = -76,
 data13 = -76,
 data9 = -86]

 

음수 해가 나올때가 있다.

 

s.add(data[0] > 0)
s.add(data[1] > 0)
s.add(data[2] > 0)
s.add(data[3] > 0)
s.add(data[4] > 0)
s.add(data[5] > 0)
s.add(data[6] > 0)
s.add(data[7] > 0)
s.add(data[8] > 0)
s.add(data[9] > 0)
s.add(data[10] > 0)
s.add(data[11] > 0)
s.add(data[12] > 0)
s.add(data[13] > 0)
s.add(data[14] > 0)
s.add(data[15] > 0)

 

그래서 이렇게 조건을 추가해봤다.

 

[data3 = 69,
 data8 = 79,
 data9 = 66,
 data0 = 76,
 data6 = 80,
 data10 = 95,
 data4 = 90,
 data14 = 33,
 data2 = 123,
 data7 = 82,
 data12 = 79,
 data1 = 55,
 data11 = 83,
 data15 = 125,
 data5 = 95,
 data13 = 76]

 

이제야 ascii범위로 잘 나오는것 같다.

 

from z3 import *

data = [Int('data%i'%i) for i in range(16)]

s = Solver()

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

if s.check() == sat:
    res = s.model()
    for i in range(len(res)):
        print(chr(int(str(res[data[i]]))&0xff), end='')

 

문자열로 출력해보면

 

 

이제야 제대로 나온다. z3가 왜 BitVec에서 고장나는진 잘 모르겠지만 비트 연산 없는 방정식에서는 Int를 써야겠다.

 

 

prob-4

 

#include <stdio.h>
#include <stdlib.h>

int main()
{
    unsigned long long data[4 + 1];
    printf("Flag: ");
    scanf("%32s", data);

    if ((data[0] ^ 0x0DD8E7527EE669B1) == 0x5487A31B3A9D5EFD && (data[0] ^ data[1]) == 0x1C0B170809246203 && (data[0] ^ data[2]) == 0x151017167721681E && (data[0] ^ data[3]) == 0x24080B1E7B29721A && (data[1] ^ data[2]) == 0x091B001E7E050A1D && (data[1] ^ data[3]) == 0x38031C16720D1019 && (data[2] ^ data[3]) == 0x31181C080C081A04)
        printf("Correct!\n");
    else
        printf("Wrong...\n");

    return 0;
}

 

이 문제도 마찬가지로 C언어로 제공되고 방정식을 풀어야 한다. prob-1처럼 8바이트 단위로 연산을 진행하니까 아까와 비슷하게 z3 solver로 8바이트 해를 구해주고 pwntools의 p64함수를 이용해서 문자열로 변환해줬다.

 

from z3 import *
from pwn import *

data = [BitVec('data%i'%i, 64) for i in range(4)]

s = Solver()

s.add((data[0] ^ 0x0DD8E7527EE669B1) == 0x5487A31B3A9D5EFD)
s.add((data[0] ^ data[1]) == 0x1C0B170809246203)
s.add((data[0] ^ data[2]) == 0x151017167721681E)
s.add((data[0] ^ data[3]) == 0x24080B1E7B29721A)
s.add((data[1] ^ data[2]) == 0x091B001E7E050A1D)
s.add((data[1] ^ data[3]) == 0x38031C16720D1019)
s.add((data[2] ^ data[3]) == 0x31181C080C081A04)

if s.check() == sat:
    res = s.model()
    for i in range(len(res)):
        print(p64(int(str(res[data[i]]))).decode(), end='')

 

 

깔끔하게 잘 나온다.

 

그런데 여기서 끝내도 되지만 이 문제는 자세히 보면 첫번째 데이터랑 xor하는 값이 공개되어 있으므로 역으로 비교하는 값에 xor을 해가면서 역산을 짤수도 있다. 첫번째 값을 구할 수 있고 그 값을 기반으로 두번째, 세번째 연속해서 역산할 수 있다.

 

from pwn import *

data = [0 for i in range(4)]
enc = [0x5487A31B3A9D5EFD, 0x1C0B170809246203, 0x151017167721681E, 0x24080B1E7B29721A]

firstkey = 0x0DD8E7527EE669B1
data[0] = enc[0]^firstkey

for i in range(1, 4):
    data[i] = enc[i]^data[0]

for i in data:
    print(p64(i).decode(), end='')

 

이렇게 역산해도

 

 

플래그 잘 나온다.