This challenge asked us to recover the initial state of three linear-feedback shift registers (each of size 48), given the output of a nonlinear combine() function applied to the three individual output streams:

def combine(x1,x2,x3):
    return (x1*x2)^(x2*x3)^(x1*x3)

The given challenge source code consists of a fairly typical lfsr class, along with some code that writes the generated stream to a file:

from secret import init1,init2,init3,FLAG
import hashlib
assert(FLAG=="flag{"+hashlib.sha256(init1+init2+init3).hexdigest()+"}")

class lfsr():
    def __init__(self, init, mask, length):
        self.init = init
        self.mask = mask
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask 
        i = self.init & self.mask & self.lengthmask 
        output = 0
        while i != 0:
            output ^= (i & 1)
            i = i >> 1
        nextdata ^= output
        self.init = nextdata
        return output

def combine(x1,x2,x3):
    return (x1*x2)^(x2*x3)^(x1*x3)

if __name__=="__main__":
    l1 = lfsr(int.from_bytes(init1,"big"),0b100000000000000000000000010000000000000000000000,48)
    l2 = lfsr(int.from_bytes(init2,"big"),0b100000000000000000000000000000000010000000000000,48)
    l3 = lfsr(int.from_bytes(init3,"big"),0b100000100000000000000000000000000000000000000000,48)

    with open("keystream","wb") as f:
        for i in range(8192):
            b = 0
            for j in range(8):
                b = (b<<1)+combine(l1.next(),l2.next(),l3.next())
            f.write(chr(b).encode())

While one could try to understand the structure of these computations and find a mathematical way to recover the secret initial states, we went for a less sophisticated approach: Observing that growing prefixes of the output bits depend on more and more bits of init1 through init3 (and short prefixes depend on very few secret bits), we suspected that setting up the whole problem as a system of equations and simply throwing a generic SMT solver at it would probably work.

There is one little caveat that we stumbled over: The keystream file does not contain the actual output bytes, but the UTF8-encoded version of the output bytes interpreted as Unicode codepoints. That is, if the output value was 0xcc, then what the script above writes to the keystream file are the bytes c3 8c.

After fixing this small slip-up, we ended up with the following script using z3’s awesome Python bindings:

#!/usr/bin/env python3
import z3, hashlib

class lfsr():
    def __init__(self, init, mask, length):
        self.init = init
        self.mask = mask
        self.lengthmask = 2**(length+1)-1

    def next(self):
        nextdata = (self.init << 1) & self.lengthmask
        i = self.init & self.mask & self.lengthmask
        output = 0
        for j in range(self.lengthmask.bit_length() + 42):
            output ^= z3.LShR(i,j) & 1
        self.init = nextdata ^ output
        return output

def combine(x1,x2,x3):
    return (x1*x2)^(x2*x3)^(x1*x3)

keystream = [ord(x) for x in open('keystream','r').read()]

inits = [z3.BitVec('init{}'.format(i), 48) for i in (1,2,3)]

l1 = lfsr(inits[0],0b100000000000000000000000010000000000000000000000,48)
l2 = lfsr(inits[1],0b100000000000000000000000000000000010000000000000,48)
l3 = lfsr(inits[2],0b100000100000000000000000000000000000000000000000,48)

solver = z3.Solver()
for i,b in enumerate(keystream[:23]):
    for j in reversed(range(8)):
        solver.add(((b >> j) & 1) == combine(l1.next(),l2.next(),l3.next()))

print(solver.check())
m = solver.model()
print(m)

inits = [m[i].as_long() for i in inits]
sol = b''.join(i.to_bytes(6,'big') for i in inits)
flag = 'flag{' + hashlib.sha256(sol).hexdigest() + '}'
print('-->', flag)

It takes less than 10 seconds to recover the flag:

$ ./pwn.py
sat
[init3 = 191532558614761,
 init2 = 181037482648735,
 init1 = 70989122156399]
--> flag{b527e2621131134ec22250cfbca75e8c9f5ae4f40370871fd55910927f66a1b4}
$