记一次brainfuck逆向分析

记一次brainfuck逆向分析

5m10v3

这是笔者第一次分析brainfuck感觉蛮有学习意义的,同时记录一下自己的学习过程,如果有不足之处,请各位师傅多多指正。

题目下载链接
rbf

Brainfuck介绍

以下是来自维基百科的介绍

1
2
3
4
5
6
Brainfuck,简称BF,是一种极小化的程序语言,由Urban Müller在1993年创造。Fuck在英语中是脏话,所以这种语言有时称为Brainf*ck或Brainf***,或者只用简称。
Müller的目标是创建一种简单的、可以用最小的编译器来实现的、符合图灵完全思想的编程语言。这个语言由八种运算符构成,为Amiga机器编写的编译器(第二版)只有240个字节大小。[1]

Brainfuck的名字已经暗示出来,它的程序代码很难读懂。尽管如此,Brainfuck仍然可以像图灵机一般完成任何计算任务。它虽然计算方式与众不同,但确实能够正确运行。

这种语言基于一个简单的机器模型。这个机器除了指令以外,还包括:一个以字节为单位、已初始化为零的数组、一个指向该数组的指针(开始时指向数组的第一个字节)、以及用于输入输出的两个字节流。

下面是这八种状态的描述,其中每个状态由一个字符标识:

字符 含义
> 指针加一
< 指针减一
+ 指针所指字节的值加一
- 指针所指字节的值减一
. 输出指针所指字节内容(ASCII码
, 向指针所指的字节输入内容(ASCII码)
[ 若指针所指字节的值为零,则向后跳转,跳转到其对应的]的下一个指令处
] 若指针所指字节的值不为零,则向前跳转,跳转到其对应的[的下一个指令处

Brainfuck指令可以逐一替换,翻译成C语言(假设ptrchar *类型)的语句之类:

Brainfuck C
> ++ptr;
< --ptr;
+ ++*ptr;
- --*ptr;
. putchar(*ptr);
, *ptr = getchar();
[ while (*ptr) {
] }

从以上来看它只用了八条指令就实现了图灵完备,那么对于这种题目,比较好的方法就是写一个解释器出来,那么接下来笔者将会通过一道例题来讲解brainfuck的分析思路

例题

mini-L2025-rbf

题目简介如下:

经过java层的分析可知,首先检验flag的格式和长度,然后再调用native的check函数进行校验

native层的check函数会检查flag的内容必须都是小写字母,然后才会调用brainfuck进行flag的检验

直接下断点提取brainfuck的操作码,提取结果如下图:

接下来就是解析器的编写

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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
#include <iostream>
#include <windows.h>
#include <fstream>
#include <map>

int WriteToFile(const std::string &file_string, const std::string str)
{
std::ofstream OsWrite(file_string, std::ofstream::trunc);
OsWrite << str;
OsWrite << std::endl;
OsWrite.close();
return 0;
}

void ProcessLoop(uint8_t *Code, int &i, int &p, std::string &Result, int &p_in, int len, int indentLevel = 0)
{
std::string indent(indentLevel, '\t');

char Buf[256]{};
sprintf(Buf, "%swhile(d[p])\n%s{\n", indent.c_str(), indent.c_str());
Result += Buf;

int initial_p = p;
i++;
while (i < len && Code[i] != ']')
{
uint8_t CurrentCode = Code[i];
switch (CurrentCode)
{
case '>':
{
// printf("++p;");
int add{};
while (Code[i] == '>')
{
++add;
i++;
}
i--;
if (add != 0)
{
sprintf(Buf, "%s\tp += %d;\n", indent.c_str(), add);
Result += Buf;
// printf("++p;");
p += add;
}
break;
}
case '<':
{
// printf("--p;");
int sub{};
while (Code[i] == '<')
{
++sub;
i++;
}
i--;
if (sub != 0)
{
sprintf(Buf, "%s\tp -= %d;\n", indent.c_str(), sub);
Result += Buf;
// printf("++p;");
p -= sub;
}
break;
}
case '+':
{
int add{};
while (i < len && Code[i] == '+')
{
++add;
i++;
}
i--;
if (add != 0)
{
// sprintf(Buf, "%s\td[p] += %d;\n", indent.c_str(), add);
sprintf(Buf, "%s\td[p] += %d;\n", indent.c_str(), add);
Result += Buf;
}
break;
}
case '-':
{
int sub{};
while (i < len && Code[i] == '-')
{
++sub;
i++;
}
i--;
if (sub != 0)
{
// sprintf(Buf, "%s\td[%d] -= %d;\n", indent.c_str(), p, sub);
sprintf(Buf, "%s\td[p] -= %d;\n", indent.c_str(), sub);
Result += Buf;
}
break;
}
case ',':
{
// sprintf(Buf, "%s\td[%d] = in[%d];\n", indent.c_str(), p, p_in);
sprintf(Buf, "%s\td[p] = in[p_in];\n%s\t++p_in;\n", indent.c_str(), indent.c_str());
Result += Buf;
++p_in;
break;
}
case '[':
{
ProcessLoop(Code, i, p, Result, p_in, len, indentLevel + 1);
break;
}
case '.':
{
// sprintf(Buf, "%s\tif(d[%d]==\'0\')\n%s\t\{\n%s%s\t\treturn 0;\n%s\t\}\n%s\tif(d[%d]==\'1\')\n%s\t\{\n%s%s\t\treturn 1;\n%s\t\}\n", indent.c_str(), p, indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), p, indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str());
sprintf(Buf, "%s\tif(d[p]==\'0\')\n%s\t\{\n%s%s\t\tbreak;\n%s\t\}\n%s\tif(d[p]==\'1\')\n%s\t\{\n%s%s\t\tbreak;\n%s\t\}\n", indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str(), indent.c_str());
Result += Buf;
break;
}
default:
break;
}
i++;
}
sprintf(Buf, "%s}\n", indent.c_str());
Result += Buf;
}

int main()
{
int index = 0;
std::ifstream bfCodeFile("bf.txt");

uint8_t *Code = new uint8_t[45000];
if (!bfCodeFile.is_open())
{
delete[] Code;
return 0;
}

bfCodeFile.seekg(0, std::ios::end);
int len = bfCodeFile.tellg();
bfCodeFile.seekg(0, std::ios::beg);
bfCodeFile.read((char *)Code, len);

std::string Result;

int p = 0;
int p_in = 0;
char Buf[256]{};
for (int i = 0; i < len; i++)
{
uint8_t CurrentCode = Code[i];
switch (CurrentCode)
{
case '>':
{
int add{};
while (Code[i] == '>')
{
++add;
i++;
}
i--;
if (add != 0)
{
sprintf(Buf, "p += %d;\n", add);
Result += Buf;
// printf("++p;");
p += add;
}

break;
}
case '<':
{
int sub{};
while (Code[i] == '<')
{
++sub;
i++;
}
i--;
if (sub != 0)
{
sprintf(Buf, "p -= %d;\n", sub);
Result += Buf;
// printf("++p;");
p -= sub;
}
break;
}
case '+':
{
int add{};
while (Code[i] == '+')
{
++add;
i++;
}
i--;
if (add != 0)
{
// sprintf(Buf, "d[%d] += %d;\n", p, add);
sprintf(Buf, "d[p] += %d;\n", add);
Result += Buf;
}
break;
}
case '-':
{
int sub{};
while (Code[i] == '-')
{
++sub;
i++;
}
i--;
if (sub != 0)
{
// sprintf(Buf, "d[%d] -= %d;\n", p, sub);
sprintf(Buf, "d[p] -= %d;\n", sub);
Result += Buf;
}
break;
}
case ',':
{
// sprintf(Buf, "d[%d] = in[%d];\n", p, p_in);
sprintf(Buf, "d[p] = in[p_in];\n++p_in;\n");
Result += Buf;
++p_in;
break;
}
case '[':
{
ProcessLoop(Code, i, p, Result, p_in, len);
// 格式化注释
Result += "//" + std::to_string(index++) + "\n";
Result += "for(int count = 13;count<13+35;count++){printf(\"\%d,\",d[count]);}printf(\"\\n\");\n";
break;
}
case '.':
{
// sprintf(Buf, "if(d[%d]==\'0\')\n\{\n\treturn 0;\n\}\nif(d[%d]==\'1\')\n\{\n\treturn 1;\n\}\n", p, p);
sprintf(Buf, "if(d[p]==\'0\')\n\{\n\treturn 0;\n\}\nif(d[p]==\'1\')\n\{\n\treturn 1;\n\}\n");
Result += Buf;
break;
}
default:
break;
}
}
WriteToFile("C_Code.txt", Result);
END:
bfCodeFile.close();
delete[] Code;

return 0;
}

其实大家也可以直接去网上找脚本然后自己改,这里我添加了一些东西,我们在遍历完循环之后有一个数据的输出,为啥从13开始因为经过调试发现从13开始正好就是我们输入的值-‘a’,然后我又增加了行数注释,这样我们在调试我们生成的代码样本的时候可以全局搜索然后定位到具体的分析位置。

输出的C_code如下图:

然后我们直接运行这个程序,这里为啥选择xydefghijklm作为示例输入,稍后笔者会给出答案,输出结果如下图:

才1719行数据也不是很多,然后我们就可以注意到前12列,正好就是我们的示例输入-‘a’,这里为啥不用a,b这些,在笔者多次测试下00,01很容易混淆,所以笔者选择了xydefghijklm

我们接着分析这些数据,前面那些行很显然是可以直接删去的

然后我们一眼盯真,发现了类似下标值的东西,我们不确定继续往下面找,最终确定确实是下标值,那么我们是不是可以想成就是循环,然后每个循环之间还有一些00,其实可以删掉。

分离出每一个循环之后,我们发现每个循环的末尾都有一个值,比如下图这个就是F7,这里很显然就是cmp

那么我们看一下什么情况才是正确的情况,最后d[p]的值必须为’1’

我们在输出的C_code里面发现后面是有两个while循环的,但这两个while循环又是固定的两种情况,一种是+7,一种是+8,因此必须让它走第一个while循环才行

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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
while (d[p])
{
p += 1;
d[p] -= 1;
p += 1;
while (d[p])
{
d[p] -= 1;
}
p += 1;
while (d[p])
{
d[p] -= 1;
}
p -= 1;
p += 1;
d[p] += 7;
while (d[p])
{
p -= 1;
d[p] += 7;
p += 1;
d[p] -= 1;
}
p -= 1;
if (d[p] == '0')
{
break;
}
if (d[p] == '1')
{
break;
}
p -= 2;
while (d[p])
{
d[p] -= 1;
}
}
//1717
for (int count = 13; count < 13 + 35; count++) { printf("%02X ", d[count]); }printf("\n");
p += 1;
while (d[p])
{
p += 1;
while (d[p])
{
d[p] -= 1;
}
p += 1;
while (d[p])
{
d[p] -= 1;
}
p -= 1;
p += 1;
d[p] += 6;
while (d[p])
{
p -= 1;
d[p] += 8;
p += 1;
d[p] -= 1;
}
p -= 1;
if (d[p] == '0')
{
break;
}
if (d[p] == '1')
{
break;
}
p -= 1;
d[p] -= 1;
}
//1718
for (int count = 13; count < 13 + 35; count++) { printf("%02X ", d[count]); }printf("\n");
p -= 27;

回到我们之前分析的打印的数据那里这三列,第一列是我们自己经过加密后的数据,第二列是我们需要相等的数据(但是这个需要相等的数据不完全是打印出来的这个数字),需要我们去验证一下,因为我们所框的第二排数据是我们的密文减去我们加密的数据,这个数字是正确的,因此我们只需要用下面的数字加上我们自己输入的加密数据就可以得出密文,然后如果每一组对比正确的话第三排的第一列就会返回1

接下来我们就要分析每个循环里面的加密流程,他每个加密流程都是如下图这样,都是一个一个的方程组

然后手动提取方程组写个z3求解就行

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
from z3 import *

enc = [0xFD, 0xC7, 0xF8, 0x93, 0x9E, 0x66, 0xC0, 0xA9, 0xFF, 0xF3, 0xDC, 0xE5]
input = [BitVec(f"input{i}", 8) for i in range(12)]
s = Solver()
for i in range(12):
s.add(input[i] >=0, input[i] <= 26)
Temp =[0]*12
Temp[0]=0x03*input[0] + 0x03*input[1] + 0x03*input[2] + 0x03*input[3] + 0x01*input[4] + 0x01*input[5] + 0x03*input[7] + 0x02*input[10] +0x03*input[11]
Temp[1]=0x03*input[0] + 0x02*input[1] + 0x02*input[2] + 0x02*input[3] + 0x02*input[4] + 0x02*input[6] + 0x01*input[7] + 0x02*input[8]
Temp[2]=0x02*input[0] + 0x03*input[2] + 0x03*input[5] + 0x03*input[6] + 0x01*input[7] + 0x01*input[8] + 0x02*input[9] + 0x03*input[10]+ 0x01*input[11]
Temp[3]=0x02*input[2] + 0x03*input[6] + 0x02*input[7] + 0x03*input[8] + 0x02*input[10]
Temp[4]=0x01*input[0] + 0x02*input[1] + 0x02*input[2] + 0x01*input[3] + 0x02*input[5] + 0x01*input[8] + 0x02*input[10] + 0x01*input[11]
Temp[5]=0x03*input[1] + 0x03*input[5] + 0x02*input[6] + 0x02*input[10] + 0x01*input[11]
Temp[6]=0x01*input[0] + 0x01*input[1] + 0x03*input[2] + 0x01*input[5] + 0x02*input[6] + 0x02*input[7] + 0x02*input[8] + 0x02*input[9] + 0x01*input[10] + 0x02*input[11]
Temp[7]=0x03*input[0] + 0x02*input[1] + 0x02*input[2] + 0x02*input[4] + 0x01*input[5] + 0x02*input[8] + 0x01*input[10] + 0x01*input[11]
Temp[8]=0x03*input[0] + 0x03*input[1] + 0x03*input[2] + 0x03*input[3] + 0x01*input[4] + 0x02*input[5] + 0x02*input[6] + 0x02*input[9] + 0x02*input[11]
Temp[9]=0x01*input[0] + 0x01*input[1] + 0x02*input[3] + 0x02*input[4] + 0x02*input[5] + 0x02*input[6] + 0x02*input[7] + 0x02*input[8] + 0x03*input[10] + 0x01*input[11]
Temp[10]=0x03*input[1] + 0x02*input[2] + 0x01*input[5] + 0x01*input[6] + 0x02*input[7] + 0x03*input[8] + 0x03*input[9] + 0x03*input[10] + 0x01*input[11]
Temp[11]=0x03*input[0] + 0x03*input[1] + 0x03*input[3] + 0x01*input[4] + 0x02*input[5] + 0x03*input[6] + 0x02*input[7] + 0x01*input[9] + 0x02*input[10] + 0x03*input[11]

for j in range(12):
s.add(Temp[j] == enc[j])
if s.check() == sat:
m = s.model()
solution = [m.evaluate(input[i]).as_long() for i in range(12)]
Flag = [(v+0x61)&0xFF for v in solution]
flag = ''.join(chr(c) for c in Flag)
print("miniLCTF{"+flag+"}")
else:
print("No solution found")
# miniLCTF{favyxwekppoa}
  • Title: 记一次brainfuck逆向分析
  • Author: 5m10v3
  • Created at : 2025-05-09 00:00:00
  • Updated at : 2025-05-09 16:17:15
  • Link: https://redefine.ohevan.com/2025/05/09/记一次brainfuck逆向分析/
  • License: This work is licensed under CC BY-NC-SA 4.0.
Comments
On this page
记一次brainfuck逆向分析