ZetaTwo

Advent OverTheWire 2019 - Level 8

Dec 26th, 2019
122
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

Adblocker detected! Please consider disabling it...

We've detected AdBlock Plus or some other adblocking software preventing Pastebin.com from fully loading.

We don't have any obnoxious sound, or popup ads, we actively block these annoying types of ads!

Please add Pastebin.com to your ad blocker whitelist or disable your adblocking software.

×