首页
社区
课程
招聘
[翻译]在IDA中使用Python Z3库来简化函数中的算术运算
2018-6-20 22:32 12284

[翻译]在IDA中使用Python Z3库来简化函数中的算术运算

2018-6-20 22:32
12284

我在很早的时候就想接触基于SMT的程序分析,近日我开始了解这个方向。 这个方面有许多的框架,文章和教程,我会一点一点深入了解。

尽管我仍然在学习这部分内容,但无论如何我并不觉得这很先进或者很高大上,相反,它是非常基础的知识,Z3(来自Microsoft Research的一个定理证明的库)对于大部分初学者来说是十分简易的。 到目前为止,我所知道的除了来自Eric的Z3Py入门教材之外,还阅读Dennis Yurichev的文章"Quick introduction into SAT/SMT solvers and symbolic execution").

在上周的发表的博客中,我演示了在不运行的情况下如何编写基本模拟器来评估函数的返回值。 在本文中,我将展示如何将数千个算术运算从晦涩的x86汇编代码转换为月简易的Z3表达式,本文主要分为三个部分:

  • 简介
  • Z3库的快速上手
  • 将汇编转成Z3表达式
简介本文的测试程序和上周的测试程序很类似,由主函数调用的12个挑战函数。每个挑战函数都是随机生成的,因此它包含随eax、ebx 、ecx、edx寄存器(以及立即数)一起工作的add、sub、dec、inc指令的随机序列。示例程序在附件中可以下载。下面是第一个挑战函数的汇编代码:
//-------------------------------------------------------------------------
uint32_t challenge_1(uint32_t c1, uint32_t c2, uint32_t c3, uint32_t c4) // 1953 operation(s)
{
    uint32_t result;
    __asm
    {
        pushad
        mov eax, [c1]
        mov edx, [c2]
        mov ecx, [c3]
        mov ebx, [c4]
        sub eax, ebx
        inc ebx
        sub ebx, ecx
        sub ecx, 0x852e4867
        add ebx, ebx
        inc ecx
        add eax, edx
        add ecx, ebx
        sub ecx, ebx
        inc ecx
        sub ebx, edx
        add eax, 0x7a20f9e6
        add ebx, 0xaa5a1584
        add edx, edx
        sub ebx, 0x1ca0a567
        sub eax, 0xf94f7d8c
        inc ecx
        inc eax
        add edx, eax
        sub ebx, edx
        inc ebx
        sub edx, 0xd68a9fa7
        inc ebx
        inc eax
        inc eax
        .
        .
        ...1000+ instructions later...
        .
        sub ebx, edx
        inc eax
        sub ebx, edx
        sub ecx, eax
        add eax, ebx
        add ecx, 0xd2cb013d
        add ecx, 0xda9d6a2e
        add edx, eax
        sub edx, 0x25ebd85d
        add ebx, ebx
        add ebx, 0x936e2259
        inc eax
        add eax, ecx
        add ebx, 0xc0c1aa
        inc ebx
        add edx, 0x921ee6d5
        add edx, edx
        add ecx, eax
        add ecx, eax
        inc ebx
        sub ebx, edx
        add ebx, eax
        inc ebx
        sub eax, 0xd9d2f9c2
        add edx, eax
        inc ecx
        add ecx, 0xad2e6bb0
        add ecx, eax
        sub ecx, ebx
        add ebx, eax
        sub ecx, 0xe2786d0c
        add eax, ebx
        add eax, ecx
        add eax, edx
        mov dword ptr [result], eax
        popad
    }
    return result;
}


上面函数的汇编代码看起来很相似,分析不出什么东西,所以这里就不去分析了,直接使用F5大法查看伪代码:

int __cdecl challenge_1(unsigned int c1, unsigned int c2, unsigned int c3, unsigned int c4)
{
  unsigned int v4; // edx
  unsigned int v5; // ebx
  unsigned int v6; // ecx
  unsigned int v7; // eax
  int v8; // ecx
  int v9; // eax
  int v10; // edx
  int v11; // ebx
  int v12; // ecx
  int v13; // eax
  int v14; // ebx
  int v15; // edx
  int v16; // eax
  int v17; // ebx
  int v18; // ecx
  int v19; // edx
  int v20; // ecx
  int v21; // edx
  int v22; // eax
  int v23; // ebx
  int v24; // edx
  int v25; // eax
  int v26; // ecx
  int v27; // edx
  int v28; // ecx
  int v29; // edx
  int v30; // eax
  int v31; // ebx
  int v32; // ecx
  int v33; // eax
  int v34; // edx
  int v35; // ecx
  int v36; // ebx
  int v37; // edx
  int v38; // ecx
  int v39; // eax
  int v40; // ebx
  int v41; // ecx
  int v42; // eax
  int v43; // edx
  int v44; // ebx
  int v45; // ebx
  int v46; // edx
  int v47; // ecx
  int v48; // eax
  int v49; // edx
  int v50; // ebx
  int v51; // eax
  int v52; // edx
  int v53; // ebx
  int v54; // eax
  int v55; // edx
  int v56; // ecx
  int v57; // ecx
  int v58; // eax
  int v59; // edx
  int v60; // eax
  int v61; // ebx
  int v62; // eax
  int v63; // ebx
  int v64; // ecx
  int v65; // eax
  int v66; // edx
  int v67; // ecx
  int v68; // ebx
  int v69; // edx
  int v70; // ebx
  int v71; // edx
  int v72; // ecx
  int v73; // eax
  int v74; // ecx
  int v75; // edx
  int v76; // ebx
  int v77; // edx
  int v78; // edx
  int v79; // eax
  int v80; // ebx
  int v81; // ecx
  int v82; // ebx
  int v83; // eax
  int v84; // ebx
  int v85; // edx
  int v86; // ebx
  int v87; // eax
  int v88; // edx
  int v89; // ecx
  int v90; // eax
  int v91; // edx
  int v92; // ebx
  int v93; // ecx
  int v94; // ebx
  int v95; // eax
  int v96; // ecx
  int v97; // ecx
  int v98; // ebx
  int v99; // ecx
  int v100; // eax
  int v101; // edx
  int v102; // ebx
  int v103; // edx
  int v104; // edx
  int v105; // ecx
  int v106; // eax
  int v107; // ecx
  int v108; // edx
  int v109; // eax
  int v110; // edx
  int v111; // eax
  int v112; // ebx
  int v113; // ecx
  int v114; // edx
  int v115; // eax
  int v116; // edx
  int v117; // ecx
  int v118; // ebx
  int v119; // eax
  int v120; // ecx
  int v121; // edx
  int v122; // edx
  int v123; // eax
  int v124; // edx
  int v125; // ebx
  int v126; // eax
  int v127; // edx
  int v128; // ecx
  int v129; // ebx
  int v130; // edx
  int v131; // ebx
  int v132; // ecx
  int v133; // ebx
  int v134; // ebx
  int v135; // eax
  int v136; // ecx
  int v137; // ebx
  int v138; // ebx
  int v139; // edx
  int v140; // ecx
  int v141; // ebx
  int v142; // eax
  int v143; // ecx
  int v144; // ebx
  int v145; // edx
  int v146; // ebx
  int v147; // edx
  int v148; // ecx
  int v149; // eax
  int v150; // ebx
  int v151; // ecx
  int v152; // ebx
  int v153; // edx
  int v154; // eax
  int v155; // edx
  int v156; // ebx
  int v157; // edx
  int v158; // ebx
  int v159; // ecx
  int v160; // ebx
  int v161; // eax
  int v162; // ecx
  int v163; // ebx
  int v164; // edx
  int v165; // eax
  int v166; // ecx
  int v167; // eax
  int v168; // edx
  int v169; // ebx
  int v170; // ecx
  int v171; // eax
  int v172; // ecx
  int v173; // ebx
  int v174; // ecx
  int v175; // edx
  int v176; // ebx
  int v177; // ebx
  int v178; // eax
  int v179; // edx
  int v180; // ecx
  int v181; // eax
  int v182; // edx
  int v183; // eax
  int v184; // eax
  int v185; // ebx
  int v186; // ecx
  int v187; // ebx
  int v188; // edx
  int v189; // ecx
  int v190; // ebx
  int v191; // eax
  int v192; // ecx
  int v193; // eax
  int v194; // edx
  int v195; // ecx
  int v196; // edx
  int v197; // ecx
  int v198; // eax
  int v199; // edx
  int v200; // eax
  int v201; // ecx
  int v202; // ebx
  int v203; // eax
  int v204; // ebx
  int v205; // eax
  int v206; // ecx
  int v207; // edx
  int v208; // ebx
  int v209; // eax
  int v210; // edx
  int v211; // eax
  int v212; // eax
  int v213; // ecx
  int v214; // ebx
  int v215; // edx
  int v216; // ecx
  int v217; // edx
  int v218; // ebx
  int v219; // eax
  int v220; // ecx
  int v221; // eax
  int v222; // ebx
  int v223; // eax
  int v224; // ecx
  int v225; // ecx
  int v226; // ebx
  int v227; // eax
  int v228; // ebx
  int v229; // ecx
  int v230; // edx
  int v231; // eax
  int v232; // ecx
  int v233; // edx
  int v234; // ecx
  int v235; // edx
  int v236; // edx
  int v237; // ecx
  int v238; // eax
  int v239; // ebx
  int v240; // edx
  int v241; // ebx
  int v242; // edx
  int v243; // ebx
  int v244; // eax
  int v245; // ecx
  int v246; // eax
  int v247; // edx
  int v248; // eax
  int v249; // ebx
  int v250; // ecx
  int v251; // eax
  int v252; // ecx
  int v253; // ebx
  int v254; // ecx
  int v255; // edx
  int v256; // eax
  int v257; // edx
  int v258; // ecx
  int v259; // eax
  int v260; // edx
  int v261; // ebx
  int v262; // ecx
  int v263; // ecx
  int v264; // eax
  int v265; // edx
  int v266; // eax
  int v267; // ecx
  int v268; // ebx
  int v269; // edx
  int v270; // eax
  int v271; // ebx
  int v272; // edx
  int v273; // eax
  int v274; // ecx
  int v275; // ebx
  int v276; // ecx
  int v277; // eax
  int v278; // edx
  int v279; // ecx
  int v280; // edx
  int v281; // eax
  int v282; // ecx
  int v283; // ebx
  int v284; // eax
  int v285; // edx
  int v286; // ebx
  int v287; // eax
  int v288; // ecx
  int v289; // eax
  int v290; // ebx
  int v291; // eax
  int v292; // ecx
  int v293; // ebx
  int v294; // edx
  int v295; // eax
  int v296; // ebx
  int v297; // ecx
  int v298; // edx
  int v299; // ebx
  int v300; // eax
  int v301; // ebx
  int v302; // eax
  int v303; // ebx
  int v304; // edx
  int v305; // eax
  int v306; // ecx
  int v307; // eax
  int v308; // ebx
  int v309; // ecx
  int v310; // ebx
  int v311; // ecx
  int v312; // ebx
  int v313; // ecx
  int v314; // edx
  int v315; // eax
  int v316; // edx
  int v317; // ebx
  int v318; // ecx
  int v319; // eax
  int v320; // edx
  int v321; // ebx
  int v322; // ecx
  int v323; // edx
  int v324; // ebx
  int v325; // edx
  int v326; // eax
  int v327; // edx
  int v328; // ebx
  int v329; // eax
  int v330; // eax
  int v331; // eax
  int v332; // edx
  int v333; // ebx
  int v334; // eax
  int v335; // ecx
  int v336; // ebx
  int v337; // ecx
  int v338; // eax
  int v339; // ecx
  int v340; // ebx
  int v341; // ecx
  int v342; // eax
  int v343; // ecx
  int v344; // eax
  int v345; // ebx
  int v346; // eax
  int v347; // eax
  int v348; // ecx
  int v349; // eax
  int v350; // ecx
  int v351; // ebx
  int v352; // edx
  int v353; // eax
  int v354; // ecx
  int v355; // ebx
  int v356; // edx
  int v357; // ebx
  int v358; // edx
  int v359; // eax
  int v360; // ebx
  int v361; // edx
  int v362; // ecx
  int v363; // eax
  int v364; // ebx
  int v365; // ecx
  int v366; // ebx
  int v367; // ecx
  int v368; // ebx
  int v369; // ecx
  int v370; // edx
  int v371; // eax
  int v372; // edx
  int v373; // ecx
  int v374; // eax
  int v375; // edx
  int v376; // ecx
  int v377; // ebx
  int v378; // eax
  int v379; // edx
  int v380; // ebx
  int v381; // edx
  int v382; // ebx
  int v383; // edx
  int v384; // eax
  int v385; // ebx
  int v386; // edx
  int v387; // ecx
  int v388; // eax
  int v389; // edx
  int v390; // ecx
  int v391; // ebx
  int v392; // edx
  int v393; // eax
  int v394; // ecx
  int v395; // ebx
  int v396; // edx
  int v397; // ecx
  int v398; // edx
  int v399; // eax
  int v400; // ecx
  int v401; // eax
  int v402; // ebx
  int v403; // ecx
  int v404; // eax
  int v405; // edx
  int v406; // ebx
  int v407; // eax
  int v408; // ecx
  int v409; // edx
  int v410; // ebx
  int v411; // ebx
  int v412; // ecx
  int v413; // eax
  int v414; // ebx
  int v415; // ecx
  int v416; // edx
  int v417; // ecx
  int v418; // ebx
  int v419; // eax
  int v420; // ecx
  int v421; // eax

  v4 = c2 + c1 - c4 - 2133754790 + 1 + 2 * c2 - 1785093898;
  v5 = 2 * (c4 + 1 - c3)- c2- 1917226979- (c2+ c1 - c4 - 2133754790+ 2 * c2)+ 2- (c3+ 539193617)- v4- 350898193;
  v6 = c3 + 539193617 - v5 - 879839410;
  v5 += 2;
  v6 += 3;
  v4 += 2109602273;
  v7 = 2 * (2 * (c2 + c1 - c4 - 2133754790 + 3 - (c3 + 539193617) - 1164434189 - v5 - v6) + 1);
  v8 = 2 * v6 - 1873426435 - v7;
  v9 = v7 - v4 + 1;
  v10 = v4 - 971527202 + 730640080;
  v11 = v5 + 1150557381 - v10 - 1412696239 + 1;
  v12 = v11 + v8 - 396431529 + 1;
  v13 = v9 + 2 - v12 + 1;
  v14 = v12 + v11 + 1;
  v15 = v10 + 204474460 - v13 - 1432203755;
  v16 = v14 + v13 + 884313224 + 813147417;
  v17 = v15 + v14 + 2;
  v18 = v15 + v12 - 451236562 + 3;
  v19 = v16 + v15 + 1;
  v17 += 138511611;
  v16 += 953411192;
  v20 = v16 + v18;
  v21 = v17 + 2 * (v19 + 1) + 119463169;
  v17 -= 738693819;
  v22 = v16 + 594867870 - v17 + 1413353867;
  v23 = v17 - v22;
  v22 += 520753425;
  v24 = v22 + v21 + 144745048;
  v25 = v24++ + v22 - 1828520841 + 1;
  v26 = v20 + 3 - v24;
  v27 = v24 - v26;
  v28 = v27 + v26 + 763465995;
  v29 = 2 * (v27 + 2);
  v30 = v29 + v25 + 1017115747;
  v31 = v23 - 879256061 + 1336943267 - v30;
  v32 = v30 + v30 + v28 + 1689547303 - 1018772533 + 1;
  v33 = v30 - v31 + 1;
  v34 = v31 + v29 - v33 + 909973850;
  v35 = v34 + v32 + 228062414;
  v36 = v35 + v31 + 347278668;
  v35 -= 720946967;
  v37 = 2 * (v34 + 1 - v35);
  v38 = v37 + v35 + 1;
  v37 += 1888994439;
  v39 = 2 * (v33 + 579771010) + 2103615418;
  v40 = v36 - 276265002 - v37 + 1864035437;
  v41 = v38 + 1 - v39;
  v37 += 1786144130;
  v42 = v39 + 1600574700 - v37;
  v43 = v37 - v40;
  v44 = v43 + v40 - v41 + 2105473564;
  v41 *= 2;
  v45 = 2 * (v44 - v41);
  v46 = v43 - 1150894576 + 3;
  v47 = v45 + v41 + 313221810 - v46 + 807301504;
  v48 = v42 - 124125674 + 1 - v46 + 1 - v46 + 1;
  v49 = v48 + v46;
  v50 = v49 + v45 - 468305613 + 3 - 2100928955;
  v51 = 2 * (v48 - v49 - ++v47) + 1;
  v52 = v49 + 1 - v47++ + 3;
  v53 = v52 + v50;
  v54 = v51 - v53;
  v55 = v52 - v47 + 1;
  v53 -= 446157988;
  v54 += 1553282976;
  v56 = v54 + v53 + v47 + 1;
  v53 *= 2;
  v57 = v53 + v56 - 1230516346 + 1 + 1205548791;
  v58 = v54 - v53 + 2128637547;
  v59 = v58 + v55 + 1;
  v60 = v58 - v57;
  v57 += 377513439;
  v61 = v53 - 799999952 - v57;
  v62 = v61 + v60 + 1;
  v63 = v61 - v57;
  v59 += 848132728;
  v64 = v57 - v63 - v59;
  v65 = v59 + v62 - 2142680737 + 1764150285;
  v63 += 2087876122;
  v66 = v59 + 1814013069 - v63 - v64;
  v67 = 2 * v64 - v65 + 1132472947;
  v68 = v63 - 788948114 + 1 - v67;
  v69 = v68 + v68 + v66 + 1553607352;
  v67 += 2;
  v70 = v69 + 2 * v68 + 1518868433;
  v71 = v67 + v67 + v69 - v70;
  v72 = v70 + v67;
  v70 += 713535814;
  v73 = 2 * v65 + 1429126951 - v70;
  v70 -= 173942082;
  v74 = v70 + v72 - 1888550847 + 1 - 394102299;
  v75 = v71 + 256237465 - v74;
  v76 = v75 + v70 + 1;
  v77 = v75 - v74++;
  v76 += 2140073780;
  v78 = 2 * (v77 - 1454905092) - 1933992509;
  v79 = v76 + 2 * (v73 + 1866717529) - v74 - 1310766122 - v78;
  v80 = v76 - v74;
  v81 = v80 + v74;
  v82 = v79 + v80;
  ++v81;
  v83 = v82 + v79 + 1;
  v78 += 1083862846;
  v84 = v82 + 1 - v81 - v78;
  v85 = v81 + v78;
  v81 -= 614253581;
  v86 = v85 + v84 - 515607244 + 238772881;
  v87 = v83 + 141351837 - v81 + 1;
  v88 = v86++ + v85 - 543286513 + 1674408964 - 794464384;
  v89 = v81 - 623767744 + 215241888;
  v90 = 2 * (v89++ + v87 + 1710998538);
  v91 = v86 + v86 + v88 + 1 + 1 - v89++;
  v92 = v89 + v86;
  v90 -= 885178085;
  v91 += 1677704898;
  v93 = v90++ + v89 - 940635716;
  v94 = v92 + 1 - v90;
  v95 = v91 + v90 + 1 + 1841924206;
  v96 = v91 + v93 + 941760921;
  v91 += 2;
  v97 = v96 + 1 - v91 + 1530834091;
  v98 = v94 - v97 + 1;
  v99 = v95 + v97 + 1699993484;
  v100 = v98 + v95 + 1;
  v101 = v98 + v91 - 523060265 + 1789589531;
  v102 = v98 + 1281582157 - v100;
  v100 += 146514254;
  v103 = v101 - v99 - v100++;
  v99 += 2080302551;
  v104 = 2 * (v99 + v103 + 1512882559 + 1);
  v105 = v99 - v100;
  v104 -= 784717007;
  v106 = v104++ + v100 - 1584810020 + 2;
  v107 = v104 + v105 + 1;
  v106 += 1065502423;
  v102 += 3;
  v108 = v102 + v104 - v107 - v106 + 342809982;
  v107 -= 1412780444;
  v109 = v108 + v106 + 1 - 858330204;
  v110 = v109 + v108;
  v102 -= 664953144;
  v111 = v109 - 1329716196 - v102;
  v112 = v102 - v107;
  v111 += 1373514701;
  v113 = v107 - 1346592359 + 216683527 - v111;
  v114 = v111 + v110 - 288276575 + 1500011784;
  v115 = v113 + v111;
  v116 = v115++ + v114;
  v117 = 2 * (v113 - 1163128426);
  v118 = v117 + v112 - 818961183 - v115 - 593940334;
  v119 = v118 + v115 + 2;
  v118 += 428412235;
  v120 = v117 + 3 - v118;
  v121 = v116 + 4 - v118 + 1;
  v118 += 894601604;
  v122 = v118 + v121;
  v123 = v122 + v119 + 1 + 443477999;
  v124 = v123 + v122;
  v125 = 2 * v118 - v123;
  v126 = v124 + v123 - 2061231162;
  v127 = v124 - v125;
  v128 = v126 + v120 + 1485909680 + 1483310720;
  v129 = v128 + v127 + v125 - 1355157173 + 1;
  v130 = v128 + v127;
  v128 += 2;
  v131 = v129 - v128;
  v130 += 1683851829;
  v132 = v128 - v131 - 354913611;
  v133 = v131 - v132;
  v132 -= 198220312;
  v134 = v133 + 172443045 - v132;
  v135 = v126 + 3 - v132 - v134;
  v136 = v130 + 2 * (v132 - v134) - v135 + 471821392;
  v137 = v130++ + v134 - v136;
  v136 += 923861112;
  v138 = v130 + 2 * (v137 + 1) + 1 - 1146928935 + 1 - v136;
  v139 = v138 + 2 * v130 + 1;
  v140 = v136 - 1156737329 - v138 + 2 - v138 - v139;
  v141 = v140 + v138 + 1;
  v142 = v135 - 608570200 + 1 - v141 + 1;
  v139 += 2;
  v143 = v140 - 1777203220 + 1;
  v144 = v139 + v141 - v142 - 440487739 + 182778494 - v143;
  v145 = v139 + 966597185 - v144;
  v142 += 967980219;
  v146 = v144 - 1652140998 + 1;
  v147 = v142 + v145 - 1363945608 + 1 - v146;
  v148 = v143 - v146 + 1350186086;
  v149 = 2 * (v148 + 2 * v142);
  v150 = v146 + 1 - v147 - 457990213;
  v151 = v148 + 1 - v150;
  v152 = v150 - 504705392 + 1;
  v153 = v147 + 1193758906 - v152;
  v154 = v149 + 1 - v152 + 144039938 - v153;
  v155 = v154 + v153;
  v154 += 2;
  v156 = v152 + 2078215581 - v154 + 1;
  v157 = v156 + v155 - 122946150 + 301662336;
  v158 = v156 - v157;
  v154 += 2;
  v159 = v157++ + v158 + v151 - 958001904 + 1284137460 + 1;
  v160 = v154 + v158 + 1002156873 - v157 + 170108160;
  v161 = v154 - 1014383826 + 161227700;
  v162 = v159 - v161;
  v163 = v160 - 255510393 + 376777367;
  v164 = v157 - v162 + 2;
  v165 = v163 + v161 - 1912551381 + 1;
  v166 = v165 + v162 - v163 + 1 + 1;
  v167 = v166 + v165 + 1;
  v168 = v163 + v164 + 201934410 + 968132783;
  v169 = v163 - v168++;
  v170 = v166 - v167;
  v171 = v168 + v167;
  v172 = v170 - v168;
  v168 += 2029379458;
  v173 = v168 + v169 - 1763166604 + 1 + 1;
  v171 -= 1188417209;
  v174 = v172 + 1 - v173 + 1;
  v175 = v174 + v168 + 2140747580 - v171 + 668304081;
  v176 = v173 - 26185106 + 474549714 - v174++;
  v177 = v176 - v174;
  v178 = v175 + v171 + 1;
  v179 = v178 + v175;
  v180 = v178 + v177 + v174 + 1 + 2141394379;
  v181 = v178 - 826788372 + 3;
  v182 = v181 + v179 + 1;
  v177 += 741838009;
  v183 = v177 + v181;
  v177 *= 2;
  v184 = v183 - 238554347 - v177 + 932383584;
  v185 = v184 + v177 + 2100277479;
  v186 = v185 + v180 + 54142085 - v182 - 1632592373;
  v187 = v185 - v184 + 579181258;
  v188 = 2 * (v182 + 1383200762) + 1;
  v189 = v187 + v188 + v186 - v184 + 1 + 1172965920 + 1;
  v190 = v187 - 101123714 - v189 + 1 - v189 - 96237627;
  v188 += 2;
  v191 = 2 * (v189 + v184 - 207227160 + 4) + 1;
  v192 = v191 + v189 - v188;
  v190 += 4;
  v193 = v191 - 1353895842 + 1;
  v194 = v190 + v188 + 2123750079 - v193;
  v190 += 1696689707;
  v195 = 2 * (v192 + 1 - v190);
  v196 = v194 + 1 - v195 - 78101511;
  v190 += 540662868;
  v197 = v190 + v195 - 1145799797 - v196;
  v198 = 2 * (v193 - 185780694) + 1;
  v199 = v198 + v196;
  v190 += 1255424563;
  v200 = 2 * (v199 + v198) - 1727929676;
  v199 += 2;
  v201 = v190 + v199 + v197;
  v202 = v190 - 1214148504 + 1;
  v199 += 401187067;
  v203 = v200 - 1564098266 + 917389966 - v202 - 1198776331 + 1 - v199;
  v204 = v201 + v202 + 2 - v203;
  v205 = v203 - 318781264 - v199 - 1605668317 + 2;
  v206 = 2 * (v201 + 1844554225) - 1604774369;
  v207 = 2 * (v205 + v199 + 790825996 - v206) + 1650229900;
  v208 = v204 - 490598907 + 1;
  v206 += 282040833;
  v209 = v206 + v205 - 2006766853 - v208;
  v206 += 2;
  v210 = v207 + 1511399432 - v208 - 1551102207;
  v211 = v206 + v206 + v209 - v210 - v208;
  v206 += 1215172648;
  v210 -= 959608047;
  v212 = v211 + 1 - v206;
  v213 = v206 - v212 - v210;
  v214 = v212 + v208 + 1869175045 - v213 - 1424027273;
  v215 = v210 + 1620160695 - v214;
  v216 = v214 + v214 + v213 - v215 - 1065981445;
  v217 = 2 * (v215 - 1244977230) + 1747029779;
  v216 -= 1257866941;
  v218 = v214 + 2143814783 - v216 - 1398907650;
  v219 = 2 * v212 + 2 - v217++;
  v220 = v219 + v216 + 1 - v218 + 1 - v217 - v217;
  v221 = v219 - v217++;
  v222 = v218 - 1855122676 + 1;
  v223 = v222 + v221 + 2;
  v224 = v223 + v217 + v220 - 1317237096;
  v217 += 2;
  v225 = v222 + v224;
  v226 = v222 - v225 - 777710099;
  v227 = v223 - 730911683 - v226;
  v228 = v227 + v226 + 1;
  v229 = v217 + v227 + v225 - 1217941265;
  v230 = v217 - v228;
  v231 = v230 + v228 + v227 - 1682643877;
  v228 += 2;
  v232 = v230 + v229 + 1938596261 + 1 - v228;
  v228 += 584042825;
  v233 = v230 - 2139100084 + 2;
  v234 = v233 + v232 + 1;
  v235 = 2 * (v228 + v233) + 1;
  v228 += 1437309881;
  v236 = v228 + v234 + v235 + 1 + 1;
  v228 -= 716828805;
  v237 = 2 * (v234 + 1 - v228) - 685322476;
  v238 = v236 + v231 - 1381742058 + 1995963757 + 2;
  v239 = v228 - 1516409973 + 1147924830;
  v240 = v236 + 1 - v238 - v239 - 2104005844;
  v241 = v239 + 1 - v240;
  v238 -= 759057394;
  v242 = v240 - v238;
  v238 -= 623914540;
  v243 = v241 - v238;
  v244 = v238 - v243;
  v243 += 237287396;
  v245 = v243 + 2 * (v237 + 1002096745) - 2048248416 + 1892930438;
  v246 = 2 * v244 + 1294486749;
  v247 = v242 + 1612687194 - v243 - 660996117 - v246;
  v248 = v247 + v246 + 720558110;
  v247 += 977714025;
  v248 -= 1491378659;
  v249 = v243 + 1945659396 - v247;
  v250 = v245 + 1 - v248;
  v251 = v249 + v248 + 1185773403;
  v252 = v250 - v249 + 1;
  v253 = v251 + v249 + 401286047;
  v254 = v252 - 998849865 + 1;
  v255 = 2 * v247 + 754645442 - v254;
  v256 = v251 - 1424315697 + 2 - v255;
  v257 = v255 - v256;
  v256 -= 1309666088;
  v258 = v256 + v254 - v253;
  v259 = v256 + 1 - v253 - 2033562943;
  v260 = v257 + 1650643934 - v259 - 1415290431;
  v261 = v260++ + v253 + 524627955;
  v262 = v260 + v258 + 2013559893;
  v260 -= 824578413;
  v261 -= 446217575;
  v263 = v262 + 508608480 - v261 + 1345436449;
  v264 = v259 + 1403184861 - v260 + 1284484219;
  v265 = v263 + v260;
  v263 -= 242016614;
  v266 = v264 + 1347235185 - v263;
  v267 = v266 + v263 + 1 + 787180614;
  v266 += 606099305;
  v268 = 2 * (v261 + 520953472) + 165941725;
  v269 = v268 + v265 - 1534490202 - v266 + 1;
  v267 += 2120509468;
  v270 = v266 + 689980400 - v269 - 2044475833 - v269;
  v269 -= 1625687532;
  v271 = v268 + 1 - v269 + 1;
  v272 = v270 + v269 + 1252726713;
  v273 = v270 - v267 + 1;
  v274 = 2 * v267 - v271 + 1;
  v272 += 531933468;
  v275 = v271 - v274 - v274 + 2039136993;
  v276 = v274 - v272;
  v277 = v273 - 1600087378 + 1;
  v278 = v275 + 2 * (v272 + 1);
  v279 = v276 + 2 - v278;
  v280 = v277 + v278;
  ++v275;
  v281 = v277 - 1762733020 - v279 + 1;
  v280 += 1278825738;
  v282 = v279 + 147538177 - v275;
  v283 = v275 - v281;
  v284 = v281 + 693844065 - v280;
  v285 = v280 - ++v282;
  v286 = v282 + v283 + 1 - v284;
  v287 = v284 - v285 - 74089317;
  v288 = v282 - v287 - v286 - 681820438;
  v289 = v287 - 1256120859 + 149723392 - v288;
  v290 = v286 - 1421591606 - v289 + 2;
  v285 += 1989232579;
  v291 = v289 + 1 - v290;
  v292 = 2 * (v288 - 685621057) + 1;
  v293 = v290 - v291 - v285;
  v294 = v285 - v292;
  v295 = v291 - 1661767175 + 42969351;
  v296 = v294 + v294 + v293 - 1972384502 + 2 - 1576459347 + 1;
  v297 = v295 + v292 - 396668767 - 1534437557;
  v298 = v296 + v294 - 1645192742 - v295 - 1479631423 + 2 - 331301694;
  v299 = v296 - 106622097 + 668588646;
  v300 = 2 * (v299 + v297 + v295 + 1 + 2) - 1263581112;
  v297 += 1979779660;
  v301 = v297 + v300 + v299 + 1343345468 + 481569519;
  v298 += 861842343;
  v302 = v298 + v300 - 1650922112 + 1803040625 - 1103549091 + 1;
  v303 = v298 + v301 - 263499248;
  v304 = v303 + v298;
  v305 = v304++ + v302 - 438171503;
  v306 = v297 - 2076009387 + 1524090740 - v304 + 1;
  v304 += 575953311;
  v307 = v305 + 1306759242 - v306;
  v308 = v303 - 429496975 + 1812284714 - v307++;
  v309 = 2 * (v306 + 1523384106) - 1468869015;
  v310 = v304 + v308 + 1260443893 - v309;
  v311 = v309 - 1158775838 - v307++;
  v312 = 2 * v310 - 441360349;
  v313 = v311 - v312;
  v314 = v313++ + v307 + v304 - 1384238736;
  v315 = 2 * v307 - v313 + 496097820;
  v316 = v315 + v314 + 2 + 1;
  v315 += 3;
  v317 = 2 * (2 * v312 + 3 - v316 + 2070720611) - 1285251516 + 88029981;
  v318 = v315 + v313 - 1389710860;
  v319 = v315 - v318;
  v320 = v319 + v319 + v316 - 589472948 + 1;
  ++v319;
  v321 = 2 * v317 + 942166371;
  v322 = v320 + v318 - 344804349 + 849785358;
  v323 = v320 - v321;
  v322 += 53013894;
  v324 = v321 - v319;
  v325 = v322 + v323 + 1;
  v326 = 4 * (v325 + v319 - v322 - 2049097191 + 1);
  v322 -= 1029516387;
  v327 = v325 + 473722879 - v322;
  v326 -= 1652737171;
  v328 = v324 + 1 - v326;
  v329 = v326 - v327;
  v322 += 1088562794;
  v327 += 78577575;
  v330 = v329 - v322 - v327 + 132302044;
  v328 -= 771106090;
  v322 += 2;
  v331 = v330 + 1 - v328;
  v332 = v327 - v331;
  v333 = v332 + v328;
  v332 += 1152138250;
  v334 = v322 + v331 - 1557943841 + 1;
  v335 = v332 + v322 - v334;
  v336 = v333 + 1293271530 - v332 - v335;
  v334 += 245975965;
  v337 = v334 + v335 + 2098061773;
  v332 += 1210065134;
  v338 = v334 - v336 + 1;
  v339 = v337 + 1 - v332 + 1042845593;
  v332 += 1017773432;
  v340 = v336 - v338 + 544855734;
  v341 = v340 + 2 * v339 + 1636319835;
  v340 -= 2122376282;
  v342 = v332 + v332 + v338 - 213405862;
  v332 += 1914409404;
  v343 = 2 * (v341 + 1) - v340 + 1026384791;
  v344 = v332 + v342 - 207594250 + 1367733505 - v340;
  v345 = v340 - v343++ + 1434173388;
  v346 = v344 - 1373169356 - v332++;
  v347 = v332 + v346 - 1698350246 + 807585909 - v343 - 1616726979;
  v348 = v343 - v332;
  v349 = v348 + v347;
  v350 = v349++ + v348 + 1;
  v351 = 2 * (v345 - 28630427 + 560310549 - v350 + 1) + 1587875006 - v349 - 258344410;
  v352 = v332 - 390257379 + 1 - v349;
  v353 = v352 + v349;
  v354 = v352++ + v350 + 4;
  v355 = v351 + 1 - v352;
  v354 -= 1828963202;
  v356 = v354 + 2 * v352 + 1;
  v357 = v356 + v355 - 1265518153 + 1354618067;
  v358 = v354 + v356 - v357;
  v354 += 24457593;
  v358 += 2081985567;
  v359 = v354 + v353 + 1624829730 + 1;
  v360 = 2 * (v358 + v357 - 1949374989) + 781522725;
  v361 = ++v354 + v358;
  v362 = v354 + 1493767541 - v359;
  v361 += 4;
  v363 = 2 * v359 - v361 - 1727523967;
  v364 = v362 + v361 + v360 + 218569202 - v363 + 449916241;
  v363 += 327109260;
  v365 = v362 + 1549803007 - v363 + 957128236;
  v363 += 916862246;
  v366 = 2 * (v364 + 414246669) + 2040411505;
  v367 = v365 + 536918145 - v366;
  v368 = v366 - v367 + 1;
  v369 = 2 * (v367 - 129161079 - v363 + 1) - 1900300983;
  v370 = 2 * (v361 - 798140456) + 4;
  v371 = v370 + v363 - 665700202 + 2;
  v369 += 30341174;
  v372 = v370 + 1 - v369 - 1952101394;
  v373 = v372 + v369 - v371;
  v374 = v373 + v371;
  v375 = 2 * (v374 + v372 + 1 - 1317292497);
  v376 = v373 - 2112199059 + 419983391;
  v377 = v376 + 2 * (v368 - 1343830370 + 442537035) - 1033591519 + 1879391070 - v375 - 2060553041 + 1;
  v378 = v375 + v375 + v374 + 738693954 + 1 - v377;
  v379 = v375 + 1 - v377;
  v380 = v377 - 1930629742 - v379 - 1928040188 + 1102478597;
  v381 = v380 + 2 * v379 + 1 - 448866693;
  v376 -= 2055000006;
  v382 = 2 * (2 * (v380 + 604066061) + 2);
  v383 = v382 + v376 + v381 - 1881910858;
  v384 = v378 - 947925440 + 2;
  v385 = v384 + v383 + v382 + 842529404 + 1;
  v376 -= 168380786;
  ++v384;
  v386 = v376 + v383 + 1;
  v387 = v376 - v384 + 1919090703;
  v388 = 2 * (v384 + 1 - v386 + 1) - 376075359 - v387;
  v389 = v388 + v386 - 1078951762;
  v388 += 4;
  v390 = v388 + v387 + 1;
  v388 += 1398399335;
  v391 = v390 + v385 - 1475310267 - v389 + 1 + 9540715;
  v392 = v389 - 1641637778 + 2 - v388 + 2;
  v393 = v388 - 1972219276 + 1;
  v392 -= 866747255;
  v394 = v392 + v390 - 1373171668 + 1586106979;
  v395 = v393 + v391 - 931348898;
  v396 = v394 + v392 - 1900058436 - v395;
  v397 = 2 * v394 + 1334476417;
  v398 = v396 - 467332541 + 1817029648;
  v399 = 2 * (v393 + 808026034) - 1047285892 + 609483421 - v397;
  v395 += 1953163588;
  v400 = v397 - 292607806 - v399 - 42192282 - v395 + 1;
  v401 = v399 + 1 - v398 + 1;
  v402 = v395 + 1 - v401;
  v403 = v400 - v402;
  v404 = v401 + 1 - v403 + 1872425146;
  v405 = v398 - 195196821 + 377105645 - v404 - v404;
  v406 = v402 - v404;
  v407 = v404 - 1842186611 + 547686199;
  v408 = v407 + v403 + 1374530959 - v405 + 1 - 184314042;
  v409 = v405 - 1871472347 + 1;
  v410 = v409 + v406;
  v409 += 2027045620;
  v411 = v409 + v410 - 855357098 + 1 - 2037318886;
  v412 = v411 + v408 + 1324830997 - v409 + 1863672173;
  v413 = 2 * (v407 - 1311778367) + 1;
  v414 = v413 + v411;
  v409 += 638982232;
  v415 = v412 - 1420319999 - v409 + 1706741566;
  v413 += 2;
  v416 = v409 + 600153250 - v415 - 1749613292 + 1;
  v417 = v415 - v413;
  v418 = v414 - 103143630 + 151909657 - v416 + 1;
  v419 = 2 * v413 - v416++;
  v420 = v417 + 1 - ++v419;
  v421 = v418 - v416 - v416 + v419;
  v420 -= 1385665685;
  return v420+ v421+ 1+ 640484926+ 2 * (v421 + v416 + 1815285368)+ v420+ v421+ 1+ 640484926+ v420+ v421+ 1+ v420+ v421 + 1+ v420- 1389466703+ 495424244+ 2 * (v420 + v421 + 1 + 640484926);
}

正如你所看到的,F5(Hex-Rays插件)在这种情况下没有实质性的帮助。 由于IDA和Hex-Rays是高度可编程的,因此其实可以自己改进Hex-Rays反编译器的输出并教导它简化这些表达式(当然这就算是另一个话题了)。除非我们将这个函数作为黑盒算法来处理,否则我们通过F5并真正理解它的操作。 我们将使用Z3库并查看它是否可以将所有这些指令简化为可读的有意义的内容。

Z3库的快速上手
Dennis和Eric对Z3的介绍已经做得很好,因此我会尽量缩短关于Z3的基础部分的章节。假设我们遇到这样一段汇编代码:

.text:0040EF04     mov     eax, [ebp+c1]
.text:0040EF07     mov     edx, [ebp+c2]
.text:0040EF0A     mov     ecx, [ebp+c3]
.text:0040EF0D     mov     ebx, [ebp+c4]
.text:0040EF10     inc     eax
.text:0040EF11     inc     ebx
.text:0040EF12     inc     edx
.text:0040EF13     inc     ecx
.text:0040EF14     add     ebx, edx
.text:0040EF16     add     ecx, 123h
.text:0040EF1C     add     eax, ebx
.text:0040EF1E     add     ebx, 456h
.text:0040EF24     add     edx, eax
.text:0040EF26     add     ecx, eax
.text:0040EF28     add     edx, ebx
.text:0040EF2A     sub     eax, 12312312h
.text:0040EF2F     add     ecx, eax
.text:0040EF31     add     eax, ebx
.text:0040EF33     add     eax, ecx
.text:0040EF35     add     eax, edx
.text:0040EF37     mov     [ebp+result], eax

从0x040EF04到0x040EF0D,我们看到eax == c1,edx == c2,ecx == c3,ebx == c4(4个输入参数)。从0x040EF10到0x040EF35,我们看到一些操作发生,并且操作的结果被复制到0x040EF37处的eax。我们可以将上面的列表翻译成一系列表达式:

.text:0040EF10     eax = eax + 1
.text:0040EF11     ebx = ebx + 1
.text:0040EF12     edx = edx + 1
.text:0040EF13     ecx = ecx + 1
.text:0040EF14     ebx = ebx + edx
.text:0040EF16     ecx = ecx + 0x123
.text:0040EF1C     eax = eax + ebx
.text:0040EF1E     ebx = ebx + 0x456
.text:0040EF24     edx = edx + eax
.text:0040EF26     ecx = ecx + eax
.text:0040EF28     edx = edx + ebx
.text:0040EF2A     eax = eax - 0x12312312
.text:0040EF2F     ecx = ecx + eax
.text:0040EF31     eax = eax + ebx
.text:0040EF33     eax = eax + ecx
.text:0040EF35     eax = eax + edx

现在让我们把这些表达式通过Z3库来表示一下(注意Z3重载算术运算符):

import z3

c1, c2, c3, c4 = z3.BitVecs('c1 c2 c3 c4', 32)
eax, edx, ecx, ebx = c1, c2, c3, c4

eax = eax + 1
ebx = ebx + 1
edx = edx + 1
ecx = ecx + 1
ebx = ebx + edx
ecx = ecx + 0x123
eax = eax + ebx
ebx = ebx + 0x456
edx = edx + eax
ecx = ecx + eax
edx = edx + ebx
eax = eax - 0x12312312
ecx = ecx + eax
eax = eax + ebx
eax = eax + ecx
eax = eax + edx

print(eax)

最后的结果是:

c1 + 1 + c4 + 1 + c2 + 1 - 305210130 +c4 + 1 + c2 + 1 + 1110 + c3 +1 + 291 + c1 + 1 + c4 + 1 + c2 +1 + c1 + 1 + c4 + 1 + c2 + 1 - 305210130 +c2 + 1 + c1 + 1 + c4 + 1 + c2 + 1 + c4 + 1 +c2 + 1 + 1110

然而,我们仍然可以通过调用z3.simplify(eax)来让Z3简化最终的表达式,并获得更为简单的输出:

3684549565 + 4*c1 + 6*c4 + 7*c2 + c3

现在我们有了最后的简化的表达式,我们可以对这个表达式进行求解:

solver = z3.Solver()

result = z3.BitVec('result', 32)

solver.add(c1 == 1, 
           c2 == 2, 
           c3 == 3, 
           c4 == 4, 
           eax == result)
if solver.check() == z3.sat:
    m = solver.model()
    print("result=%08X" % m[result].as_long())

最终,我们让解算器在给定 c1 == 1,c2 == 2,c3 == 3和c4 == 4的情况下查找表达式的结果(eax == result)。输出为restult= DB9DC3F1。

将汇编转成Z3表达式

上面我们用z3库小试牛刀,手动构建表达式并使用Z3简化和求解,那我们考虑能否自动生成反汇编列表中的表达式?答案是肯定的,我们将使用类似于上周仿真文章的技术。 我们不会计算这些值,而只是在做Z3算法

def simplify_func(emu_start, emu_end):
    # Reset registers    
    regs_initial = { 
      REG_EAX: z3.BitVec('c1', 32),
      REG_EDX: z3.BitVec('c2', 32),
      REG_ECX: z3.BitVec('c3', 32),
      REG_EBX: z3.BitVec('c4', 32),
    }

    regs = {}
    for k, v in regs_initial.items():
        regs[k] = v
    
    def get_opr_val(inst, regs):
        if inst.Op2.type == o_imm:
            return (True, z3.BitVecVal(inst.Op2.value, 32))
        elif inst.Op2.type == idaapi.o_reg:
            return (True, regs[inst.Op2.reg])
        else:
            return (False, 0)
            
    ea = emu_start
    while ea <= emu_end:
        ok = True
        inst = idautils.DecodeInstruction(ea)
        ea += inst.size
        if inst.itype == idaapi.NN_dec and inst.Op1.type == idaapi.o_reg:
            regs[inst.Op1.reg] = (regs.get(inst.Op1.reg, 0) - 1)
        elif inst.itype == idaapi.NN_inc and inst.Op1.type == idaapi.o_reg:
            regs[inst.Op1.reg] = (regs.get(inst.Op1.reg, 0) + 1)
        elif inst.itype == idaapi.NN_sub:
            ok, val = get_opr_val(inst, regs)
            regs[inst.Op1.reg] = (regs.get(inst.Op1.reg, 0) - val)
        elif inst.itype == idaapi.NN_add:
            ok, val = get_opr_val(inst, regs)
            regs[inst.Op1.reg] = (regs.get(inst.Op1.reg, 0) + val)
        else:
            ok = False

        if not ok:
            return (False, "Emulation failed at %08X" % ea)

    # Simplify the final expression which is in EAX
    result_expr = z3.simplify(regs[REG_EAX])
        
    def evaluate(c1, c2, c3, c4):
        """Capture the context and return a function that can be used to 
        evaluate the simplified expression given the input arguments"""
        s = z3.Solver()
        r = z3.BitVec('r', 32)

        # Add contraints for input variables
        s.add(regs_initial[REG_EAX] == c1, regs_initial[REG_EDX] == c2,
              regs_initial[REG_ECX] == c3, regs_initial[REG_EBX] == c4)

        # Add the result constraint
        s.add(result_expr == r)

        if s.check() == z3.sat:
            m = s.model()
            return m[r].as_long()
        else:
            return None

    return (True, evaluate)

上面的代码和我们以前见过的[http://0xeb.net/2018/02/writing-a-simple-x86-emulator-with-idapython/#scoping]非常相似,所以我只会解释Z3的相关代码:     
  • 第3-8行:创建32位Z3变量。 这些变量对应于初始变量值(和输入值)     
  • 第10-12行:别名变量。 这些别名将根据行更新并包含更复杂的表达式(不仅仅是初始值)     
  • 第44行:获取最终表达式的简化版本     
  • 第46-63行:创建捕获当前上下文的嵌套函数。 评估函数取4个输入参数并返回简化表达式的评估结果。 
我返回一个函数,以便我可以缓存它并调用它来求解特定的函数。为了测试代码,我们可以执行如下操作:

Python>ok, challenge_1 = simplify_func(0x401020, 0x40266C)
Python>print('result=%08X' % challenge_1(1, 2, 3, 4))

我得到的值为5E6571B0。 如果代码正常工作,你们也应该具有与运行该程序相同的结果:

C:\ida-z3-tests>test 0 1 2 3 4 challenge_1(1, 2, 3, 4) -> 5E6571B0

参考链接:

https://yurichev.com/writings/SAT_SMT_draft-EN.pdf

http://0xeb.net/2018/02/writing-a-simple-x86-emulator-with-idapython/ 

http://ericpony.github.io/z3py-tutorial/guide-examples.htm


 
翻译:看雪翻译组-skeep
校正: 看雪翻译组-makefile

[CTF入门培训]顶尖高校博士及硕士团队亲授《30小时教你玩转CTF》,视频+靶场+题目!助力进入CTF世界

最后于 2018-9-19 18:08 被skeep编辑 ,原因: 部分内容被折叠,新版UI发布后重新修改代码格式
上传的附件:
收藏
点赞2
打赏
分享
最新回复 (14)
雪    币: 4836
活跃值: (61)
能力值: ( LV4,RANK:45 )
在线值:
发帖
回帖
粉丝
HeyLXF 2018-6-20 23:18
2
0
一部分内容不显示??
雪    币: 375
活跃值: (141)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
gegon 2018-6-21 09:35
3
0
代码显示不正常
雪    币: 1408
活跃值: (4043)
能力值: ( LV13,RANK:240 )
在线值:
发帖
回帖
粉丝
IamHuskar 4 2018-6-21 10:27
4
0
好文
雪    币: 940
活跃值: (1053)
能力值: ( LV3,RANK:20 )
在线值:
发帖
回帖
粉丝
红金龙e晓楼 2018-6-21 10:52
5
0
咋这么多问号额
雪    币: 1473
活跃值: (382)
能力值: ( LV9,RANK:180 )
在线值:
发帖
回帖
粉丝
skeep 1 2018-6-26 18:01
6
0
里面都是一些冗余的代码,难道是被删了?晚上回去看看
雪    币: 1473
活跃值: (382)
能力值: ( LV9,RANK:180 )
在线值:
发帖
回帖
粉丝
skeep 1 2018-7-23 01:03
7
0
我看了一下那些汇编代码是被系统不显示的,在后台编辑的时候都在,所以我也没辙了
雪    币: 16429
活跃值: (59390)
能力值: (RANK:125 )
在线值:
发帖
回帖
粉丝
Editor 2018-8-8 15:41
8
0
skeep 我看了一下那些汇编代码是被系统不显示的,在后台编辑的时候都在,所以我也没辙了[em_2]
没办法显示的内容,建议截图放上去
雪    币: 375
活跃值: (141)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
gegon 2018-8-9 09:23
9
0
建议把翻译的doc放到附件里
雪    币: 3349
活跃值: (3372)
能力值: ( LV4,RANK:50 )
在线值:
发帖
回帖
粉丝
fengyunabc 1 2018-8-9 09:38
10
0
感谢分享!
雪    币: 20309
活跃值: (5274)
能力值: ( LV12,RANK:529 )
在线值:
发帖
回帖
粉丝
会飞的鱼油 8 2018-9-12 23:06
11
0
.text:0040EF10 eax = eax + 1
.text:0040EF11 ebx = ebx + 1
.text:0040EF12 edx = edx + 1
.text:0040EF13 ecx = ecx + 1
.text:0040EF14 ebx = ebx + edx
.text:0040EF16 ecx = ecx + 0x123
.text:0040EF1C eax = eax + ebx
.text:0040EF1E ebx = ebx + 0x456
.text:0040EF24 edx = edx + eax
.text:0040EF26 ecx = ecx + eax
.text:0040EF28 edx = edx + ebx
.text:0040EF2A eax = eax - 0x12312312
.text:0040EF2F ecx = ecx + eax
.text:0040EF31 eax = eax + ebx
.text:0040EF33 eax = eax + ecx
.text:0040EF35 eax = eax + edx
请问ida是怎么转换汇编运算指令到上面那样的
最后于 2018-9-12 23:07 被会飞的鱼油编辑 ,原因:
雪    币: 1473
活跃值: (382)
能力值: ( LV9,RANK:180 )
在线值:
发帖
回帖
粉丝
skeep 1 2018-9-19 17:58
12
0
更换新界面之后,我重新编辑一下已经能够正常显示,望楼上知悉
雪    币: 1473
活跃值: (382)
能力值: ( LV9,RANK:180 )
在线值:
发帖
回帖
粉丝
skeep 1 2018-9-19 19:29
13
0
会飞的鱼油 .text:0040EF10&nbsp;eax&nbsp;=&nbsp;eax&nbsp;+&nbsp;1.text:0040EF11&nbsp;ebx ...
以我的理解,那部分内容是作者随便写的,并不是IDA中的指令,所以这段应该是汇编版本的伪代码。
理由就是作者说“假设我们遇到这样一段汇编代码”
雪    币: 8211
活跃值: (4700)
能力值: ( LV4,RANK:45 )
在线值:
发帖
回帖
粉丝
v0id_ 2019-9-30 00:28
14
0
mark
雪    币: 1775
活跃值: (3995)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
Grav1ty 2023-4-28 01:23
15
0
mark
游客
登录 | 注册 方可回帖
返回