## zerolfsr-
The challenge presents us with the following Python script:
```pythonimport randomimport signalimport socketserverimport stringfrom hashlib import sha256from os import urandomfrom secret import flag
def _prod(L):    p = 1    for x in L:        p *= x    return p
def _sum(L):    s = 0    for x in L:        s ^= x    return s
def n2l(x, l):    return list(map(int, '{{0:0{}b}}'.format(l).format(x)))
class Generator1:    def __init__(self, key: list):        assert len(key) == 64        self.NFSR = key[: 48]        self.LFSR = key[48: ]        self.TAP = [0, 1, 12, 15]        self.TAP2 = [[2], [5], [9], [15], [22], [26], [39], [26, 30], [5, 9], [15, 22, 26], [15, 22, 39], [9, 22, 26, 39]]        self.h_IN = [2, 4, 7, 15, 27]        self.h_OUT = [[1], [3], [0, 3], [0, 1, 2], [0, 2, 3], [0, 2, 4], [0, 1, 2, 4]]
    def g(self):        x = self.NFSR        return _sum(_prod(x[i] for i in j) for j in self.TAP2)
    def h(self):        x = [self.LFSR[i] for i in self.h_IN[:-1]] + [self.NFSR[self.h_IN[-1]]]        return _sum(_prod(x[i] for i in j) for j in self.h_OUT)
    def f(self):        return _sum([self.NFSR[0], self.h()])
    def clock(self):        o = self.f()        self.NFSR = self.NFSR[1: ] + [self.LFSR[0] ^ self.g()]        self.LFSR = self.LFSR[1: ] + [_sum(self.LFSR[i] for i in self.TAP)]        return o
class Generator2:    def __init__(self, key):        assert len(key) == 64        self.NFSR = key[: 16]        self.LFSR = key[16: ]        self.TAP = [0, 35]        self.f_IN = [0, 10, 20, 30, 40, 47]        self.f_OUT = [[0, 1, 2, 3], [0, 1, 2, 4, 5], [0, 1, 2, 5], [0, 1, 2], [0, 1, 3, 4, 5], [0, 1, 3, 5], [0, 1, 3], [0, 1, 4], [0, 1, 5], [0, 2, 3, 4, 5], [            0, 2, 3], [0, 3, 5], [1, 2, 3, 4, 5], [1, 2, 3, 4], [1, 2, 3, 5], [1, 2], [1, 3, 5], [1, 3], [1, 4], [1], [2, 4, 5], [2, 4], [2], [3, 4], [4, 5], [4], [5]]        self.TAP2 = [[0, 3, 7], [1, 11, 13, 15], [2, 9]]        self.h_IN = [0, 2, 4, 6, 8, 13, 14]        self.h_OUT = [[0, 1, 2, 3, 4, 5], [0, 1, 2, 4, 6], [1, 3, 4]]
    def f(self):        x = [self.LFSR[i] for i in self.f_IN]        return _sum(_prod(x[i] for i in j) for j in self.f_OUT)     def h(self):        x = [self.NFSR[i] for i in self.h_IN]        return _sum(_prod(x[i] for i in j) for j in self.h_OUT)        
    def g(self):        x = self.NFSR        return _sum(_prod(x[i] for i in j) for j in self.TAP2)  
    def clock(self):        self.LFSR = self.LFSR[1: ] + [_sum(self.LFSR[i] for i in self.TAP)]        self.NFSR = self.NFSR[1: ] + [self.LFSR[1] ^ self.g()]        return self.f() ^ self.h()
class Generator3:    def __init__(self, key: list):        assert len(key) == 64        self.LFSR = key        self.TAP = [0, 55]        self.f_IN = [0, 8, 16, 24, 32, 40, 63]        self.f_OUT = [[1], [6], [0, 1, 2, 3, 4, 5], [0, 1, 2, 4, 6]]
    def f(self):        x = [self.LFSR[i] for i in self.f_IN]        return _sum(_prod(x[i] for i in j) for j in self.f_OUT)
    def clock(self):        self.LFSR = self.LFSR[1: ] + [_sum(self.LFSR[i] for i in self.TAP)]        return self.f()
class zer0lfsr:    def __init__(self, msk: int, t: int):        if t == 1:            self.g = Generator1(n2l(msk, 64))        elif t == 2:            self.g = Generator2(n2l(msk, 64))        else:            self.g = Generator3(n2l(msk, 64))        self.t = t
    def next(self):        for i in range(self.t):            o = self.g.clock()        return o
class Task(socketserver.BaseRequestHandler):    def __init__(self, *args, **kargs):        super().__init__(*args, **kargs)
    def proof_of_work(self):        random.seed(urandom(8))        proof = ''.join([random.choice(string.ascii_letters + string.digits + '!#$%&*-?') for _ in range(20)])        digest = sha256(proof.encode()).hexdigest()        self.dosend('sha256(XXXX + {}) == {}'.format(proof[4: ], digest))        self.dosend('Give me XXXX:')        x = self.request.recv(10)        x = (x.strip()).decode('utf-8')         if len(x) != 4 or sha256((x + proof[4: ]).encode()).hexdigest() != digest:             return False        return True
    def dosend(self, msg):        try:            self.request.sendall(msg.encode('latin-1') + b'\n')        except:            pass
    def timeout_handler(self, signum, frame):        raise TimeoutError
    def handle(self):        try:            signal.signal(signal.SIGALRM, self.timeout_handler)            signal.alarm(30)            if not self.proof_of_work():                self.dosend('You must pass the PoW!')                return            signal.alarm(50)            available = [1, 2, 3]            for _ in range(2):                self.dosend('which one: ')                idx = int(self.request.recv(10).strip())                assert idx in available                available.remove(idx)                msk = random.getrandbits(64)                lfsr = zer0lfsr(msk, idx)                for i in range(5):                    keystream = ''                    for j in range(1000):                        b = 0                        for k in range(8):                            b = (b << 1) + lfsr.next()                        keystream += chr(b)                    self.dosend('start:::' + keystream + ':::end')                hint = sha256(str(msk).encode()).hexdigest()                self.dosend('hint: ' + hint)                self.dosend('k: ')                guess = int(self.request.recv(100).strip())                if guess != msk:                    self.dosend('Wrong ;(')                    self.request.close()                else:                    self.dosend('Good :)')            self.dosend(flag)        except TimeoutError:            self.dosend('Timeout!')            self.request.close()        except:            self.dosend('Wtf?')            self.request.close()
class ThreadedServer(socketserver.ForkingMixIn, socketserver.TCPServer):    pass
if __name__ == "__main__":    HOST, PORT = '0.0.0.0', 31337    server = ThreadedServer((HOST, PORT), Task)    server.allow_reuse_address = True    server.serve_forever()
```### Challenge
The server first asks for a proof of work. Then you need to specify an index between 1 and 3. This index determines the Generator that will be used as your LFSR. The server will then send you 5 times 1000 bytes of the LFSR (so 40000 LFSR output bits). It will also return a hash of the key you need to guess as a hint. If you guess the key correctly, you have to choose another index that you did not yet use. The whole thing repeats and if you got both keys correct, you are given the flag.
### Solution Script
We solve the challenge using the Z3 SMT solver. First, the script solves the proof of work challenge using brute-force. It then converts the character encoded bytes into a list of bits. We use only a small amount of the 40k bits (200 seemed to be enough) as constraints for Z3. Using all of the bits would take too much time to solve. I chose Generator3 and Generator1 as targets, because they worked reasonably fast with Z3. I had to modify the function ```n2l(x, l)``` from the task script since the format string did not work with the BitVec from Z3. ```n2l(x, l)``` converts an integer into a bit list.
```pythonfrom pwn import *from hashlib import sha256from itertools import productimport reimport z3import bitarrayimport random
# this was modified to be able to use z3def n2l(x, l):    if isinstance(x, int):        return list(map(int, '{{0:0{}b}}'.format(l).format(x)))    return [z3.Extract(i, i, x) for i in reversed(range(l))]
host = args.HOST or '111.186.59.28'port = int(args.PORT or 31337)
def start():    return connect(host, port)
def solve_proof_of_work(proof_of_work_line) :    hashable_suffix = re.search('sha256\(XXXX \+ (.*)\) ==', proof_of_work_line).group(1)    hash = re.search('== (.*)', proof_of_work_line).group(1)    alphabet = (string.ascii_letters + string.digits + '!#$%&*-?')    for hashable_prefix in product(alphabet, repeat=4) :        current_hash_in_hex = sha256((''.join(hashable_prefix) + hashable_suffix).encode()).hexdigest()        if current_hash_in_hex == hash :            return ''.join(hashable_prefix)
def bytes_to_bit_list(bytes) :    ba = bitarray.bitarray()    ba.frombytes(bytes)    return ba.tolist()
def test_if_keystreams_matches_output_bits(keystreams, output_bits) :    keystreams_test = []    test_index = 0    for i in range(5):        tmp_keystream = b""        for j in range(1000):            b = 0            for k in range(8):                b = (b << 1) + lfsr_output_bits[test_index]                test_index += 1            tmp_keystream += b.to_bytes(1, 'big')        keystreams_test.append(tmp_keystream)    return keystreams_test == keystreams_test
def solve_with_z3(lfsr_output_bits, generator_index, prefix_bits_to_check) :    msk = z3.BitVec('msk', 64)    lfsr = zer0lfsr(msk, generator_index)
    solver = z3.Solver()
    for i in range(prefix_bits_to_check):        solver.add(lfsr_output_bits[i] == lfsr.next())  log.info("solver.check(): %s", solver.check())
    model = solver.model()
 log.info("model: %s", model)
    return model.evaluate(msk).as_long()
io = start()
proof_of_work_line = io.recvline(keepends=False).decode("utf-8")io.recvline()
proof = solve_proof_of_work(proof_of_work_line)io.sendline(proof)
prefix_bits_to_check = 200generator_indices = [3, 1]for generator_index in generator_indices :    io.recvline() # which one:    io.sendline(str(generator_index)) # choose Generator[generator_index]
    keystreams = []    for i in range(5) :        start = io.recvn(8)        keystream = io.recvn(1000)        end = io.recvn(7) #including the next line byte         keystreams.append(keystream)      hint_line = io.recvline(keepends=False).decode("utf-8")    hint = re.search('hint: (.*)', hint_line).group(1)
    io.recvline() #k:
    lfsr_output_bits = []    for i in range(5) :        lfsr_output_bits += bytes_to_bit_list(keystreams[i])
    assert test_if_keystreams_matches_output_bits(keystreams, lfsr_output_bits)
    solved_msk = solve_with_z3(lfsr_output_bits, generator_index, prefix_bits_to_check) log.info("solved_msk: %s", solved_msk)
    hint_compare = sha256(str(solved_msk).encode()).hexdigest() log.info("hint_compare: %s", hint_compare) log.info("hint: %s", hint)
    io.sendline(str(solved_msk))
    maybe_good = io.recvline(keepends=False) # Good :) log.info("maybe_good: %s", maybe_good) flag = io.recvline(keepends=False)log.info("flag: %s", flag)io.shutdown()```