0ctf SATBeginner

0ctf_satbeginner.py

import socket,random, zlib, struct, string
import pycosat
import hashlib, re, itertools
import bitstring

host = '202.112.26.111'
port = 23333
#host = '127.0.0.1'
#port = 6996

def bypassCaptcha(): # yeah, "captcha"
    # from https://fail0verflow.com/blog/2014/plaidctf2014-crypto375-wheeeee.html
    base = sock.recv(12)
    print base
    letters = [' ', '!', '"', '#', '$', '%', '&', '\'', '(', ')',
        '*', '+', ',', '-', '.', '/', '0', '1', '2', '3', '4', '5',
        '6', '7', '8', '9', ':', ';', '<', '=', '>', '?', '@', 'A',
        'B', 'C', 'D', 'E', 'F', 'G', 'H', 'I', 'J', 'K', 'L', 'M',
        'N', 'O', 'P', 'Q', 'R', 'S', 'T', 'U', 'V', 'W', 'X', 'Y',
        'Z', '[', '\\', ']', '^', '_', '`', 'a', 'b', 'c', 'd', 'e',
        'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o', 'p', 'q',
        'r', 's', 't', 'u', 'v', 'w', 'x', 'y', 'z', '{', '|', '}',
        '~']

    for c in itertools.combinations_with_replacement(letters, 8):
        a = "".join(c)
        if hashlib.sha1(base+a).digest().endswith("\xff\xff\xff"):
            print(base+a)
            sock.send(base+a)
            return

def read_until(wat):
    buf = ''
    while not (wat in buf):
        buf += sock.recv(1)
    return buf
    
def read_for_fun(sz): # read exactly sz bytes
    d = ''
    while (sz > 0):
        tmp = sock.recv(sz)
        sz -= len(tmp)
        d += tmp
    return d

def SATSolve():
    #read input
    s = read_until('SAT:\n')
    print(s)
    len_data = struct.unpack('>I', sock.recv(4))
    print(len_data)
    len_data = len_data[0]
    data = read_for_fun(len_data)
    print '[*] Read ', len(data)
    s = read_until('solution:\n')
    # compute the solution
    wat = eval('['+data.decode('zip')+']')
    k = (len(wat) // 3)
    cnf = [[wat[i*3 + j] for j in range(3)] for i in range(k)]
    sol = pycosat.solve(cnf)
    # packing and sending the solution
    ans = [0 for i in range((k // 8) + 1)]
    for i in xrange(k):
        ans[i // 8] |= (sol[i] > 0) << (i % 8)
    ans = ''.join([chr(i) for i in ans])
    tmp = zlib.compress(ans)
    ans = tmp
    len_ans = struct.pack('>I', len(ans))
    sock.sendall(len_ans+ans)
    print('Sent')
    s = read_until('\n') # 'Good job.' :3
    print(s)

# Init connection
sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
sock.connect((host, port))
# Captcha?
bypassCaptcha()
print('Bypassed')
# Solve the problem
for i in range(50):
    SATSolve()
# Read flag
print(read_until('\n'))
print(read_until('\n'))
print(read_until('\n'))