randomizer-2-solve.py

from pwn import *
from z3 import *
context.log_level = 'error'

def checkGuess(sample, predictions):
  for i, val in enumerate(sample):
    if (val != predictions[i]):
      return False
  return True

def nextRand(x, w, s, total_guess):
  guess_numbers = []
  for i in range(total_guess):
    w = (w + s) % (2**64)
    x = (x*x + w) % (2**64)
    x = ((x>>32) | (x<<32)) % (2**64)
    guess_numbers.append((x % (1<<32)))
  return guess_numbers

def guess_x_and_w(sample, s):
  o0 = sample[0]
  o1 = sample[1]
  o2 = sample[2]
  o3 = sample[3]
  sh = (s >> 32) % 2**32
  sl = s % 2**32
  # Brute-force carrier
  for e00 in range(2):
    for e01 in range(2):
      for e10 in range(2):
        for e11 in range(2):
          for e20 in range(2):
            for e21 in range(2):
              # First Equation
              a = BitVec('a', 32)
              b = BitVec('b', 32)
              c = BitVec('c', 32)
              d = BitVec('d', 32)
              sol = Solver()
              sol.add(b == o0)

              # Second Equation
              h00 = 2*o0
              h01 = pow(o0, 2, 2**32)
              h02 = ((o0**2) >> 32)
              c0 = c + sh + e01
              d0 = d + sl
              a0 = h01 + d0
              b0 = o1
              sol.add((h00*a + h02 + c0 + e00) % (2**32) == b0)

              # Third Equation
              h10 = 2*o1
              h11 = pow(o1, 2, 2**32)
              h12 = ((o1**2) >> 32)
              c1 = c0 + sh + e11
              d1 = d0 + sl
              a1 = h11 + d1
              b1 = o2
              sol.add((h10*a0 + h12 + c1 + e10) % (2**32) == b1)

              # Fourth Equation
              h20 = 2*o2
              h21 = pow(o2, 2, 2**32)
              h22 = ((o2**2) >> 32)
              c2 = c1 + sh + e21
              d2 = d1 + sl
              a2 = h21 + d2
              b1 = o2
              sol.add((h20*a1 + h22 + c2 + e20) % (2**32) == o3)

              sol.check()
              if(str(sol.check()) != 'unsat'):
                model = sol.model()

                # check if a, b, c, and d value is valid
                guess_a = model[a].as_long()
                guess_b = model[b].as_long()
                guess_c = model[c].as_long()
                guess_d = model[d].as_long()
                x = guess_a << 32 | guess_b
                w = guess_c << 32 | guess_d
                predictions = nextRand(x, w, s, 2)

                # using the sample to test our prediction
                if(checkGuess(sample[1:-1], predictions)):
                  return nextRand(x, w, s, 13)[3:]
  return None

if __name__ == "__main__":
  s = 0xb5ad4eceda1ce2a9
  r = remote('shell.2019.nactf.com', 31382)
  sample = []
  # Get 4 random sample
  for i in range(4):
    r.recvuntil('> ')
    r.sendline('r')
    sample.append(int(r.recvuntil('\n').strip()))
  print "[+] Sample:", sample

  # Get prediction
  predictions = guess_x_and_w(sample, s)
  print "[+] Predictions:", predictions

  # Start guessing
  r.recvuntil('> ')
  r.sendline('g')
  for num in predictions:
    r.recvuntil("Enter Guess")
    r.recvuntil('> ')
    r.sendline(str(num))

  # Print Flag
  r.recvuntil('\n')
  r.recvuntil('\n')
  print r.recvuntil('\n')
  flag = r.recvuntil('\n').strip()
  print "[+] Flag:", flag