小姐姐教你做CTF逆向题：利用符号执行技术和约束求解器

λ file release.strippedrelease.stripped: ELF 64-bit LSB shared object, ARM aarch64, version 1 (SYSV), dynamically linked, interpreter /system/bin/linker64, stripped

char flag[68];int fin; //校验状态int __cdecl main(int argc, const char **argv, const char **envp){//SNIP...scanf((const char *)&unk_3A08, &flag, envp);//scanf("%s",flag);v3 = sub_6B8();v4 = sub_73C(v3);v5 = sub_7C0(v4);v6 = sub_844(v5);v7 = sub_8C8(v6);v8 = sub_94C(v7);v9 = sub_9D0(v8);v10 = sub_A54(v9);v11 = sub_AD0(v10);v12 = sub_B54(v11);v13 = sub_BD0(v12);v14 = sub_C54(v13);v15 = sub_CD8(v14);v16 = sub_D5C(v15);v17 = sub_DE0(v16);v18 = sub_E64(v17);v19 = sub_EE8(v18);v20 = sub_F6C(v19);v21 = sub_FF0(v20);v22 = sub_1074(v21);v23 = sub_10F8(v22);v24 = sub_117C(v23);v25 = sub_1200(v24);v26 = sub_1284(v25);v27 = sub_1308(v26);v28 = sub_138C(v27);v29 = sub_1410(v28);v30 = sub_1494(v29);v31 = sub_1518(v30);v32 = sub_159C(v31);v33 = sub_1620(v32);v34 = sub_16A4(v33);v35 = sub_1720(v34);v36 = sub_17A4(v35);v37 = sub_1828(v36);v38 = sub_18AC(v37);v39 = sub_1930(v38);v40 = sub_19B4(v39);v41 = sub_1A38(v40);v42 = sub_1ABC(v41);v43 = sub_1B40(v42);v44 = sub_1BC4(v43);v45 = sub_1C48(v44);v46 = sub_1CCC(v45);v47 = sub_1D50(v46);v48 = sub_1DD4(v47);v49 = sub_1E58(v48);v50 = sub_1EDC(v49);v51 = sub_1F60(v50);v52 = sub_1FE4(v51);v53 = sub_2068(v52);v54 = sub_20EC(v53);v55 = sub_2170(v54);v56 = sub_21F4(v55);v57 = sub_2278(v56);v58 = sub_22FC(v57);v59 = sub_2380(v58);v60 = sub_2404(v59);v61 = sub_2488(v60);v62 = sub_250C(v61);v63 = sub_2590(v62);v64 = sub_2614(v63);v65 = sub_2698(v64);v66 = sub_271C(v65);v67 = sub_27A0(v66);sub_281C(v67);//flag正确时输出的fin值为0，否则为1printf((const char *)&unk_3A0B, (unsigned int)fin);//printf("%d",fin);return 0;}

void sub_6B8(){ fin = (unsigned __int8)flag * (unsigned __int8)flag - 203 * (unsigned __int8)flag != -10296 || (unsigned __int8)byte_1402E * (unsigned __int8)byte_1402E - 203 * (unsigned __int8)byte_1402E != -10296; // fin = (flag[0]*flag[0]-203*flag[0]!=-10296) || (flag[2]*flag[2]-203*flag[2]!=-10296)}

/*
* 提示：该行代码过长，系统自动注释不进行高亮。一键复制会移除系统注释 
* from z3 import *flag = [BitVec('flag[%d]'%i,8) for i in range(0,68)]s = Solver()# 添加约束：65*2个一元二次方程s.add(And((flag[0] * flag[0] - 203 * flag[0] == -10296),(flag[2] * flag[2] - 203 * flag[2] == -10296), (flag[1] * flag[1] - 204 * flag[1] == -10379), (flag[3] * flag[3] - 204 * flag[3] == -10379), (flag[2] * flag[2] - 204 * flag[2] == -10395), (flag[4]* flag[4] - 204 * flag[4] == -10395), (flag[3] * flag[3] - 216 * flag[3] == -11663), (flag[5] * flag[5] - 216 * flag[5] == -11663), (flag[4] * flag[4] - 154 * flag[4] == -5145), (flag[6] * flag[6] - 154 * flag[6] == -5145), (flag[5] * flag[5] - 165 * flag[5] == -6104), (flag[7] * flag[7] - 165 * flag[7] == -6104), (flag[6] * flag[6] - 172 * flag[6] == -6027), (flag[8] * flag[8] - 172 * flag[8] == -6027), (flag[7] * flag[7] - 95 * flag[7] == -2184), (flag[9] * flag[9] - 95 * flag[9] == -2184), (flag[8] * flag[8] - 210 * flag[8] == -10701), (flag[10] * flag[10] - 210 * flag[10] == -10701), (flag[9] * flag[9] - 87 * flag[9] == -1872), (flag[11] * flag[11] - 87 * flag[11] == -1872), (flag[10] * flag[10] - 174 * flag[10] == -7569), (flag[12] * flag[12] - 174 * flag[12] == -7569), (flag[11] * flag[11] - 143 * flag[11] == -4560), (flag[13] * flag[13] - 143 * flag[13] == -4560), (flag[12] * flag[12] - 206 * flag[12] == -10353), (flag[14] * flag[14] - 206 * flag[14] == -10353), (flag[13] * flag[13] - 206 * flag[13] == -10545), (flag[15] * flag[15] - 206 * flag[15] == -10545), (flag[14] * flag[14] - 238 * flag[14] == -14161), (flag[16] * flag[16] - 238 * flag[16] == -14161), (flag[15] * flag[15] - 206 * flag[15] == -10545), (flag[17] * flag[17] - 206 * flag[17] == -10545), (flag[16] * flag[16] - 238 * flag[16] == -14161), (flag[18] * flag[18] - 238 * flag[18] == -14161), (flag[17] * flag[17] - 143 * flag[17] == -4560), (flag[19] * flag[19] - 143 * flag[19] == -4560), (flag[18] * flag[18] - 238 * flag[18] == -14161), (flag[20] * flag[20] - 238 * flag[20] == -14161), (flag[19] * flag[19] - 143 * flag[19] == -4560),(flag[21] * flag[21] - 143 * flag[21] == -4560), (flag[20] * flag[20] - 206 * flag[20] == -10353),(flag[22] * flag[22] - 206 * flag[22] == -10353), (flag[21] * flag[21] - 206 * flag[21] == -10545),(flag[23] * flag[23] - 206 * flag[23] == -10545), (flag[22] * flag[22] - 174 * flag[22] == -7569),(flag[24] * flag[24] - 174 * flag[24] == -7569), (flag[23] * flag[23] - 206 * flag[23] == -10545),(flag[25] * flag[25] - 206 * flag[25] == -10545), (flag[24] * flag[24] - 208 * flag[24] == -10527),(flag[26] * flag[26] - 208 * flag[26] == -10527), (flag[25] * flag[25] - 143 * flag[25] == -4560),(flag[27] * flag[27] - 143 * flag[27] == -4560), (flag[26] * flag[26] - 238 * flag[26] == -14157),(flag[28] * flag[28] - 238 * flag[28] == -14157), (flag[27] * flag[27] - 143 * flag[27] == -4560),(flag[29] * flag[29] - 143 * flag[29] == -4560), (flag[28] * flag[28] - 221 * flag[28] == -12168),(flag[30] * flag[30] - 221 * flag[30] == -12168), (flag[29] * flag[29] - 147 * flag[29] == -4940),(flag[31] * flag[31] - 147 * flag[31] == -4940), (flag[30] * flag[30] - 222 * flag[30] == -12272),(flag[32] * flag[32] - 222 * flag[32] == -12272), (flag[31] * flag[31] - 103 * flag[31] == -2652),(flag[33] * flag[33] - 103 * flag[33] == -2652), (flag[32] * flag[32] - 213 * flag[32] == -11210),(flag[34] * flag[34] - 213 * flag[34] == -11210), (flag[33] * flag[33] - 160 * flag[33] == -5559),(flag[35] * flag[35] - 160 * flag[35] == -5559), (flag[34] * flag[34] - 147 * flag[34] == -4940),(flag[36] * flag[36] - 147 * flag[36] == -4940), (flag[35] * flag[35] - 225 * flag[35] == -12644),(flag[37] * flag[37] - 225 * flag[37] == -12644), (flag[36] * flag[36] - 156 * flag[36] == -5408),(flag[38] * flag[38] - 156 * flag[38] == -5408), (flag[37] * flag[37] - 211 * flag[37] == -11020),(flag[39] * flag[39] - 211 * flag[39] == -11020), (flag[38] * flag[38] - 219 * flag[38] == -11960),(flag[40] * flag[40] - 219 * flag[40] == -11960), (flag[39] * flag[39] - 202 * flag[39] == -10165),(flag[41] * flag[41] - 202 * flag[41] == -10165), (flag[40] * flag[40] - 164 * flag[40] == -5635),(flag[42] * flag[42] - 164 * flag[42] == -5635), (flag[41] * flag[41] - 215 * flag[41] == -11556),(flag[43] * flag[43] - 215 * flag[43] == -11556), (flag[42] * flag[42] - 157 * flag[42] == -5292),(flag[44] * flag[44] - 157 * flag[44] == -5292), (flag[43] * flag[43] - 161 * flag[43] == -5724),(flag[45] * flag[45] - 161 * flag[45] == -5724), (flag[44] * flag[44] - 203 * flag[44] == -10260),(flag[46] * flag[46] - 203 * flag[46] == -10260), (flag[45] * flag[45] - 140 * flag[45] == -4611),(flag[47] * flag[47] - 140 * flag[47] == -4611), (flag[46] * flag[46] - 143 * flag[46] == -4560),(flag[48] * flag[48] - 143 * flag[48] == -4560), (flag[47] * flag[47] - 198 * flag[47] == -9657),(flag[49] * flag[49] - 198 * flag[49] == -9657), (flag[48] * flag[48] - 135 * flag[48] == -4176),(flag[50] * flag[50] - 135 * flag[50] == -4176), (flag[49] * flag[49] - 206 * flag[49] == -10545),(flag[51] * flag[51] - 206 * flag[51] == -10545), (flag[50] * flag[50] - 206 * flag[50] == -10353),(flag[52] * flag[52] - 206 * flag[52] == -10353), (flag[51] * flag[51] - 143 * flag[51] == -4560),(flag[53] * flag[53] - 143 * flag[53] == -4560), (flag[52] * flag[52] - 230 * flag[52] == -13209),(flag[54] * flag[54] - 230 * flag[54] == -13209), (flag[53] * flag[53] - 167 * flag[53] == -5712),(flag[55] * flag[55] - 167 * flag[55] == -5712), (flag[54] * flag[54] - 206 * flag[54] == -10545),(flag[56] * flag[56] - 206 * flag[56] == -10545), (flag[55] * flag[55] - 238 * flag[55] == -14161),(flag[57] * flag[57] - 238 * flag[57] == -14161), (flag[56] * flag[56] - 206 * flag[56] == -10545),(flag[58] * flag[58] - 206 * flag[58] == -10545), (flag[57] * flag[57] - 167 * flag[57] == -5712),(flag[59] * flag[59] - 167 * flag[59] == -5712), (flag[58] * flag[58] - 230 * flag[58] == -13209),(flag[60] * flag[60] - 230 * flag[60] == -13209), (flag[59] * flag[59] - 143 * flag[59] == -4560),(flag[61] * flag[61] - 143 * flag[61] == -4560), (flag[60] * flag[60] - 206 * flag[60] == -10353),(flag[62] * flag[62] - 206 * flag[62] == -10353), (flag[61] * flag[61] - 206 * flag[61] == -10545),(flag[63] * flag[63] - 206 * flag[63] == -10545), (flag[62] * flag[62] - 135 * flag[62] == -4176),(flag[64] * flag[64] - 135 * flag[64] == -4176), (flag[63] * flag[63] - 198 * flag[63] == -9657),(flag[65] * flag[65] - 198 * flag[65] == -9657), (flag[64] * flag[64] - 87 * flag[64] == -1872),(flag[66] * flag[66] - 87 * flag[66] == -1872), (flag[65] * flag[65] - 212 * flag[65] == -10875),(flag[67] * flag[67] - 212 * flag[67] == -10875)))# 添加约束：flag格式为hackim18{''}for i in range(0,10): s.add(flag[i]==ord('hackim18{\''[i]))s.add(flag[66]==ord("'"))s.add(flag[67]==ord('}'))# 添加约束：flag只能包含数字、字母或下划线for i in range(10,66): s.add(And(Or(And(flag[i] >= ord('A'), flag[i] <= ord('Z')), And(flag[i] >= ord('a'), flag[i] <= ord('z')), And(flag[i] >= ord('0'), flag[i] <= ord('9')), flag[i] == ord('_'))))s.add(Or(flag[12]==ord('W'),flag[12]==ord('w')))# 找到满足的输入if s.check() == sat: m = s.model() r_flag = '' for i in range(0,68):  r_flag += chr(m[flag[i]].as_long().real) print r_flag# hackim18{'W0W_Wow_W0W_WoW_y0u_h4v3_m4th_sk1ll5_W0oW_W0owOwo0w_Wo0W'}
*/

#!/usr/bin/python## IDApython script to extract avoid address#function_list = [ 0x6B8, 0x73C, 0x7C0, 0x844, 0x8C8, 0x94C, 0x9D0, 0xA54, 0xAD0, 0xB54, 0xBD0, 0xC54, 0xCD8, 0xD5C, 0xDE0, 0xE64, 0xEE8, 0xF6C, 0xFF0, 0x1074, 0x10F8, 0x117C, 0x1200, 0x1284, 0x1308, 0x138C, 0x1410, 0x1494, 0x1518, 0x159C, 0x1620, 0x16A4, 0x1720, 0x17A4, 0x1828, 0x18AC, 0x1930, 0x19B4, 0x1A38, 0x1ABC, 0x1B40, 0x1BC4, 0x1C48, 0x1CCC, 0x1D50, 0x1DD4, 0x1E58, 0x1EDC, 0x1F60, 0x1FE4, 0x2068, 0x20EC, 0x2170, 0x21F4, 0x2278, 0x22FC, 0x2380, 0x2404, 0x2488, 0x250C, 0x2590, 0x2614, 0x2698, 0x271C, 0x27A0, 0x281C]base_addr = 0x400000avoid_lst = []for function in function_list: # mov W8, #1 addr = FindBinary(function, SEARCH_DOWN, "E8 03 00 32") if addr != BADADDR:  avoid_lst.append(addr)print ', '.join(["0x%x" % base_addr+addr for addr in avoid_lst])

avoid_lst = [0x400718,0x40079c,0x400820,0x4008a4,0x400928,0x4009ac,0x400a30,0x400aac,0x400b30,0x400bac,0x400c30,0x400cb4,0x400d38,0x400dbc,0x400e40,0x400ec4,0x400f48,0x400fcc,0x401050,0x4010d4,0x401158,0x4011dc,0x401260,0x4012e4,0x401368,0x4013ec,0x401470,0x4014f4,0x401578,0x4015fc,0x401680,0x4016fc,0x401780,0x401804,0x401888,0x40190c,0x401990,0x401a14,0x401a98,0x401b1c,0x401ba0,0x401c24,0x401ca8,0x401d2c,0x401db0,0x401e34,0x401eb8,0x401f3c,0x401fc0,0x402044,0x4020c8,0x40214c,0x4021d0,0x402254,0x4022d8,0x40235c,0x4023e0,0x402464,0x4024e8,0x40256c,0x4025f0,0x402674,0x4026f8,0x40277c,0x4027f8,0x40287c]

# coding: utf-8import angrmain_addr = 0x4028A0 # main函数入口find = 0x402A04 # main函数结束处flag_length = 68# 搜索时避开的路径avoid_lst = [ 0x400718,0x40079c,0x400820,0x4008a4,0x400928,0x4009ac,0x400a30,0x400aac, 0x400b30,0x400bac,0x400c30,0x400cb4,0x400d38,0x400dbc,0x400e40,0x400ec4, 0x400f48,0x400fcc,0x401050,0x4010d4,0x401158,0x4011dc,0x401260,0x4012e4, 0x401368,0x4013ec,0x401470,0x4014f4,0x401578,0x4015fc,0x401680,0x4016fc, 0x401780,0x401804,0x401888,0x40190c,0x401990,0x401a14,0x401a98,0x401b1c, 0x401ba0,0x401c24,0x401ca8,0x401d2c,0x401db0,0x401e34,0x401eb8,0x401f3c, 0x401fc0,0x402044,0x4020c8,0x40214c,0x4021d0,0x402254,0x4022d8,0x40235c, 0x4023e0,0x402464,0x4024e8,0x40256c,0x4025f0,0x402674,0x4026f8,0x40277c, 0x4027f8,0x40287c]p = angr.Project('release.stripped')state = p.factory.blank_state(addr=main_addr)# 约束：flag范围在可见字符内（32-127）for i in range(flag_length-2): c = state.posix.files[0].read_from(1) state.solver.add(state.solver.And(c <= '~', c >= 0))# 约束：flag最后两个字符为'}c = state.posix.files[0].read_from(1)state.solver.add(state.solver.And(c == "'"))c = state.posix.files[0].read_from(1)state.solver.add(state.solver.And(c == "}"))# 约束：flag最后以\x00作字符串结尾结束c = state.posix.files[0].read_from(1)state.solver.add(state.solver.And(c == "\x00"))# 重定位输入到开始处（0），且长度为68state.posix.files[0].seek(0)state.posix.files[0].length = 68ex = p.surveyors.Explorer(start=state, find=find, avoid=avoid_lst)ex.run()flag = ex._f.posix.dumps(0)print flag# hackim18{'W0W_Wow_W0W_WoW_y0u_h4v3_m4th_sk1ll5_W0oW_W0owOwo0w_Wo0W'}