A simple Z3 challenge. 使用Z3即可。
Code for solver：解题代码：```#/usr/local/bin/python3
from pwn import *import refrom hashlib import sha256import itertoolsimport 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 = 0for 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 POWPOW代码（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;  }  
```