Использование Z3 с IDA для упрощения арифметических операций в функциях

[kitsu]

Оригинал: 0xeb.net

Всегда хотелось изучить анализ програм на основе SMT и недавно я начал изучать эту тему. Существует большое количество фреймворков, статей и туториалов, которое следовало бы изучить.

Поскольку я все еще изучаю данную тему, я не утверждаю, что этот материал какой-то повышенной сложности, наоборот он достаточно базовый и должен быть понятен всем новичкам Z3 (система для доказательства теорем от Microsoft Research). Мои знания основываются на книге Дениса Юричева Quick introduction into SAT/SMT solvers and symbolic execution (прим.пер.: есть только на английском), а также введение в Z3Py от Eric.

В прошлом блогпосте, я проиллюстрировал как писать просто эмулятор для вычисление значения функции без исполнения последней. В этом посте я постараюсь показать как конвертировать арифметические операции из x86 ассемблера в упрощенные выражения Z3.

Введение

Тестовая программа подобная той, что мы видели ранее, где есть таблица из 12 функций, вызывающиеся из main. Каждая функция была сгенерирована случайно, поэтому они содержут случайную последовательность add/sub/dec/inc инструкций, которые работают с eax/ebx/ecx/edx регистрами (и константами).

Вот фрагмент первой функции (по адресу 0x401000):

Code: ASM

//-------------------------------------------------------------------------

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;

}

Инструкции из листинг дизассемблера выглядят очень похоже друг на друга, так что вместое этого я покажу вывод декомпилятора Hex-Rays:

Code: C/C++

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);

}

Как можно заметить, вывод Hex-Rays достаточно бесполезен в этом случае. Поскольку IDA и Hex-Rays легко расширяются с помощью плагинов и скриптов, то можно упростить вывод декомпилятора Hex-Rays и научить его упрощению этих выражений.

Если мы не подходим к этой функции как к черному ящику, то до сих пор у нас нет понимания того, что происходит внутри. Мы воспользуемся Z3, чтобы упростить все эти инструкции в нечто более понимаемое.

Краткое введение в Z3

Денис и Eric сделали отличную работу по вводной части в Z3, поэтому я оставлю мое введение очень коротки.

Посмотрим на этот пример ассемблерного листинга:

Code: ASM

.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 мы можем увидеть несколько операций, после которых результат копируется в eax на адресе 0x040EF37.

Говоря математически, мы можем преобразовать код выше в набор выражений:

Code: ASM

.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 переопределяет арифметические операции):

Code: Python

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 упростить выражения с помощью вызова z3.simplify(eax) и получим следующий вывод:

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

Теперь, поскольку у нас есть конечное выражение, мы можем вычислить его следующем образом:

Code: Python

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())

По существу, мы просим солвера найти результат выражения (eax == result), зная что c1 == 1, c2 == 2, c3 == 3 и c4 == 4. Полученный вывод: result=DB9DC3F1.

Конвертация ассемблерного листинга в выражения Z3

Теперь мы знаем как вручную собирать выражения и упрощать и выполнять с помощью Z3, можем ли мы автоматически генерировать выражения из вывода дизассемблера.

Ответ - да и мы собираемся использовать похожую технику из предыдущей статьи по эмуляции. Вместо вычисления значений, мы попросту вычислим арифметику с помощью Z3:

Code: Python

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)

Код выше очень похож на тот, что мы видели раннее, поэтому я объясню лишь ту часть, что связана с Z3:

• Строки 3-8: Создание 32-битных переменных Z3. Эти переменные соответствуют начальным значениям переменным (и входным переменным)
• Строки 10-12: Создание псевдонимов переменным. Эти псевдонимы в конечном счете будут обновлены и будут содержать более сложные выражения (не только начальные значения)
• Строка 44: Получить упрощенную версию конечного выражения
• Строки 46-63: Создание вложенной функции, которая захватывает текущий контекст. Функция evaluate принимает 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

© Translated by Kitsu special for r0 Crew