文章插图
PS：因为最近开始考试 ， 耽误了很多时间 ， 重新开始恢复
在之前的学习中我们学会了利用angr符号化寄存器、栈上的值、内存、malloc开辟的动态内存和文件系统 ， 感受到了angr强大的仿真系统 ， 在CTF中题目的简单利用 ， 接下来我们要学习angr的更多的高级用法
由于angr的api一直有一些变化 ， 网上的很多脚本需要修改才能运行
08_angr_constraints该题主要学习通过添加约束条件来解决路径爆炸问题
首先检查一下该程序：
syc@ubuntu:~/Desktop/TEMP$ checksec 08_angr_constraints[*] '/home/syc/Desktop/TEMP/08_angr_constraints'Arch:i386-32-littleRELRO:Partial RELROStack:No canary foundNX:NX enabledPIE:No PIE (0x8048000)然后进入IDA查看该：
int __cdecl main(int argc, const char **argv, const char **envp){signed int i; // [esp+Ch] [ebp-Ch]password = 1146115393;dword_804A044 = 1380994638;dword_804A048 = 1381647695;dword_804A04C = 1112233802;memset(printf("Enter the password: ");__isoc99_scanf("%16s",for ( i = 0; i <= 15; ++i )*(_BYTE *)(i + 0x804A050) = complex_function(*(char *)(i + 0x804A050), 15 - i);if ( check_equals_AUPDNNPROEZRJWKB(elseputs("Try again.");return 0;}int __cdecl complex_function(signed int a1, int a2){if ( a1 <= 64 || a1 > 90 ){puts("Try again.");exit(1);}return (a1 - 65 + 53 * a2) % 26 + 65;}_BOOL4 __cdecl check_equals_AUPDNNPROEZRJWKB(int a1, unsigned int a2){int v3; // [esp+8h] [ebp-8h]unsigned int i; // [esp+Ch] [ebp-4h]v3 = 0;for ( i = 0; i < a2; ++i ){if ( *(_BYTE *)(i + a1) == *(_BYTE *)(i + 0x804A040) )++v3;}return v3 == a2;}路径爆炸通过我们之前的学习体验感觉到angr这么强大的应用怎么没有在实际的测试生产中大规模应用 ， 这是因为给符号执行技术在复杂程序的测试案例生成的应用中造成阻碍的两个大问题：一个是约束求解问题 ， 另一个就是路径爆炸问题
所谓符号执行就是把程序中的变量符号化去模拟程序运行 ， 搜集路径约束条件并使用约束求解器对其进行求解后得到结果 。 当一个程序存在循环结构时 ， 即使逻辑十分简单也可能会产生规模十分巨大的执行路径 。 在符号执行的过程中 ， 每个分支点都会产生两个实例 ， 当程序中存在循环结构展开时 ， 可能会导致程序分支路径数呈指数级增长 ， 即路径爆炸问题 。 故我们需要提供更多的约束条件控制路径爆照问题
回到这个题目本身
_BOOL4 __cdecl check_equals_AUPDNNPROEZRJWKB(int a1, unsigned int a2){int v3; // [esp+8h] [ebp-8h]unsigned int i; // [esp+Ch] [ebp-4h]v3 = 0;for ( i = 0; i < a2; ++i ){if ( *(_BYTE *)(i + a1) == *(_BYTE *)(i + 0x804A040) )++v3;}return v3 == a2;}check_equals_AUPDNNPROEZRJWKB()函数就是一个字符一个字符的比较 ， 就会产生路径爆炸问题 ， 原始也是每次调用循环中的if语句（16次）时 ， 计算机都需要产生判断分支 ， 从而导致2 ^ 16 = 65,536分支 ， 这将花费很长时间来测试并获得我们的答案 。 我们解决这个问题的答案 ， 直接用约束条件取代这个判断函数 ， 用字符串直接比较约束 ， 从而避免因为循环和判断语句逐一字符比较而产生分支引起路径爆炸问题
约束求解在angr中提供了可以用加入一个约束条件到一个state中的方法（state.solver.add） ， 将每一个符号化的布尔值作为一个关于符号变量合法性的断言 。 之后可以通过使用state.solver.eval(symbol)对各个断言进行评测来求出一个合法的符号值（若有多个合法值 ， 返回其中的一个） 。 简单来说就是通过 .add 对 state 对象添加约束 ， 并使用 .eval 接口求解 ， 得到符号变量的可行解
例如：
# fresh state>>> state = proj.factory.entry_state()>>> state.solver.add(x - y >= 4)>>> state.solver.add(y > 0)>>> state.solver.eval(x)5>>> state.solver.eval(y)1>>> state.solver.eval(x + y)6总而言之先放EXP ， 再逐步分析：
import angrimport sysimport claripydef Go():path_to_binary = "./08_angr_constraints"project = angr.Project(path_to_binary, auto_load_libs=False)start_address = 0x8048625buff_addr = 0x0804A050address_to_check_constraint = 0x08048565initial_state = project.factory.blank_state(addr=start_address)char_size_in_bits = 8passwd_len = 16passwd0 = claripy.BVS('passwd0', char_size_in_bits*passwd_len)initial_state.memory.store(buff_addr, passwd0)simulation = project.factory.simgr(initial_state)simulation.explore(find=address_to_check_constraint)if simulation.found:solution_state = simulation.found[0]constrained_parameter_address = buff_addrconstrained_parameter_size_bytes = 16constrained_parameter_bitvector = solution_state.memory.load(constrained_parameter_address,constrained_parameter_size_bytes)constrained_parameter_desired_value = 'http://kandian.youth.cn/index/AUPDNNPROEZRJWKB'solution_state.solver.add(constrained_parameter_bitvector == constrained_parameter_desired_value)solution0 = solution_state.solver.eval(passwd0,cast_to=bytes)print("[+] Success! Solution is: {0}".format(solution0))else:raise Exception('Could not find the solution')if __name__ == "__main__":Go()