-
-
[原创]BUUCTF-reverse-Universe_final_answer
-
发表于: 2022-4-18 22:42 8116
-
题目链接:https://buuoj.cn/challenges#[ACTF%E6%96%B0%E7%94%9F%E8%B5%9B2020]Universe_final_answer
先将文件用Die查看一下
是一个无壳的ELF64位文件,用IDA64打开文件,直接点进main函数,反编译一下,看到关键函数
可以看到关键的验证函数在sub_860函数里面,验证成功后又在sub_C50函数中进行了什么操作,最后输出flag,我们先跟进sub_860函数
这边可以用python的z3来解出这几个数
这里提一下z3的基本使用,安装方法网上很多这里就不多说了
大致流程如上,不过当问题有多个解的时候,z3只会输出一个解
也是一个加密的操作,不过建立在我们验证成功的基础上,也就是说这个地方我们可以通过动调来直接得到flag。
写exp的时候要注意两个地方,一个是原式中有两个z3解不了的移位的操作,需要将其转化成能识别的形式。还一个就是v1和v2的位置还有v6和v7是被调换过的,需要调回来
跑出的结果
将位置换一下,还有v1和v2的值,v6和v7的值对调一下,转成字符串
然后执行一下文件,输入我们跑出的字符串就可以得到flag
flag actf{F0uRTy_7w@_42}
,在buuctf上将actf换成flag就行
这题并不难就是看你细不细心了,还有一个就是意识到在第一个加密函数之前我们可以求到明文,不需要再去分析第二个加密的函数,虽然从结果看来这个函数不是加密,只是在尾部加了东西,但这个意识还是可以有的
__int64 __fastcall main(
int
a1, char
*
*
a2, char
*
*
a3)
{
char v4[
32
];
/
/
[rsp
+
0h
] [rbp
-
A8h] BYREF
char v5[
104
];
/
/
[rsp
+
20h
] [rbp
-
88h
] BYREF
unsigned __int64 v6;
/
/
[rsp
+
88h
] [rbp
-
20h
]
v6
=
__readfsqword(
0x28u
);
__printf_chk(
1LL
,
"Please give me the key string:"
, a3);
scanf(
"%s"
, v5);
if
( (unsigned __int8)sub_860(v5) )
{
sub_C50(v5, v4);
__printf_chk(
1LL
,
"Judgement pass! flag is actf{%s_%s}\n"
, v5);
}
else
{
puts(
"False key!"
);
}
return
0LL
;
}
__int64 __fastcall main(
int
a1, char
*
*
a2, char
*
*
a3)
{
char v4[
32
];
/
/
[rsp
+
0h
] [rbp
-
A8h] BYREF
char v5[
104
];
/
/
[rsp
+
20h
] [rbp
-
88h
] BYREF
unsigned __int64 v6;
/
/
[rsp
+
88h
] [rbp
-
20h
]
v6
=
__readfsqword(
0x28u
);
__printf_chk(
1LL
,
"Please give me the key string:"
, a3);
scanf(
"%s"
, v5);
if
( (unsigned __int8)sub_860(v5) )
{
sub_C50(v5, v4);
__printf_chk(
1LL
,
"Judgement pass! flag is actf{%s_%s}\n"
, v5);
}
else
{
puts(
"False key!"
);
}
return
0LL
;
}
bool
__fastcall sub_860(char
*
a1)
{
int
v1;
/
/
ecx
int
v2;
/
/
esi
int
v3;
/
/
edx
int
v4;
/
/
er9
int
v5;
/
/
er11
int
v6;
/
/
ebp
int
v7;
/
/
ebx
int
v8;
/
/
er8
int
v9;
/
/
er10
bool
result;
/
/
al
int
v11;
/
/
[rsp
+
0h
] [rbp
-
38h
]
v1
=
a1[
1
];
v2
=
*
a1;
v3
=
a1[
2
];
v4
=
a1[
3
];
v5
=
a1[
4
];
v6
=
a1[
6
];
v7
=
a1[
5
];
v8
=
a1[
7
];
v9
=
a1[
8
];
result
=
0
;
if
(
-
85
*
v9
+
58
*
v8
+
97
*
v6
+
v7
+
-
45
*
v5
+
84
*
v4
+
95
*
v2
-
20
*
v1
+
12
*
v3
=
=
12613
)
{
v11
=
a1[
9
];
if
(
30
*
v11
+
-
70
*
v9
+
-
122
*
v6
+
-
81
*
v7
+
-
66
*
v5
+
-
115
*
v4
+
-
41
*
v3
+
-
86
*
v1
-
15
*
v2
-
30
*
v8
=
=
-
54400
&&
-
103
*
v11
+
120
*
v8
+
108
*
v7
+
48
*
v4
+
-
89
*
v3
+
78
*
v1
-
41
*
v2
+
31
*
v5
-
(v6 <<
6
)
-
120
*
v9
=
=
-
10283
&&
71
*
v6
+
(v7 <<
7
)
+
99
*
v5
+
-
111
*
v3
+
85
*
v1
+
79
*
v2
-
30
*
v4
-
119
*
v8
+
48
*
v9
-
16
*
v11
=
=
22855
&&
5
*
v11
+
23
*
v9
+
122
*
v8
+
-
19
*
v6
+
99
*
v7
+
-
117
*
v5
+
-
69
*
v3
+
22
*
v1
-
98
*
v2
+
10
*
v4
=
=
-
2944
&&
-
54
*
v11
+
-
23
*
v8
+
-
82
*
v3
+
-
85
*
v2
+
124
*
v1
-
11
*
v4
-
8
*
v5
-
60
*
v7
+
95
*
v6
+
100
*
v9
=
=
-
2222
&&
-
83
*
v11
+
-
111
*
v7
+
-
57
*
v2
+
41
*
v1
+
73
*
v3
-
18
*
v4
+
26
*
v5
+
16
*
v6
+
77
*
v8
-
63
*
v9
=
=
-
13258
&&
81
*
v11
+
-
48
*
v9
+
66
*
v8
+
-
104
*
v6
+
-
121
*
v7
+
95
*
v5
+
85
*
v4
+
60
*
v3
+
-
85
*
v2
+
80
*
v1
=
=
-
1559
&&
101
*
v11
+
-
85
*
v9
+
7
*
v6
+
117
*
v7
+
-
83
*
v5
+
-
101
*
v4
+
90
*
v3
+
-
28
*
v1
+
18
*
v2
-
v8
=
=
6308
)
{
result
=
99
*
v11
+
-
28
*
v9
+
5
*
v8
+
93
*
v6
+
-
18
*
v7
+
-
127
*
v5
+
6
*
v4
+
-
9
*
v3
+
-
93
*
v1
+
58
*
v2
=
=
-
1697
;
}
}
return
result;
}
bool
__fastcall sub_860(char
*
a1)
{
int
v1;
/
/
ecx
int
v2;
/
/
esi
int
v3;
/
/
edx
int
v4;
/
/
er9
int
v5;
/
/
er11
int
v6;
/
/
ebp
int
v7;
/
/
ebx
int
v8;
/
/
er8
int
v9;
/
/
er10
bool
result;
/
/
al
int
v11;
/
/
[rsp
+
0h
] [rbp
-
38h
]
v1
=
a1[
1
];
v2
=
*
a1;
v3
=
a1[
2
];
v4
=
a1[
3
];
v5
=
a1[
4
];
v6
=
a1[
6
];
v7
=
a1[
5
];
v8
=
a1[
7
];
v9
=
a1[
8
];
result
=
0
;
if
(
-
85
*
v9
+
58
*
v8
+
97
*
v6
+
v7
+
-
45
*
v5
+
84
*
v4
+
95
*
v2
-
20
*
v1
+
12
*
v3
=
=
12613
)
{
v11
=
a1[
9
];
if
(
30
*
v11
+
-
70
*
v9
+
-
122
*
v6
+
-
81
*
v7
+
-
66
*
v5
+
-
115
*
v4
+
-
41
*
v3
+
-
86
*
v1
-
15
*
v2
-
30
*
v8
=
=
-
54400
&&
-
103
*
v11
+
120
*
v8
+
108
*
v7
+
48
*
v4
+
-
89
*
v3
+
78
*
v1
-
41
*
v2
+
31
*
v5
-
(v6 <<
6
)
-
120
*
v9
=
=
-
10283
&&
71
*
v6
+
(v7 <<
7
)
+
99
*
v5
+
-
111
*
v3
+
85
*
v1
+
79
*
v2
-
30
*
v4
-
119
*
v8
+
48
*
v9
-
16
*
v11
=
=
22855
&&
5
*
v11
+
23
*
v9
+
122
*
v8
+
-
19
*
v6
+
99
*
v7
+
-
117
*
v5
+
-
69
*
v3
+
22
*
v1
-
98
*
v2
+
10
*
v4
=
=
-
2944
&&
-
54
*
v11
+
-
23
*
v8
+
-
82
*
v3
+
-
85
*
v2
+
124
*
v1
-
11
*
v4
-
8
*
v5
-
60
*
v7
+
95
*
v6
+
100
*
v9
=
=
-
2222
&&
-
83
*
v11
+
-
111
*
v7
+
-
57
*
v2
+
41
*
v1
+
73
*
v3
-
18
*
v4
+
26
*
v5
+
16
*
v6
+
77
*
v8
-
63
*
v9
=
=
-
13258
&&
81
*
v11
+
-
48
*
v9
+
66
*
v8
+
-
104
*
v6
+
-
121
*
v7
+
95
*
v5
+
85
*
v4
+
60
*
v3
+
-
85
*
v2
+
80
*
v1
=
=
-
1559
&&
101
*
v11
+
-
85
*
v9
+
7
*
v6
+
117
*
v7
+
-
83
*
v5
+
-
101
*
v4
+
90
*
v3
+
-
28
*
v1
+
18
*
v2
-
v8
=
=
6308
)
{
result
=
99
*
v11
+
-
28
*
v9
+
5
*
v8
+
93
*
v6
+
-
18
*
v7
+
-
127
*
v5
+
6
*
v4
+
-
9
*
v3
+
-
93
*
v1
+
58
*
v2
=
=
-
1697
;
}
}
return
result;
}
x
=
Int
(
'x'
)
#声明整数
x
=
Real(
'x'
)
#声明实数
x
=
Bool
(
'x'
)
#声明布尔类型
a, b, c
=
Reals(
'a b c'
)
#批量声明
x
=
Int
(
'x'
)
#声明整数
x
=
Real(
'x'
)
#声明实数
x
=
Bool
(
'x'
)
#声明布尔类型
a, b, c
=
Reals(
'a b c'
)
#批量声明
x
=
Int
(
'x'
)
#变量
y
=
Int
(
'y'
)
s
=
Solver()
#创建一个通用求解器
s.add
=
(
2x
+
y
=
5
)
#约束条件
s.add
=
(x
*
y
=
3
)
if
s.check()
=
=
sat:
#检验是否有解
print
(s.model())
#输出解
else
:
print
(
"no result"
)
x
=
Int
(
'x'
)
#变量
y
=
Int
(
'y'
)
s
=
Solver()
#创建一个通用求解器
s.add
=
(
2x
+
y
=
5
)
#约束条件
s.add
=
(x
*
y
=
3
)
if
s.check()
=
=
sat:
#检验是否有解
print
(s.model())
#输出解
else
:
print
(
"no result"
)
unsigned __int64 __fastcall sub_C50(const char
*
a1, _BYTE
*
a2)
{
size_t v4;
/
/
rax
unsigned
int
v5;
/
/
edx
int
v6;
/
/
edi
int
v7;
/
/
ecx
__int64 v8;
/
/
r8
__int128
*
v9;
/
/
rsi
unsigned
int
v10;
/
/
ecx
int
v11;
/
/
eax
int
v12;
/
/
edi
int
v13;
/
/
edx
int
v14;
/
/
eax
_BYTE
*
v15;
/
/
rsi
_BYTE
*
v16;
/
/
rcx
_BYTE
*
v17;
/
/
r8
int
*
i;
/
/
rax
unsigned __int64 result;
/
/
rax
__int128 v20[
2
];
/
/
[rsp
+
0h
] [rbp
-
48h
] BYREF
__int64 v21;
/
/
[rsp
+
20h
] [rbp
-
28h
]
unsigned __int64 v22;
/
/
[rsp
+
28h
] [rbp
-
20h
]
v22
=
__readfsqword(
0x28u
);
v20[
0
]
=
0LL
;
v21
=
0LL
;
v20[
1
]
=
0LL
;
v4
=
strlen(a1);
v5
=
0
;
v6
=
9
;
while
( v5 < v4 )
{
v7
=
a1[v5
+
+
];
v6 ^
=
v7;
}
if
( v6 )
{
v8
=
0LL
;
v9
=
v20;
while
(
1
)
{
v9
=
(__int128
*
)((char
*
)v9
+
4
);
v10
=
v8
+
1
;
v11
=
v6
/
10
;
v12
=
v6
%
10
;
*
((_DWORD
*
)v9
-
1
)
=
v12;
LOBYTE(v13)
=
v12;
v6
=
v11;
if
( !v11 )
break
;
v8
=
v10;
}
v14
=
v8
-
1
;
v15
=
a2;
v16
=
&a2[v10];
v17
=
&a2[v8];
for
( i
=
(
int
*
)v20
+
v14; ;
-
-
i )
{
*
v15
=
v13
+
48
;
if
( v17
=
=
v15 )
break
;
v13
=
*
i;
+
+
v15;
}
}
else
{
v16
=
a2;
}
result
=
__readfsqword(
0x28u
) ^ v22;
*
v16
=
0
;
return
result;
}
unsigned __int64 __fastcall sub_C50(const char
*
a1, _BYTE
*
a2)
{
size_t v4;
/
/
rax
unsigned
int
v5;
/
/
edx
int
v6;
/
/
edi
int
v7;
/
/
ecx
__int64 v8;
/
/
r8
__int128
*
v9;
/
/
rsi
unsigned
int
v10;
/
/
ecx
int
v11;
/
/
eax
int
v12;
/
/
edi
int
v13;
/
/
edx
int
v14;
/
/
eax
_BYTE
*
v15;
/
/
rsi
赞赏记录
参与人
雪币
留言
时间
伟叔叔
为你点赞~
2023-3-18 03:06
一笑人间万事
为你点赞~
2022-7-27 23:39
小阿年
为你点赞~
2022-4-19 08:22
赞赏
他的文章
谁下载
看原图
赞赏
雪币:
留言: