glibc derandomization

compute-internal-state.py

#!/usr/bin/env python

import z3
import sys

# glibc default PRNG
# it is called TYPE_3, and is an additive recursive generator
# its internal state is made of 31 32-bits integers
# r_0 ... r_30
# each call to random will modify the internal state
#   r_j = r_(j-31) + r_(j-3)
#   yield r_j>>1
# as seen above, each call to random yields 31 bits of an internal state integer

def break_rand(draws):
  n_draws = len(draws)

  # these variables form the initial state of the PRNG
  # we try to solve them, to be able to predict future calls
  rs = [z3.BitVec(('r_%d' % i), 32) for i in range(31)]

  s = z3.Solver()

  for i in range(len(draws)):
    j = 31+i
    
    # create a new variable
    rs.append(z3.BitVec(('r_%d' % j), 32))
    
    # generative rule
    s.add(rs[j-31] + rs[j-3] == rs[j])
    # 
    s.add(z3.LShR(rs[j], 1) == z3.BitVecVal(draws[i], 32))

  if s.check() == z3.sat:
    print('Problem is satisfiable')
  else:
    print('Problem is not satisfiable')

  return s, rs

draws = map(lambda x: int(x, 0), sys.argv[1:])
print('[*] will use %d random draws to deduce the initial internal state' % len(draws))


def enumerate_solutions(draws):
  s, rs = break_rand(draws)

  counter = 0
  solution_list = set()

  while s.check() == z3.sat:
    counter += 1
    initial_state = tuple(s.model()[x].as_long() for x in rs[:31])
    solution_list.add(initial_state)

    or_expr = 'z3.Or('
    for i in range(len(initial_state)):
      or_expr += 'rs[%d] != %d,' % (i, initial_state[i])
    or_expr += ')'

    s.add(eval(or_expr))

  print('[*] found a total of %d solutions' % len(solution_list))
  return solution_list

solutions = enumerate_solutions(draws)
for sol in solutions:
  print('%s' % (' '.join('%d' % x for x in sol)))

predict.py

#!/usr/bin/env python

import argparse

class PRNG(object):
  def __init__(self, state):
    assert(len(state) == 31)
    self.state = [s for s in state]

  def next(self):
    val = self.state[-3] + self.state[-31]
    val %= pow(2, 32)
    self.state.append(val)
    self.state.pop(0)
    return (val>>1)

if __name__ == '__main__':
  parser = argparse.ArgumentParser(description='Generate random numbers given initial state of PRNG')
  parser.add_argument('--skip', type=int, help='Number of draws to skip')
  parser.add_argument('--count', type=int, help='Number of draws to predict')
  parser.add_argument('initial_state', type=int, nargs='+', help='')

  args = parser.parse_args()

  assert(type(args.initial_state) == type([]))
  prng = PRNG(args.initial_state)
  for x in range(args.skip):
    prng.next()
  for x in range(args.count):
    print('%d' % prng.next())