chaussette_xs_miasm.py

from z3 import *
from pwn import *
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB
from miasm.analysis.binary import Container
from miasm.jitter.csts import *
from miasm.expression.expression import *
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.ir.translators.z3_ir import TranslatorZ3
from miasm.arch.x86.lifter_model_call import LifterModelCall_x86_64
from miasm.core.bin_stream import bin_stream_str

def slv(data):
    loc_db = LocationDB()
    bs = bin_stream_str(data)
    machine = Machine("x86_64")
    ira = machine.lifter(loc_db)
    dis_engine = machine.dis_engine(bs, loc_db=loc_db)
    asm_cfg = dis_engine.dis_multiblock(0x0)
    ira_cfg = ira.new_ircfg_from_asmcfg(asm_cfg)

    init_state = {}

    sb = SymbolicExecutionEngine(LifterModelCall_x86_64(loc_db) , state=init_state)
    sb.run_block_at(ira_cfg, addr=0x0, step=False)
    trans = TranslatorZ3(loc_db=loc_db)

    rax = trans.from_expr(sb.symbols[ira.arch.regs.RAX])
    s = Solver()
    s.add(rax == 0)
    print(s.check())
    m = s.model()
    print(m)

    out = {}
    for x in m:
        out[x.name()] = m[x].as_long()
    return out



n1 = 14171339039947875846
n2 = 12

io = remote("challenges.france-cybersecurity-challenge.fr", 2253)
r = 0
while True:
    print("sending: %d %d"%(n1, n2))
    #input()
    io.send(p64(n1))
    io.send(p64(n2))
    size = u64(io.recv(8))
    print("receving: %x"%size)
    if size == 0xffffffffffffffff:
        print(io.recv(4096))
        break
    code = b''
    while len(code) < size:
        code += io.recv(size - len(code))
    print(hex(len(code)))
    
    #open('out/%d.bin'%r, 'wb').write(code)
    r += 1

    out = slv(code)
    if 'RDI' in out:
        n1 = out['RDI']
    if 'RSI' in out:
        n2 = out['RSI']