# Insomnihack Teaser 2018 - Rule86

by chq-matteo
January 24, 2018

## Why

There are already couple writeups available, so I just want to show a different approach to this challenge. I will not discuss the first part of this challenge since it has been explained before.

The writeup is kind of long, but it doesnâ€™t take much time or effort to use these ideas during a competition.

After we have obtained the decrypted python script and gif, we have to obtain the seed of the PRNG.

The algorithm is quite simple.

RULE = [86 >> i & 1 for i in range(8)]
N_BYTES = 32
N = 8 * N_BYTES

def next(x):
x = (x & 1) << N+1 | x << 1 | x >> N-1
y = 0
for i in range(N):
y |= RULE[(x >> i) & 7] << i
return y

# Bootstrap the PNRG
keystream = int.from_bytes(args.key.encode(),'little')
for i in range(N//2):
print(i)
keystream = next(keystream)

At the time of writing, every writeup focuses on reversing the next function. However there is a trick that can be used to find preimages for similar simple algorithms which does not require to a lot of understanding of the algorithm to reverse.

The idea is that we can use a SAT or SMT solver to find the preimage of a function. We will use Z3.

So we rewrite each function to take an expression and output an expression.

## Rewriting the functions

For function next we take an array of booleans (z3.Bool) which represent the bits of the seed with the least significant bit in x[0] and the most significant bit in x[-1]

def next(x):
# we translate the bit operations
x = [x[-1]] + x + [x[0]]
# we convert RULE to a function that takes 3 bits
return [RULE(x[i + 2], x[i + 1], x[i]) for i in range(256)]

For RULE we take the truth table associated with the array and write its associated boolean function in disjunctive normal form.

def RULE(x, y, z):
return Or(
And(Not(x), Not(y), z), # 001 = 1 -> 1
And(Not(x), y, Not(z)), # 010 = 2 -> 1
And(x, Not(y), Not(z)), # 100 = 4 -> 1
And(x, y, Not(z))       # 110 = 6 -> 1
)

Now we just need to obtain the constraits. We create a Solver, an array of 256 Bools to model our 64 32 byte integer and we save the expression for the output of next.

s = Solver()
seed = [Bool('seed[{}]'.format(i)) for i in range(256)]
next_value = next(seed)

We set as a target the first known output value of the PRNG. Since we want to know the preimage of this value, we add constraints for bit to bit equality to next_value. If the constraints are satisfiable we get a model (some concrete values for each of the variables we defined) for these constraints and then convert the bits to an integer

target = 37450399269036614778703305999225837723915454186067915626747458322635448226786
for j in range(256):
bit = ((1 << j) & target) >= 1
if s.check() == sat:
m = s.model()
ans = 0
for j in range(256):
ans |= (1 if m[seed[j]] else 0) << j

We just repeat this process 128 times to get the original seed and print the flag

## Putting it all together

### Final notes

• we actually can reverse multiple applications of the next function just by calling multiple time next
• we actually may want to do this since next is actually not injective (another plus of SAT and SMT solvers is that we can and proved this next(0x73245e28a24b91090a0967c212e2496612c42512e29c0a224945c428b0b39271) == next(0x892814514904a727172102ce41492116429c8a41442f14c922829c50b08490a))
• however notice that if you compute too many iterations at the same time, you kill performance
• if we had used more of the SMT features that z3 offers, we could have almost copy pasted the original code
from z3 import *
from binascii import unhexlify
s = Solver()
seed = [Bool('seed[{}]'.format(i)) for i in range(256)]

def RULE(x, y, z):
return Or(
And(Not(x), Not(y), z), # 001 = 1 -> 1
And(Not(x), y, Not(z)), # 010 = 2 -> 1
And(x, Not(y), Not(z)), # 100 = 4 -> 1
And(x, y, Not(z))       # 110 = 6 -> 1
)

def next(x):
x = [x[-1]] + x + [x[0]]
return [RULE(x[i + 2], x[i + 1], x[i]) for i in range(256)]

target = 37450399269036614778703305999225837723915454186067915626747458322635448226786
next_value = seed

steps = 8

for i in range(steps):
next_value = next(next_value)

for i in range(128 // steps):
# take a snapshots of the solver constraints
s.push()
for j in range(256):
bit = ((1 << j) & target) >= 1
if s.check() == sat:
m = s.model()
ans = 0
for j in range(256):
ans |= (1 if m[seed[j]] else 0) << j
# renew the target
target = ans

if 'INS' in unhexlify('%064x' % ans)[::-1]:
print(repr(unhexlify('%064x' % ans)[::-1]))
# restore the snapshot
s.pop()

### next is not injective (e.g. not invertible)

s = Solver()
seed = [Bool('seed[{}]'.format(i)) for i in range(256)]
seed1 = [Bool('seed1[{}]'.format(i)) for i in range(256)]

nv = next(seed)
nv1 = next(seed1)
# we want same output
for j in range(256):

# we want different input
dis = False
for i in range(256):
dis = Or(dis, seed[i] != seed1[i])