[NCTF 2023] Re
中文编程1
载入x64dbg，注意到一堆浮点运算，果断载入IDA。
由于易语言中的整数操作，全部都是拿浮点数进行的，所以这里直接大胆假设为整数，进行计算。
唯一坑人的地方在于，有一个数字，xxxx.e11，.e11去掉后是错误的，因为少了个0，这个卡了很久。
from z3 import *
s = Solver()
flag_length = 11
v4=[i for i in range(flag_length)]
for i in range(flag_length):
v4[i] = Real("v{}".format(i))
s.add(v4[0]*52+v4[1]*93+v4[2]*15+v4[3]*72+v4[4]*61+v4[5]*21+v4[6]*83+v4[7]*87+v4[8]*75+v4[9]*75+v4[10]*88==786241466532)
s.add(v4[0]*24+v4[1]*3 +v4[2]*22+v4[3]*53+v4[4]*2 +v4[5]*88+v4[6]*30+v4[7]*38+v4[8]*2 +v4[9]*64+v4[10]*60==376271212978)
s.add(v4[0]*21+v4[1]*33+v4[2]*76+v4[3]*58+v4[4]*22+v4[5]*89+v4[6]*49+v4[7]*91+v4[8]*59+v4[9]*42+v4[10]*92==647642467922)
s.add(v4[0]*60+v4[1]*80+v4[2]*15+v4[3]*62+v4[4]*62+v4[5]*47+v4[6]*62+v4[7]*51+v4[8]*55+v4[9]*64+v4[10]*3==670839740597)
s.add(v4[0]*51+v4[1]*7 +v4[2]*21+v4[3]*73+v4[4]*39+v4[5]*18+v4[6]*4 +v4[7]*89+v4[8]*60+v4[9]*14+v4[10]*9==549200140865)
s.add(v4[0]*90+v4[1]*53+v4[2]*2 +v4[3]*84+v4[4]*92+v4[5]*60+v4[6]*71+v4[7]*44+v4[8]*8 +v4[9]*47+v4[10]*35==664730113280)
s.add(v4[0]*78+v4[1]*81+v4[2]*36+v4[3]*50+v4[4]*4 +v4[5]*2 +v4[6]*6 +v4[7]*54+v4[8]*4 +v4[9]*54+v4[10]*93==476762422687)
s.add(v4[0]*63+v4[1]*18+v4[2]*90+v4[3]*44+v4[4]*34+v4[5]*74+v4[6]*62+v4[7]*14+v4[8]*95+v4[9]*48+v4[10]*15==644352175854)
s.add(v4[0]*72+v4[1]*78+v4[2]*87+v4[3]*62+v4[4]*40+v4[5]*85+v4[6]*80+v4[7]*82+v4[8]*53+v4[9]*24+v4[10]*26==787224288556)
s.add(v4[0]*89+v4[1]*60+v4[2]*41+v4[3]*29+v4[4]*15+v4[5]*45+v4[6]*65+v4[7]*89+v4[8]*71+v4[9]*9 +v4[10]*88==667891172792)
s.add(v4[0] +v4[1]*8 +v4[2]*88+v4[3]*63+v4[4]*11+v4[5]*81+v4[6]*8 +v4[7]*35+v4[8]*35+v4[9]*33+v4[10]*5==417587420064)
flag = []
if s.check() == sat:
ans = s.model()
for i in range(flag_length):
flag.append(ans[v4[i]])
else:
print("unable to solve...")
for x in flag:
print(x,end=" ")
有11组DWORD，每一组都是flag的ASCII码拼接而成，用z3进行爆破，最后还原就行。
Jvav
先拖入jadx，发现混淆直接给jadx干爆了，然后拖入GDA，发现同样被干爆。最后拖入JByteMod中，发现成功读取，也不需要进行反混淆，效果如图：
然后在Idea里面新建一个项目，手动拷贝（由于部分解密函数有调用栈检测，所以不好扣出来）
进行了一会人工反混淆后，注意flag判断：（var4是用户输入的东西异或51的结果）
if(ALLATORIxDEMO(var4).equals("😉😶😌😕😃😀😃😄😉😂🙂😀🤐😂🤗☹️🤗😐🤗😱😃🤣😀😘😐😄😔😄😃🤣🤨😋🤐😑😌🙂🤗😂😌🤐😃😀🤨😄🤗🤨🙂🤐😉🤩😔😘😐🙂😛😍😤😘😌😚😗🤩😧🤗"));
那么前面的这个ALLATORIxDEMO一定就是关键函数。通过更改输入，发现这个函数对于一个字符的输入可能会引起1-2个emoji的变化。我这里采用了爆破的方法：
static int simi(String a) {
int sum = 0;
String re = "😉😶😌😕😃😀😃😄😉😂🙂😀🤐😂🤗☹️🤗😐🤗😱😃🤣😀😘😐😄😔😄😃🤣🤨😋🤐😑😌🙂🤗😂😌🤐😃😀🤨😄🤗🤨🙂🤐😉🤩😔😘😐🙂😛😍😤😘😌😚😗🤩😧🤗";
for (int i = 0;i < re.length();i++)
{
if(re.charAt(i) != a.charAt(i)) continue;
sum++;
}
return sum;
}这个函数返回加密后的flag和真正加密后flag的相似度（字符匹配，如果相同位置一样则++）
然后通过一个函数进行爆破
public static void test()
{
var arr = new char[]{'a', 'b', 'c', 'd', 'e', 'f', '-', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9'};
String flag = "\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0";
StringBuilder strBuilder = new StringBuilder(flag);
for(int j = 0;j < flag.length();j++)
{
char max_char = '0';
int lastSimi = 0;
for(int k = 0; k<arr.length;k++)
{
strBuilder.setCharAt(j, arr[k]);
var bf = strBuilder.toString().getBytes();
for(int i = 0;i < flag.length();i ++) {
bf[i] = (byte)(bf[i] ^ 51);
}
String result = ALLATORIxDEMO(bf);
int s = simi(result);
if(s >= lastSimi)
{
max_char = arr[k];
lastSimi = s;
}
}
strBuilder.setCharAt(j, max_char);
System.out.println(strBuilder.toString());
}a
a9
a97
a979
a979b
a979b9
a979b92
a979b923
a979b923-
a979b923-6
a979b923-68
a979b923-68c
a979b923-68c6
a979b923-68c6-
a979b923-68c6-7
a979b923-68c6-7c
a979b923-68c6-7c0
a979b923-68c6-7c0f
a979b923-68c6-7c0f-
a979b923-68c6-7c0f-b
a979b923-68c6-7c0f-b7
a979b923-68c6-7c0f-b7f
a979b923-68c6-7c0f-b7f9
a979b923-68c6-7c0f-b7f9-
a979b923-68c6-7c0f-b7f9-a
a979b923-68c6-7c0f-b7f9-a7
a979b923-68c6-7c0f-b7f9-a7c
a979b923-68c6-7c0f-b7f9-a7c1
a979b923-68c6-7c0f-b7f9-a7c14
a979b923-68c6-7c0f-b7f9-a7c147
a979b923-68c6-7c0f-b7f9-a7c1476
a979b923-68c6-7c0f-b7f9-a7c14769
a979b923-68c6-7c0f-b7f9-a7c14769c
a979b923-68c6-7c0f-b7f9-a7c14769cb
a979b923-68c6-7c0f-b7f9-a7c14769cb4
a979b923-68c6-7c0f-b7f9-a7c14769cb49输入测试，发现是错的，但是大致雏形已经有了。
然后进行更精细化的爆破
String flag = "a973b923-68bf-430f-b42a-a7a1472b\0\0\0\0";
StringBuilder strBuilder = new StringBuilder(flag);
var arr = new char[]{'a', 'b', 'c', 'd', 'e', 'f', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9'};
for(char a1 : arr)
{
for(char a2 : arr)
{
for(char a3 : arr)
{
for(char a4 : arr)
{
for(int i = 0;i < arr.length;i++)
{
strBuilder.setCharAt(32, a1);
strBuilder.setCharAt(33, a2);
strBuilder.setCharAt(34, a3);
strBuilder.setCharAt(35, a4);
var bf = strBuilder.toString().getBytes();
for(int j = 0;j < flag.length();j ++) {
bf[j] = (byte)(bf[j] ^ 51);
}
String result = ALLATORIxDEMO(bf);
//System.out.println(result);
if(result.startsWith("\uD83D\uDE09\uD83D\uDE36\uD83D\uDE0C\uD83D\uDE15\uD83D\uDE03\uD83D\uDE00\uD83D\uDE03\uD83D\uDE04\uD83D\uDE09\uD83D\uDE02\uD83D\uDE42\uD83D\uDE00\uD83E\uDD10\uD83D\uDE02\uD83E\uDD17☹\uFE0F\uD83E\uDD17\uD83D\uDE10\uD83E\uDD17\uD83D\uDE31\uD83D\uDE03\uD83E\uDD23\uD83D\uDE00\uD83D\uDE18\uD83D\uDE10\uD83D\uDE04\uD83D\uDE14\uD83D\uDE04\uD83D\uDE03\uD83E\uDD23\uD83E\uDD28\uD83D\uDE0B\uD83E\uDD10\uD83D\uDE11\uD83D\uDE0C\uD83D\uDE42\uD83E\uDD17\uD83D\uDE02\uD83D\uDE0C\uD83E\uDD10\uD83D\uDE03\uD83D\uDE00\uD83E\uDD28\uD83D\uDE04\uD83E\uDD17\uD83E\uDD28\uD83D\uDE42\uD83E\uDD10\uD83D\uDE09\uD83E\uDD29\uD83D\uDE14\uD83D\uDE18\uD83D\uDE10\uD83D\uDE42\uD83D\uDE1B\uD83D\uDE0D\uD83D\uDE24\uD83D\uDE18\uD83D\uDE0C\uD83D\uDE1A\uD83D\uDE17\uD83E\uDD29\uD83D\uDE27\uD83E\uDD17"))
{
System.out.println(strBuilder.toString());
}
}
}
}
}
}通过手动修改，每四个进行爆破，逐个敲出（时间复杂度$O(n^4)$），最后得到了flag：
flag{a973b923-68bf-430f-b42a-a7a1472bcb49}(本题用时2小时)
比赛结束后听别人说，这是base64改的，直接爆了。
ezVM
拖入x64dbg和IDA进行对比，注意到有upx壳，所以直接upx -d，然后继续进行分析。拖入IDA后，发现
但是其实F5后，VM的架构已经很清晰了。我们只需要拿到vm字节码，然后进行自动化或者手动分析即可。
经过一段时间的F8单步跑后，注意到vm中许多指令并没有用，switch中直接走了default路径;但是这对我们的静态分析是比较困难的。我们其实可以直接从gets_s开始分析。
方法一、由于动态调试x64dbg的方便性，我们可以采用对输入的东西进行内存软件/硬件断点，然后逐个追踪并分析，逐字节拿到flag，而且我们也知道flag长度是44，且格式为flag{.?}，这个方法虽然很慢，但是能保证做出来。
方法二、静态对字节码进行分析，注意到
case 50u:
v7 = byte_140004040[v4];
v5 = (unsigned int)(v5 - 1);
dword_14001FF94 = v5;
LODWORD(v4) = v4 + 1;
byte_14002058F[v5 + 1] = v7;
continue;实际上是从字节码下一位拿到一个值，并把它推入vStack上，我们记作vmLdImm8
case 184u:
byte_14002058F[v5 + 1] = *(_BYTE *)(byte_14002058F[v5 + 1] + *(_QWORD *)&byte_14002058F[v5 + 2]);
continue;这个是从栈上拿到一个值（offset）和一个指针ptr，进行寻址并push到栈上
这两个其实完成了从某个地址拿数据的操作。注意到vm里面其实一直在进行这样的操作，且input handler会push buffer的地址
case 123u:
v14 = (char)byte_14002058F[v5 + 1];
v15 = (unsigned int)(v5 - 7);
dword_14001FF94 = v15;
*(_QWORD *)&byte_14002058F[v15 + 1] = Buffer;
gets_s(Buffer, v14);
goto LABEL_2;如此以来，对于VM的数据读入，我们就可以对其字节码进行正则匹配或者是python中自动处理，而且我们无需管垃圾指令。数据拿到以后，我们需要继续分析VM。发现VM其实是在对数据进行xor操作并在最后判断是否为0，而且每个xor指令中都没有掺入垃圾指令，这在VM的字节码中重复率很高，非常显眼，而且没组相同数据之前都有一个vmLdImm8, imm的形式，记录下来每一个立即数，在最后即可还原flag。
不过在还原xor的时候，还需要用到一些万用门的知识（实际上可以才出来是xor）
万用门实现逻辑指令
理论知识：
vmp里面只有1个逻辑运算指令 not_not_and 设这条指令为P
P(a,b) = ~a & ~b
这条指令的神奇之处就是能模拟 not and or xor 4条常规的逻辑运算指令
怕忘记了，直接给出公式，后面的数字指需要几次P运算
not(a) = P(a,a) 1
and(a,b) = P(P(a,a),P(b,b)) 3
or(a,b) = P(P(a,b),P(a,b)) 2
xor(a,b) = P(P(P(a,a),P(b,b)),P(a,b)) 5
————————————————
版权声明：本文为CSDN博主「鱼无伦次」的原创文章，遵循CC 4.0 BY-SA版权协议，转载请附上原文出处链接及本声明。
原文链接：https://blog.csdn.net/u014738665/article/details/120722455 // VM部分字节码
VmgetInput
..trash
vmLdImm8, 输入字符的索引,
vLoadMemoryImm8,
vmLdImm8, Imm
vm_xor
..trash
vmLdImm8, Imm
vm_xor
..trash
vmLdImm8, Imm
vm_xor
....
重复很多次最后得到Flag:flag{O1SC_VM_1s_h4rd_to_r3v3rs3_#a78abffaa#}
评论已关闭