从网鼎杯ctf题目窥见符号执行
本帖最后由 Ginobili 于 2020-5-26 23:22 编辑2020网鼎杯青龙组有一道VM的逆向，通过向大佬请教弄明白了三种解题方法。其中两种方法都使用到了符号执行。于是就去学习了一下。现借着这个题目的做法讲一下符号执行的操作。
符号执行
首先介绍一下符号执行：符号执行 （Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。 ---------------来自维基百科
通俗一点来说就是我们可以去模拟整个程序的执行过程，比方说我们输入一个字符串，程序经过一系列的加密与判断之后和某个字符串进行比较，然后进行正确和错误的判断跳转。我们就可以使用符号执行并且限定要跳转正确结果来模拟这个过程，这个时候，我们输入的数值就作为一个符号，就可以在限定的条件下探索所有的路径。并找出其中的正确结果。
我们比较著名的工具有SMT和SAT（我所使用的Ponce插件就是利用了SMT的功能）。
下面是题目：
signal：
1.Ponce
可以看到程序进行了一个vm指令的加密，&unk_403040是给定的opcode,进入函数我们查看算法。
int __cdecl vm_operad(int *a1, int a2)
{
int result; // eax@2
char v3; // @4
char v4; // @5
char v5; // @5
int v6; // @1
int v7; // @1
int v8; // @1
int v9; // @1
int v10; // @1
v10 = 0;
v9 = 0;
v8 = 0;
v7 = 0;
v6 = 0;
while ( 1 )
{
result = v10;
if ( v10 >= a2 )
return result;
switch ( a1 )
{
case 10:
read(v3); // 输入操作，且长度限定为15
++v10;
break;
case 1:
v4 = v5;
++v10;
++v7;
++v9;
break;
case 2:
v5 = a1 + v3;
v10 += 2;
break;
case 3:
v5 = v3 - LOBYTE(a1);
v10 += 2;
break;
case 4:
v5 = a1 ^ v3;
v10 += 2;
break;
case 5:
v5 = a1 * v3;
v10 += 2;
break;
case 6:
++v10;
break;
case 7:
if ( v4 != a1 ) // 最后判断的结果
{
printf("what a shame...");
exit(0);
}
++v8;
v10 += 2;
break;
case 11:
v5 = v3 - 1;
++v10;
break;
case 12:
v5 = v3 + 1;
++v10;
break;
case 8:
v3 = v5;
++v10;
++v6;
break;
default:
continue;
}
}
}
v3为输入的数值，长度限定。整个流程是先输入长度是15的字符串，进行加密，最后与opcode的某个值是否相等来判断。
我们的思路是：可以限定程序执行正确的结果，在刚输入字符串之后设置符号。进行执行。
其中用到了ida的一个插件Ponce。附上项目链接：
https://github.com/illera88/Ponce
说一下Ponce的坑，这个插件ida7.x版本使用比较复杂。配置也很复杂，建议使用ida6.8或者6.9的版本。使用6.8的时候最新的版本不能使用的话可以使用最老那几个版本。
我们开始操作，找到输入的位置之后下断。
然后在它最终的判断位置下断。相当于我们限定了范围。
打开Ponce插件，选择符号执行。
开启动态调试，输入15个数字之后程序断在了第一个断点处。我们跟随输入的数据，右键->在数据中跟随
找到位置后一定要点击到汇编窗口再次按Ctrl+Shift+M。弹出符号窗口输入数据。
F9继续运行，程序运行到跳转处，这个时候就是第一个字符的加密过程后的判断。我们对其符号执行之后查看“右键->SMT->solve->formula->第一处”输出窗口查看结果。
进行下面的执行，我们直接修改EIP到正确分支。F9运行重复上述结果最终得到flag
2.Angr
就简单说一下Angr是一个基于符号执行和模拟执行的二进制框架，可以用在很多的场景。重要的一点是Angr可以在linux下符号执行windows程序。安装过程有可能点复杂。
import angr
p= angr.Project('./signal.exe',auto_load_libs=False)#auto_load_libs是否加载依赖的库
state=p.factory.entry_state()#设置entry_state
simgr=p.factory.simgr(state)#创建一个simulation_manager进行模拟执行
simgr.explore(find=0x40175E,avoid=0x4016E6)#进行模拟执行
print(simgr.found.posix.dumps(0))#用simgr.found找到所有复合条件的分支,dumps可以获得文件输入的内容
关于符号执行我暂时理解了这么一点。欢迎大佬交流批评！
附上请教的L15263458908师傅的题解链接和参考的链接：
https://www.52pojie.cn/thread-1176826-1-1.html
angr学习：https://xz.aliyun.com/t/3990
符号执行：https://www.k0rz3n.com/2019/02/28/%E7%AE%80%E5%8D%95%E7%90%86%E8%A7%A3%E7%AC%A6%E5%8F%B7%E6%89%A7%E8%A1%8C%E6%8A%80%E6%9C%AF/#0X02-%E4%BB%8E%E5%85%AC%E5%BC%8F%E5%8E%9F%E7%90%86%E4%B8%8A%E7%90%86%E8%A7%A3%E7%AC%A6%E5%8F%B7%E6%89%A7%E8%A1%8C
题目链接：https://pan.baidu.com/s/1IIKlkQ6EOLaYXXJBcpoMYw
提取码：9m2l
为什么都这么优秀{:1_921:} 这个有点深度 感谢楼主分享！！！学到了！！！ 稍微复杂的跑不出来的，秒秒简单的还行 嗯嗯 感谢分享！ 感觉这东西主要还是用在ctf，实战没怎么看到有人用过 感谢分享，我也去试试Ponce 流浪星空 发表于 2020-5-27 09:57
嗯嗯 感谢分享！
LLeave师傅？ 学到了新方法
页:
[1]
2