试试miasm的符号执行。虽然感觉miasm比较老学了不知道有没有用，不过先学几天玩玩也不是不行

仍然是看的官方blog

https://miasm.re/blog/2017/10/05/playing_with_dynamic_symbolic_execution.html

这次环境纯Ubuntu22+miasm0.1.3+vscode remote，不想再被0.1.5折磨了，遂更换。

动态符号执行

动态符号执行（Dynamic Symbolic Execution）是一种软件测试和分析技术，用于自动化地探索程序的执行路径和输入空间。与传统的静态分析或基于覆盖率的测试方法相比，动态符号执行具有更高的覆盖率和更好的路径探索能力。

模拟

用tigress的一个程序来测试miasm的动态符号执行

https://github.com/JonathanSalwan/Tigress_protection/blob/master/tigress-challenges/tigress-0-challenge-0

1
2
3
4
5
6
7
8
9
10
11
12
13
14
from miasm.analysis.sandbox import Sandbox_Linux_x86_64

# Create sandbox
parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer")
parser.add_argument("filename", help="ELF Filename")
options = parser.parse_args()
# Force environment simulation
options.mimic_env = True
# Dummy argument: 123456789
options.command_line = ["".join(chr(0x30 + i) for i in range(1, 10))]

# Instantiate and run
sb = Sandbox_Linux_x86_64(options.filename, options, globals())
sb.run()

只是在官方示例上加了一个输入，flag是命令行输入的。

直接运行后报错

1
ValueError: ('unknown api', '0x71111044', "'xxx_strtoul'")

非常经典的补环境的操作，这个报错是因为strtoul没有实现模拟不了。

对着strtoul的代码实现一遍

1
2
3
4
5
6
7
def xxx_strtoul(jitter:jitter_x86_64):
    ret_ad, args = jitter.func_args_systemv(["nptr", "endptr", "base"])
    assert args.endptr == 0
    content = win_api_x86_32.get_win_str_a(jitter,args.nptr)

    value = int(content, args.base)
    jitter.func_ret_systemv(ret_ad, ret_value=value)

解释一遍。首先是func_args_systemv，就是获取该模拟的函数的参数。直接去ida或者谷歌其参数即可。

image-20240418193344956

然后即可获取args，通过args.xxx即可访问获取的参数的具体的值，打印出args的话输出如下

1
args(nptr=1310700, endptr=0, base=10)

很好理解。随后就是一个获取字符的函数。别问我为什么是win_api_x86_32,而不是linux_api_x86_64，我也很奇怪。将nptr指向的内存的值获取，也就是我们的输入(在ida代码中可知传入的就是我们的输入)。然后将输入转成int后返回，调用func_ret_systemv返回。总体来说就是模拟一遍这个函数的实现。

然后跑一遍，函数成功模拟了，但是报错内存错误。这是因为有canary。canary我们也得模拟

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
from miasm.analysis.sandbox import Sandbox_Linux_x86_64
from miasm.arch.x86.jit import jitter_x86_64
from miasm.os_dep import win_api_x86_32
from miasm.jitter.csts import PAGE_READ

def xxx_strtoul(jitter:jitter_x86_64):
    ret_ad, args = jitter.func_args_systemv(["nptr", "endptr", "base"])
    assert args.endptr == 0
    print(args)
    content = win_api_x86_32.get_win_str_a(jitter,args.nptr)

    value = int(content, args.base)
    jitter.func_ret_systemv(ret_ad, ret_value=value)


# Create sandbox
parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer")
parser.add_argument("filename", help="ELF Filename")
options = parser.parse_args()
# Force environment simulation
options.mimic_env = True
# Dummy argument: 123456789
options.command_line = ["".join(chr(0x30 + i) for i in range(1, 10))]
options.jitter = "python"
# Instantiate and run
sb = Sandbox_Linux_x86_64(options.filename, options, globals())

sb.jitter.ir_arch.do_all_segm = True
FS_0_ADDR = 0x7ff70000
sb.jitter.cpu.FS = 0x4
sb.jitter.cpu.set_segm_base(sb.jitter.cpu.FS,FS_0_ADDR)
sb.jitter.vm.add_memory_page(FS_0_ADDR + 0x28, PAGE_READ, b"\x42\x42\x42\x42\x42\x42\x42\x42", "Stack canary FS[0x28]")
sb.run()

接着解释代码。这里是首先在一个比较高的内存区域设置一个FS的段基址的地址。然后将FS寄存器设置为4，表示FS寄存器指向GDT的第四个段描述符。随后用set_segm_base将FS寄存器的段基址设置为FS_0_ADDR，这样的话，当程序用FS寄存器做内存访问时，会使用这个FS_0_ADDR作基址。

最后就是调用add_memory_page，在内存中加一个页，起始地址是FS_0_ADDR+0x28，权限只读。存储了八个字节，实际上就是FS:[0x28]处的canary而已。

跑一遍后得出加密后的结果

image-20240418193839599

添加动态符号执行

我们已经能模拟了，现在我们想获取输入生成输出的约束，也就是获得输出的方程，需要用到我们的这次的主题的动态符号执行了。

首先导入miasm的符号执行引擎，然后和z3一样创建一个64位的符号。然后创建一个符号执行引擎，接下来add_lib_handler应该是指定要模拟执行的程序所依赖的库，我也不是很懂。

1
2
3
4
from miasm.expression.expression import ExprId, ExprInt
VALUE = ExprId("VALUE", 64)
dse = DSEEngine(sb.machine)
dse.add_lib_handler(sb.libs, globals())

这里我们把strtoul的返回值符号化，然后在printf时将约束打印出来看看怎么个事儿

首先符号化返回值

1
2
3
4
5
6
7
8
9
10
11
12
13
def xxx_strtoul(jitter:jitter_x86_64):
    ret_ad, args = jitter.func_args_systemv(["nptr", "endptr", "base"])
    assert args.endptr == 0
    print(args)
    content = win_api_x86_32.get_win_str_a(jitter,args.nptr)

    value = int(content, args.base)
    jitter.func_ret_systemv(ret_ad, ret_value=value)
    dse.attach(jitter)
    dse.update_state_from_concrete()
    dse.update_state({
        dse.ir_arch.arch.regs.RAX: VALUE,
    })

update_state_from_concrete相当于先把实际执行的代码的数据和模拟的数据同步一下，然后下一步更新rax的值为一个符号。随后的操作就是符号的操作了。这里我们需要把printf也重改一下，因为我们这次输出的不是一个数而是一个带约束的符号。我们直接输出它的第二个参数，看看约束的结果。

1
2
3
def xxx_printf_symb(dse:DSEEngine):
    result = dse.eval_expr(dse.ir_arch.arch.regs.RSI)
    print(result)

输出了一大堆约束的代码

image-20240418202338637

我们尝试将最开始的确定的输入带入进去。看看结果是不是和直接执行的一样

1
2
3
4
def xxx_printf_symb(dse:DSEEngine):
    result = dse.eval_expr(dse.ir_arch.arch.regs.RSI)
    obtained = dse.symb.expr_simp(result.replace_expr({VALUE: ExprInt(123456789, 64)}))
    print(obtained)

可以看到输出的结果是一样的，也就是说符号执行的比较成功。

动态符号执行+fuzz

用的也是这个文章的案例。