试试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_64parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer" ) parser.add_argument("filename" , help ="ELF Filename" ) options = parser.parse_args() options.mimic_env = True options.command_line = ["" .join(chr (0x30 + i) for i in range (1 , 10 ))] 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或者谷歌其参数即可。
然后即可获取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_64from miasm.arch.x86.jit import jitter_x86_64from miasm.os_dep import win_api_x86_32from miasm.jitter.csts import PAGE_READdef 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) parser = Sandbox_Linux_x86_64.parser(description="ELF sandboxer" ) parser.add_argument("filename" , help ="ELF Filename" ) options = parser.parse_args() options.mimic_env = True options.command_line = ["" .join(chr (0x30 + i) for i in range (1 , 10 ))] options.jitter = "python" 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而已。
跑一遍后得出加密后的结果
添加动态符号执行 我们已经能模拟了,现在我们想获取输入生成输出的约束,也就是获得输出的方程,需要用到我们的这次的主题的动态符号执行了。
首先导入miasm的符号执行引擎,然后和z3一样创建一个64位的符号。然后创建一个符号执行引擎,接下来add_lib_handler应该是指定要模拟执行的程序所依赖的库,我也不是很懂。
1 2 3 4 from miasm.expression.expression import ExprId, ExprIntVALUE = 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)
输出了一大堆约束的代码
我们尝试将最开始的确定的输入带入进去。看看结果是不是和直接执行的一样
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 用的也是这个文章的案例。