R0 CREW

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

Оригинал: 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):

//-------------------------------------------------------------------------
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:

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, поэтому я оставлю мое введение очень коротки.

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

.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.

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

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

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

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

Конвертация ассемблерного листинга в выражения 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)

Код выше очень похож на тот, что мы видели раннее, поэтому я объясню лишь ту часть, что связана с 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