Kaspersky Industrial CTF Quals 2017 - RE700 BlaBlaMan

BlaBlaMan.py

# -*- coding: utf-8 -*-
from pwn import *
from z3 import *

context(arch = 'i386', os = 'linux')
# context(arch = 'amd64', os = 'linux')
context.log_level = 'debug'

v1 = 1240041760064458136
v2 = 2569194187569403613
v3 = 622703256829790890
v4 = 18101253111159542915

p = remote('195.133.196.43', 27777)

p.recvuntil(': ')
s = p.recvline().strip()

payload = ''
for i in xrange(0, 64, 16):
    input_num = BitVec("input_num", 64)
    target = int(s[i:i+16], 16)
    solver = Solver()
    solver.add(target == input_num * (v1 + input_num * (v2 * input_num - v3)) - v4)
    print(solver.check())
    m = solver.model()
    res = m[input_num].as_long()
    payload += '{0:016X}'.format(res & 0xffffffffffffffff)
    print payload

p.sendline(payload)
p.interactive()

'''
[ubuntu@vu]# python BlaBlaMan.py                                             [/home/ubuntu/sd/-work]
[+] Opening connection to 195.133.196.43 on port 27777: Done
[DEBUG] Received 0x4f bytes:
    'Talk to me: 88542ABD9C3BD9B61F9E63EAA21D1BAA2CBA6A6CC5BC1A06EB7C2DA710ABD48E\r'
    '\r\n'
sat
384335782218EA87
sat
384335782218EA87F87201096381CD33
sat
384335782218EA87F87201096381CD33247218EE62D7CBF7
sat
384335782218EA87F87201096381CD33247218EE62D7CBF7A54BC3B9115BFB0F
[DEBUG] Sent 0x41 bytes:
    '384335782218EA87F87201096381CD33247218EE62D7CBF7A54BC3B9115BFB0F\n'
[*] Switching to interactive mode
[DEBUG] Received 0x2e bytes:
    'Flag: KLCTF38529ECCA6F8863442331C40E1BD5F9C\r'
    '\r\n'
Flag: KLCTF38529ECCA6F8863442331C40E1BD5F9C
[*] Got EOF while reading in interactive
$
[*] Closed connection to 195.133.196.43 port 27777
'''