cea-sec / miasm

Reverse engineering framework in Python
https://miasm.re/
GNU General Public License v2.0
3.44k stars 471 forks source link

expression propagation in SymbolicExecutionEngine #1352

Open P1224 opened 3 years ago

P1224 commented 3 years ago

Hi, I'm dealing with some obfuscations with SymbolicExecutionEngine and i'm stuck with the following sample:

mov eax, xxx
and eax, 1
mov [esp + 4], 123
mov [esp], 456
mov edx, [esp + eax * 4]

I want to transfrom it to edx = (xxx & 1) ? 123 : 456, so i wrote a custom simplifier callback to transfrom eax & 1 to (eax & 1) ? 1 : 0 and combined it with built-in simplifier simp_cond_op_int, but only get edx = (xxx & 1) ? [esp + 4] : [esp].

I looked into SymbolicExecutionEngine.eval_expr_visitor, and it seems to work as

simplify expression
eval with symbolic state
simplify expression

original expr:               [esp + eax * 4]
after simplification:        [esp + eax * 4]
after eval:                  [esp + (xxx & 1) * 4]
after second simplification: (xxx & 1) ? [esp + 4] : [esp]

It is obvious that expression propagation is not applied to [esp + 4] and [esp].

How could I fix this behavior?

serpilliere commented 3 years ago

Hi @P1224 When doing memory propagation, Miasm has some hypothesis and constraints. For example: if you have the following sequence of assignments (suppose memory accesses are 1 byte long:

[A] = 1
[A+4] = 2
B = [A]

the [A] = 1 can be propagated through the [A+4] = 2, has [A] and [A+4] won't interfer here. So we will have:

[A] = 1
[A+4] = 2
B = 1

The rule is: we can compare two 'symbolic' memory values based on the same symbolic pointer (Ex [A] and [A+1]. But we cannot determine if 2 symbolic memories based on different symbolic base pointer (Ex: [A] and [B+1]``) This is because we know that[A]and[A+1]won't alias (ok, there may be special cases with dual mapped memory) but[A]and[B+1]` may alias here.

But in your case, I think this should be ok. So I recoded your example. First the source::

main:
    MOV EAX, EDX
    AND EAX, 1
    MOV DWORD PTR [ESI + 4], 0x123
    MOV DWORD PTR [ESI], 0x456
    MOV EDX, DWORD PTR [ESI + EAX * 4]
    MOV EAX, EDX
    RET

Then the test code. It's a merge between miasm/example/disasm/dis_binary_lift_model_call.py and miasm/example/expression/simplification_add.py:

from __future__ import print_function
import sys

from future.utils import viewvalues
from miasm.analysis.binary import Container
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB

from miasm.analysis.simplifier import IRCFGSimplifierCommon, IRCFGSimplifierSSA
from miasm.expression.simplifications import expr_simp
from miasm.expression.expression import *

#####################################
# Common section from dis_binary.py #
#####################################

fdesc = open(sys.argv[1], 'rb')
loc_db = LocationDB()

cont = Container.from_stream(fdesc, loc_db)

machine = Machine(cont.arch)

mdis = machine.dis_engine(cont.bin_stream, loc_db=cont.loc_db)

addr = cont.entry_point
head = loc_db.get_or_create_offset_location(addr)
asmcfg = mdis.dis_multiblock(addr)

#####################################
#    End common section             #
#####################################

# Get an IRA converter
# The sub call are modelised by default operators
# call_func_ret and call_func_stack
lifter = machine.lifter_model_call(mdis.loc_db)

# Get the IR of the asmcfg
ircfg_analysis = lifter.new_ircfg_from_asmcfg(asmcfg)

# Display each IR basic blocks
for irblock in viewvalues(ircfg_analysis.blocks):
    print(irblock)

# Output ir control flow graph in a dot file
open('bin_lifter_model_call_cfg.dot', 'w').write(ircfg_analysis.dot())

# Create joker for match expr
joker1 = ExprId('joker1', 32)
joker2 = ExprId('joker2', 32)
pattern = expr_simp(joker1 + (joker2 & ExprInt(1, 32)) * ExprInt(4, 32))

# Add simplification pass
def simp_lookup(expr_simp, expr):
    """
    Add simplification:
    @32[X + Y & 1] => ExprCond(Y & 1, @32[X+4], @32[X])
    """
    if expr.size != 32:
        return expr
    ptr = expr.ptr
    found = {}
    result = match_expr(ptr, pattern, set([joker1, joker2]), found)
    if not result:
        return expr
    base = found[joker1]
    index = found[joker2]
    print("found pattern in %s with %s %s" % (expr, base, index))
    src1 = expr_simp(ExprMem(base + ExprInt(4, 32), 32))
    src2 = expr_simp(ExprMem(base, 32))
    result = ExprCond(index & ExprInt(1, 32), src1, src2)
    result = expr_simp(result)
    return result

# Enable pass

expr_simp.enable_passes({ExprMem: [simp_lookup]})

simplifier = IRCFGSimplifierSSA(lifter)
ircfg = simplifier.simplify(ircfg_analysis, head)
open('final.dot', 'w').write(ircfg.dot())

And here is the result: final

It seems that the simplification is applied. Are you ok with this? Maybe there is a bug in your implementation of the simplification ?

P1224 commented 3 years ago

Thank you for your reply.

The problem is I am dealing with obfuscated code and IRCFGSimplifierSSA should not be used here.

This type of obfuscation is used to implement x86 jcc instructions and I don't have a cleaned function level ircfg that IRCFGSimplifierSSA required. I have tried this before and all register assignments except eax and esp were lost, which is wrong.

What I am tring to do is

  1. disassemble and deobfuscate current basic block
  2. figure out the jcc instruction (IRDst = ExprCond(cond, dest1, dest2))
  3. add dest1 and dest2 to basic block address list
  4. goto 1

Maybe I need a basic block level IRCFGSimplifierSSA.

serpilliere commented 3 years ago

The fact that miasm deletes all registers except EAX and ESP is a default behavior. You can subclass the lifter in order to keep all registers during simplifications.

See lifter_model_call.py:


class LifterModelCall_x86_16(Lifter_X86_16, LifterModelCall):

    def __init__(self, loc_db):
        Lifter_X86_16.__init__(self, loc_db)
        self.ret_reg = self.arch.regs.AX

    def get_out_regs(self, _):
        return set([self.ret_reg, self.sp])

class LifterModelCall_x86_32(Lifter_X86_32, LifterModelCall_x86_16):

    def __init__(self, loc_db):
        Lifter_X86_32.__init__(self, loc_db)
        self.ret_reg = self.arch.regs.EAX
    ...

But by default, if you have jumps to unknown destinations (ie incomplete graphs) by default miasm keeps all definitions. For example:

main:
        MOV EBX, 1
        CMP EAX, EBX
        JZ  0x11223344
        ADD ECX, 1
        JMP 0x11223355

which gives: graph

gives in IR: final

Note that eflags, EBX and ECX definitions are kept.

Or maybe I have missed something?

P1224 commented 3 years ago

Here is a obfuscated function sample:

global main
main:
push ebp
mov ebp, esp
cmp dword [ebp + 8], 1

push eax ; save eax && place holder for ret

pushf ; save eflags

pushf ; get eflags for bit calculation
pop eax
shr eax, 6
and eax, 1 ; get zf bit from eflags
push loc1
push loc0
mov eax, [esp + eax * 4] ; do select
add esp, 8

popf ; resotre eflags

xchg [esp], eax ; restore eax
ret

loc0:
mov eax, 0
leave
ret

loc1:
mov eax, 1
leave
ret

; nasm -f elf ta1.asm && gcc -m32 -o ta1 ta1.o && python3 q1.py ta1

And the script:

from __future__ import print_function

import sys

from future.utils import viewvalues
from miasm.analysis.binary import Container
from miasm.analysis.machine import Machine
from miasm.core.locationdb import LocationDB

from miasm.analysis.simplifier import IRCFGSimplifierCommon, IRCFGSimplifierSSA
from miasm.expression.simplifications import expr_simp, expr_simp_explicit, ExpressionSimplifier
from miasm.expression.expression import *

#####################################
# Common section from dis_binary.py #
#####################################

fdesc = open(sys.argv[1], 'rb')
loc_db = LocationDB()

cont = Container.from_stream(fdesc, loc_db)

machine = Machine(cont.arch)

mdis = machine.dis_engine(cont.bin_stream, loc_db=cont.loc_db)

# addr = cont.entry_point
addr = loc_db.get_name_offset('main')
head = loc_db.get_or_create_offset_location(addr)
asmcfg = mdis.dis_multiblock(addr)

from miasm.arch.x86.lifter_model_call import LifterModelCall_x86_32

class MyLifter(LifterModelCall_x86_32):
    def get_out_regs(self, _):
        ori = super().get_out_regs(_)
        full = ori | {
            self.arch.regs.EAX, 
            self.arch.regs.ECX,
            self.arch.regs.EDX,
            self.arch.regs.EBX,
            self.arch.regs.ESP,
            self.arch.regs.EBP,
            self.arch.regs.ESI,
            self.arch.regs.EDI,
            self.arch.regs.cf, 
            self.arch.regs.pf, 
            self.arch.regs.af, 
            self.arch.regs.zf,
            self.arch.regs.nf,
            self.arch.regs.of,
        }
        return full
#####################################
#    End common section             #
#####################################

lifter = MyLifter(mdis.loc_db)

# Get the IR of the asmcfg
ircfg_analysis = lifter.new_ircfg_from_asmcfg(asmcfg)

# Create joker for match expr
joker1 = ExprId('joker1', 32)
joker2 = ExprId('joker2', 32)
joker3 = ExprId('joker3', 1)
pattern = expr_simp(joker1 + (joker2 & ExprInt(1, 32)) * ExprInt(4, 32))
pattern2 = ExprCompose(joker3, ExprInt(0, 31)) * joker1
# Add simplification pass
def simp_lookup(expr_simp, expr):
    """
    Add simplification:
    @32[X + Y & 1] => ExprCond(Y & 1, @32[X+4], @32[X])
    """
    if expr.size != 32:
        return expr
    ptr = expr.ptr
    found = {}
    result = match_expr(ptr, pattern, set([joker1, joker2]), found)
    if not result:
        return expr
    base = found[joker1]
    index = found[joker2]
    print("found pattern in %s with %s %s" % (expr, base, index))
    src1 = expr_simp(ExprMem(base + ExprInt(4, 32), 32))
    src2 = expr_simp(ExprMem(base, 32))
    result = ExprCond(index & ExprInt(1, 32), src1, src2)
    result = expr_simp(result)
    return result

def simp_compose_mul(expr_simp, expr):
    '''
    {cond 0 1, 0x0 1 32} * const => ExprCond(cond, const, 0)
    '''
    out = {}
    if not match_expr(expr, pattern2, {joker1, joker3}, out):
        return expr
    cond = out[joker3]
    const = out[joker1]
    if not const.is_int():
        return expr
    return ExprCond(cond, const, ExprInt(0, expr.size))

# Enable pass

my_expr_simp = ExpressionSimplifier()
my_expr_simp.enable_passes(expr_simp_explicit.expr_simp_cb)
my_expr_simp.enable_passes({ExprMem: [simp_lookup]})
my_expr_simp.enable_passes({ExprOp: [simp_compose_mul]})

simplifier = IRCFGSimplifierSSA(lifter, my_expr_simp)
ircfg2 = simplifier.simplify(ircfg_analysis, head)
print('first attempt: ircfg from IRCFGSimplifierSSA')
print(ircfg2.get_block(loc_db.get_offset_location(addr)))

print('#' * 50)

from miasm.ir.symbexec import SymbolicExecutionEngine

# run from original ircfg
print('second attempt: run from original ircfg')
ircfg = lifter.new_ircfg_from_asmcfg(asmcfg)
engine = SymbolicExecutionEngine(lifter, sb_expr_simp=my_expr_simp)
engine.run_block_at(ircfg, head)
engine.del_mem_above_stack(lifter.arch.regs.ESP)
engine.dump()

print('#' * 50)
# run from ssa ircfg
print('third attempt: run from ssa ircfg')
engine = SymbolicExecutionEngine(lifter, sb_expr_simp=my_expr_simp)
engine.run_block_at(ircfg2, head)
engine.dump()

Output:

first attempt: IRCFGSimplifierSSA
b'main':

@32[ESP + 0xFFFFFFFC] = EBP

EBP.0 = ESP + 0xFFFFFFFC

@32[ESP + 0xFFFFFFF8] = EAX

@32[ESP + 0xFFFFFFF4] = {(@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32] 0 1, 0x1 1 2, parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF) 2 3, 0x0 3 4, (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5] 4 5, 0x0 5 6, @32[ESP + 0x4] == 0x1 6 7, (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32] 7 8, tf 8 9, i_f 9 10, df 10 11, ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32] 11 12, iopl_f 12 14, nt 14 15, 0x0 15 16, rf 16 17, vm 17 18, ac 18 19, vif 19 20, vip 20 21, i_d 21 22, 0x0 22 32}

@32[ESP + 0xFFFFFFF0] = {(@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32] 0 1, 0x1 1 2, parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF) 2 3, 0x0 3 4, (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5] 4 5, 0x0 5 6, @32[ESP + 0x4] == 0x1 6 7, (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32] 7 8, tf 8 9, i_f 9 10, df 10 11, ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32] 11 12, iopl_f 12 14, nt 14 15, 0x0 15 16, rf 16 17, vm 17 18, ac 18 19, vif 19 20, vip 20 21, i_d 21 22, 0x0 22 32}

@32[ESP + 0xFFFFFFF0] = 0x52D

@32[ESP + 0xFFFFFFEC] = 0x526

cf.4 = (@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32]

pf.4 = parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF)

af.2 = (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5]

zf.4 = @32[ESP + 0x4] == 0x1

nf.4 = (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32]

of.4 = ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32]

exception_flags = tf?(0x2,exception_flags)

@32[ESP + 0xFFFFFFF8] = (@32[ESP + 0x4] == 0x1)?(0x52D,0x526)

EAX.4 = EAX

ESP.9 = ESP + 0xFFFFFFFC

IRDst = (@32[ESP + 0x4] == 0x1)?(0x52D,0x526)

##################################################
second attempt: run from original ircfg
ESP                = ESP + 0xFFFFFFFC
EBP                = ESP + 0xFFFFFFFC
zf                 = @32[ESP + 0x4] == 0x1
nf                 = (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32]
pf                 = parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF)
cf                 = (@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32]
of                 = ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32]
af                 = (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5]
exception_flags    = tf?(0x2,exception_flags)
EIP                = (@32[ESP + 0x4] == 0x1)?(@32[ESP + 0xFFFFFFF0],@32[ESP + 0xFFFFFFEC])
IRDst              = (@32[ESP + 0x4] == 0x1)?(@32[ESP + 0xFFFFFFF0],@32[ESP + 0xFFFFFFEC])
@32[ESP + 0xFFFFFFFC] = EBP
##################################################
third attempt: run from ssa ircfg
EBP.0              = ESP + 0xFFFFFFFC
cf.4               = (@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32]
pf.4               = parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF)
af.2               = (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5]
zf.4               = @32[ESP + 0x4] == 0x1
nf.4               = (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32]
of.4               = ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32]
exception_flags    = tf?(0x2,exception_flags)
EAX.4              = EAX
ESP.9              = ESP + 0xFFFFFFFC
IRDst              = (@32[ESP + 0x4] == 0x1)?(0x52D,0x526)
@32[ESP + 0xFFFFFFEC] = 0x526
@32[ESP + 0xFFFFFFF0] = 0x52D
@32[ESP + 0xFFFFFFF4] = {(@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32] 0 1, 0x1 1 2, parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF) 2 3, 0x0 3 4, (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5] 4 5, 0x0 5 6, @32[ESP + 0x4] == 0x1 6 7, (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32] 7 8, tf 8 9, i_f 9 10, df 10 11, ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32] 11 12, iopl_f 12 14, nt 14 15, 0x0 15 16, rf 16 17, vm 17 18, ac 18 19, vif 19 20, vip 20 21, i_d 21 22, 0x0 22 32}
@32[ESP + 0xFFFFFFF8] = (@32[ESP + 0x4] == 0x1)?(0x52D,0x526)
@32[ESP + 0xFFFFFFFC] = EBP

For the entry basic block, my ideal output is (dont care it's ir assign blocks or symbolic state):

ESP                = ESP + 0xFFFFFFFC
EBP                = ESP + 0xFFFFFFFC
zf                 = @32[ESP + 0x4] == 0x1
nf                 = (@32[ESP + 0x4] + 0xFFFFFFFF)[31:32]
pf                 = parity((@32[ESP + 0x4] + 0xFFFFFFFF) & 0xFF)
cf                 = (@32[ESP + 0x4] ^ ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1)) ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[31:32]
of                 = ((@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF)) & (@32[ESP + 0x4] ^ 0x1))[31:32]
af                 = (@32[ESP + 0x4] ^ (@32[ESP + 0x4] + 0xFFFFFFFF) ^ 0x1)[4:5]
EIP                = (@32[ESP + 0x4] == 0x1)?(0x52D,0x526)
IRDst              = (@32[ESP + 0x4] == 0x1)?(0x52D,0x526)
@32[ESP + 0xFFFFFFFC] = EBP

The first output gives out many dead stack memory assignments, these can be removed by SymbolicExecutionEngine.del_mem_above_stack but I am not sure how to do the same thing in ircfg.

The second output, which is my original attempt, failed to simplify IRDst.

The thrid output gives out some weird ExprId('reg.num').

I'm confused and don't known how to do.

serpilliere commented 3 years ago

Hey @P1224!

You used two different techniques here. One using static analysis with the ircfgsimplifier, and another using symbolic execution. Has you saw, the IRCFGSimplifierSSA uses the SSA (Single Static Assignment). This implies that multiple versions of a register are present in the result, which are represented with the ExprId('reg.num') as you saw.

But dont be afraid of it: it can be a powerfull tool.

If you look at the output of the disassembling with the basic miasm example, you get:

python miasm/example/disasm/full.py  ta1 0x1190 -g -s -p -x

output_1

The interesting part is at the end of the block:

@32[ESP + 0xFFFFFFF8] = @32[ESP + zeroExt_32(FLAG_EQ_CMP(@32[ESP + 0x4], 0x1)) * 0x4 + 0xFFFFFFEC]

Miasm has (for now) no simplifications to handle this code and the resulting IRDst is:

IRDst = @32[ESP + 0xFFFFFFF8]

But you can add a simplification exactly as before here. In Miasm, the operator FLAG_EQ_CMP(X, Y) returns ExprInt(1, 1) if X == Y and ExprInt(0, 1) if X != Y. So we can add the simplification:


# Add simplification pass
def simp_ext_flag(expr_simp, expr):
    """
    Add simplification:
    zeroExt(FLAG_EQ_CMP(X, Y)) => ExprCond(X == Y, 1, 0)
    """
    if not expr.is_op("zeroExt_32"):
        return expr
    arg = expr.args[0]
    if not arg.is_op("FLAG_EQ_CMP"):
        return expr
    args = arg.args
    ret = ExprCond(ExprOp("==", *args), ExprInt(1, 32), ExprInt(0, 32))
    return ret

# Enable pass

expr_simp.enable_passes({ExprOp: [simp_ext_flag]})

which gives: final

As it simplifies the code, Miasm can apply more simplifications rules, and resolves the IRDst :smile:

...
@32[ESP + 0xFFFFFFF8] = (@32[ESP + 0x4] == 0x1)?(0x11BD,0x11B6)

EAX.4 = EAX

ESP.9 = ESP + 0xFFFFFFFC

IRDst = (@32[ESP + 0x4] == 0x1)?(0x11BD,0x11B6)