ZetaTwo

Advent OverTheWire 2019 - Level 8

Dec 26th, 2019
89
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #!/usr/bin/solve
  2.  
  3. from z3 import *
  4. from pwn import *
  5.  
  6. HOST = '3.93.128.89'
  7. PORT = 1218
  8.  
  9. def attempt(values):
  10.  
  11.     #r = process('./chal')
  12.     r = remote(HOST, PORT)
  13.  
  14.     solution_idx = [
  15.         [3, 6, 7, 5, 8, 4, 1, 2, 9],
  16.         [2, 4, 1, 7, 3, 9, 5, 6, 8],
  17.         [9, 8, 5, 2, 6, 1, 4, 3, 7],
  18.         [6, 5, 2, 3, 9, 7, 8, 4, 1],
  19.         [7, 1, 3, 8, 4, 2, 6, 9, 5],
  20.         [4, 9, 8, 6, 1, 5, 2, 7, 3],
  21.         [1, 7, 9, 4, 2, 8, 3, 5, 6],
  22.         [8, 2, 6, 9, 5, 3, 7, 1, 4],
  23.         [5, 3, 4, 1, 7, 6, 9, 8, 2],
  24.     ]
  25.  
  26.     #pause()
  27.  
  28.     for row in range(9):
  29.         r.sendline(' '.join(str(values[idx-1]) for idx in solution_idx[row]).encode('ascii'))
  30.  
  31.     response = r.recvall()
  32.     r.close()
  33.     if b'AOTW{' in response:
  34.         print(response)
  35.         return True
  36.     return False
  37.  
  38.  
  39. NUM_CELLS = 9
  40. cells = [BitVec('c_%d' % i, 32) for i in range(9)]
  41.  
  42. ADDR_WIN = 0x08048799
  43. ADDR_PUTS = 0x0804A010
  44. ADDR_SCORER = 0x0804A1C0
  45. OFFSET_PUTS = (ADDR_PUTS - ADDR_SCORER) // 4
  46.  
  47. print(ADDR_WIN)
  48. print(OFFSET_PUTS+2**32)
  49. #print((ADDR_PUTS - ADDR_SCORER))
  50.  
  51. s = Solver()
  52.  
  53. #for c in cells:
  54. #    s.add(c >= 0)
  55.  
  56. s.add(sum(cells) == 45)
  57. s.add(Product(cells) == 362880)
  58.  
  59. #s.add(cells[])
  60.  
  61. """
  62. s.add(And(
  63.    Or(*[x == BitVecVal(ADDR_WIN, 32) for x in cells]),
  64.    Or(*[x == BitVecVal(OFFSET_PUTS+2**32, 32) for x in cells]),
  65.    Or(*[x <= BitVecVal(9, 32) for x in cells])
  66. ))
  67. """
  68.  
  69. #s.add(cells[0]//4 <= 9)
  70. s.add(cells[0] == OFFSET_PUTS+2**32)
  71. s.add(cells[1] == ADDR_WIN)
  72. s.add(cells[2] == 1)
  73. s.add(cells[3] == 2)
  74. s.add(cells[4] == 3)
  75.  
  76. print(s)
  77.  
  78. #for i in range(1, len(cells)):
  79. #    s.add(cells[i-1] <= cells[i])
  80.  
  81. while s.check() == sat:
  82.     m = s.model()
  83.     row = [m[c].as_long() for c in cells]
  84.     print(row)
  85.     s.add(Not(And(*[x==y for x,y in zip(row, cells)])))
  86.  
  87.     if attempt(row):
  88.         print(row)
  89.         break
  90.  
  91. """
  92. python3 solve_z3.py
  93. 134514585
  94. 4294967188
  95. [0 + c_0 + c_1 + c_2 + c_3 + c_4 + c_5 + c_6 + c_7 + c_8 ==
  96. 45,
  97. 1*c_0*c_1*c_2*c_3*c_4*c_5*c_6*c_7*c_8 == 362880,
  98. c_0 == 4294967188,
  99. c_1 == 134514585,
  100. c_2 == 1,
  101. c_3 == 2,
  102. c_4 == 3]
  103. [4294967188, 134514585, 1, 2, 3, 3911297825, 108947494, 113742248, 26465291]
  104. [+] Opening connection to 3.93.128.89 on port 1218: Done
  105. [+] Receiving all data: Done (162B)
  106. [*] Closed connection to 3.93.128.89 port 1218
  107. b'Could you give me a fully solved sudoku?\nEnter 9 lines, each containing 9 integers, space separated:\nLet me take a look...\nAOTW{Th3t_is_such_aN_1mpr3ssive_Sud0ku}'
  108. [4294967188, 134514585, 1, 2, 3, 3911297825, 108947494, 113742248, 26465291]
RAW Paste Data