rao_bash nsec2k17

rao_bash.py

from z3 import *

init(PATH_TO_Z3)

# >rao_bash.py
# 4sM1s:1f3_Fl4gzZ
# 4sM1s 1f3_Fl4gzZ
# 4sM1s 1f3(Fl4gzZ
# 4sM1s:1f3(Fl4gzZ
# 4sM1s@1f3_Fl4gzZ
# 4sM1sL1f3_Fl4gzZ
# 4sM1sL1f3(Fl4gzZ
# 4sM1s@1f3(Fl4gzZ
# 4sM1s`1f3_Fl4gzZ
# 4sM1s`1f3(Fl4gzZ
# 4sM1sr1f3_Fl4gzZ
# 4sM1sr1f3(Fl4gzZ

def display_model(m):
    block = {}
    #print m
    for x in m:
        if str(x)[0] == "p":
            block[int(str(x)[1:])] = int(str(m[x]))
    password = "".join(map(chr, block.values()))
    print password

def is_printable(x):
    return And(x >= 0x20, x <= 0x7E)

def lzcnt(expr):
    # 63 - "bsr"
    size = expr.size()
    res = BitVec('res', 8)
    for i in xrange(size - 1, 0, -1):
        index = - i % size
        res = z3.If((expr & (1 << index)) != 0, index, res)
    return 63 - res

def compute_it(cur_char):
    # .rodata:00000000004D3B08 F3 48 0F BD DA                          lzcnt   rbx, rdx
    leading_zero = lzcnt(cur_char)
    # .rodata:00000000004D3B0D F2 0F 2A D3                             cvtsi2sd xmm2, ebx
    xmm_2 = ZeroExt(64 - leading_zero.size(), leading_zero)
    xmm_2 = fpBVToFP(xmm_2, Float64())
    # .rodata:00000000004D3B11 F2 0F 2A C3                             cvtsi2sd xmm0, ebx
    xmm_0 = ZeroExt(64 - leading_zero.size(), leading_zero)
    xmm_0 = fpBVToFP(xmm_0, Float64())
    # .rodata:00000000004D3B15 F2 0F 2A CA                             cvtsi2sd xmm1, edx
    xmm_1 = ZeroExt(64 - cur_char.size(), cur_char)
    xmm_1 = fpBVToFP(xmm_1, Float64())
    # .rodata:00000000004D3B19 F2 0F 5E C1                             divsd   xmm0, xmm1
    xmm_0 = fpToIEEEBV(fpDiv(RNE(), xmm_0, xmm_1))
    # .rodata:00000000004D3B1D 66 0F EF C2                             pxor    xmm0, xmm2
    xmm_0 = xmm_0 ^ fpToUBV(RNE(), xmm_2, BitVecSort(64))
    # .rodata:00000000004D3B21 66 0F 7E C2                             movd    edx, xmm0
    return (xmm_0 & 0xFFFFFFFF)

s = Solver()
table_res = [0x89D89D8A, 0xE54975FC, 0x31DEC0D5, 0x97829CBC, 0xE54975FC, 0x00, 0x97829CBC, 0xE1E1E1E2, 0x32323232, 0x33333333, 0xEA0EA0EA, 0x38E38E39, 0x89D89D8A, 0xD83BA686, 0xD60864B9, 0x44444444]
length = len(table_res)
password = [BitVec("p%d" % i, 8) for i in range(length)]

for i in xrange(0, length):
    s.add(is_printable(password[i]))
    s.add(compute_it(password[i]) == table_res[i])

while s.check() == sat:
    model = s.model()
    display_model(model)
    s.add(Or([sym != model[sym] for sym in password]))