A simple Z3 challenge.
使用Z3即可。

Code for solver：
解题代码：
```
#/usr/local/bin/python3

from pwn import *
import re
from hashlib import sha256
import itertools
import string

'''
b'sha256(XXXX + u*Sbb#fDFH!Ch7$G) == 8899ba88a4c96f02d0bb75d567e0c37ac594788f6284fcfa814c746a6bc2d370\nGive me XXXX:\n'
'''

r = remote('111.186.59.28', 31337)
pow_line = r.recvuntil('Give me XXXX:\n')

# pow_line = b'sha256(XXXX + u*Sbb#fDFH!Ch7$G) == 8899ba88a4c96f02d0bb75d567e0c37ac594788f6284fcfa814c746a6bc2d370\nGive me XXXX:\n'
m = re.search(b'^sha256\(XXXX \+ (.*)\) == ([0-9a-f]*)\nGive me', pow_line)
print(m.group(1))
print(m.group(2))

'''
ords = list(map(ord, string.printable[:-6]))
h = m.group(2).decode()

index = 0
for item in itertools.product(ords, repeat=4):
s = bytes(item) + m.group(1)
if sha256(s).hexdigest() == h:
print('found!')
print(item)
exit()
index += 1
if index % 100000 == 0:
print(index)
'''

p = process(argv=['./calc', m.group(1), m.group(2).upper()])
pow_answer = p.recv(1000)
print(pow_answer)
pow_answer = bytes(list(map(int, pow_answer.strip().split(b' '))))
print(pow_answer)
r.send(pow_answer + b'\n')

# 'start:::' + keystream + ':::end'
'''
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 :)')
'''
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_IN = [24, 63]
self.f_OUT = [[1], [6], [0, 1, 2, 3, 4, 5], [0, 1, 2, 4, 6]]
#self.f_OUT = [[0, 1], [0]]

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

idx = [b'3', b'1']
import z3

for i in range(2):
print(r.recvuntil('which one: \n'))
r.send(idx[i] + b'\n')
keystreams = []
for j in range(5):
keystream = r.recvuntil(':::end\n')
keystreams.append(keystream.strip()[len('start:::'):-len(':::end')])
print('Got keystream ', i, j)
print(r.recvuntil('k: \n'))
x = z3.BitVec('x', 64)
solver = z3.Solver()
state = []
for j in range(64):
state.append(z3.LShR(x, j) & 1)
state = state[::-1]
if i == 0:
g = Generator3(state)
else:
g = Generator1(state)
for keystream in keystreams[:1]:
length = 16
print(keystream[:length])
bits = n2l(int.from_bytes(keystream[:length], 'big'), length*8)
for bit in bits:
o = 0
for _ in range(int(idx[i])):
o = g.clock()
solver.add(o == bit)
solver.check()
print('solve: ', solver.model()[x])
r.send(str(solver.model()[x]).encode() + b'\n')
print(r.recv(1024))

print(r.recv(1024))
```

Code for POW
POW代码（C）：
```
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <openssl/sha.h>

unsigned char convert(char* hex) {
unsigned char result = 0;
int offset = 1;
for (int i = 0; i < 2; ++i) {
char ch = hex[1 - i];
if (ch >= '0' && ch <= '9') {
result += offset * (ch - '0');
} else {
result += offset * (10 + ch - 'A');
}
offset *= 16;
}
return result;
}

int main(int argc, char** argv) {

char message[30] = {0};
char target[65] = {0}; // = argv[1];
//printf("%s %s", argv[0], argv[1]);
strncpy(&message[4], argv[1], strlen(argv[1]));
strncpy(target, argv[2], strlen(argv[2]));
//printf("%d\n", strlen(target));
unsigned char target_ch[33] = {0};

for(int i = 0; i < 32; ++i) {
target_ch[i] = convert(&target[2*i]);
}
//for(int i = 0; i < 32; ++i) {
// printf("%d ", target_ch[i]);
//}
//printf("\n");

char ords[94] = {48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 58, 59, 60, 61, 62, 63, 64, 91, 92, 93, 94, 95, 96, 123, 124, 125, 126};

/*
>>> ord('r')
114
>>> ord('4')
52
>>> ord(')')
41
>>> ord('!')
33
>>> exit()
*/

for (int i = 0; i < 94; ++i) {
for (int j = 0; j < 94; ++j) {
for (int m = 0; m < 94; ++m) {
for (int n = 0; n < 94; ++n) {
message[0] = ords[i];
message[1] = ords[j];
message[2] = ords[m];
message[3] = ords[n];
unsigned char digest[33] = {0};
SHA256((const unsigned char *)message, strlen(message), digest);
int flag = 1;
for (int k = 0; k < 32; ++k) {
if (digest[k] != target_ch[k]) {
flag = 0;
break;
}
}
//if (ords[i] == 114 && ords[j] == 52 && ords[m] == 41 && ords[n] == 33) {
// printf("AAA\n");
// for (int k = 0; k < 32 ; ++k) {
// printf("%d ", digest[k]);
// }
// printf("\n");
//}
if (flag) {
printf("%d %d %d %d\n", ords[i], ords[j], ords[m], ords[n]);
exit(0);
}
}
}
}
}
return 0;
}

```