Using Z3 with IDA to simplify arithmetic operations in functions

I have been meaning to learn about SMT based program analysis for a long time and recently I started learning about the topic. There are so many frameworks, articles and tutorials out there that I shall explore as time goes by.

Since I am still learning, I do not claim that the following material is rocket science or advanced by any means, instead, it is very basic and should be approachable enough by absolute beginners to Z3 (a theorem prover from Microsoft Research). All I know so far comes from reading Dennis Yurichev‘s e-book “Quick introduction into SAT/SMT solvers and symbolic execution” in addition to the Z3Py introductory material by Eric (https://github.com/ericpony/z3py-tutorial).

In last week’s blog post, I illustrated how to write a basic emulator to evaluate a function’s return value without running it. In today’s blog post, I am going to show how to convert thousands of arithmetic operations from x86 assembly code into simplified Z3 expressions.

Introduction

The test program is similar to last week’s test program, where it has a table of 12 challenge functions that get called from the main function. Each challenge function was randomly generated so it contains a random sequence of add/sub/dec/inc instructions that work with the eax/ebx/ecx/edx registers (and immediate values).

Here’s a snippet of the first challenge function (at 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;
}

The disassembly listing of the function above is going to look similar, so instead of showing the disassembly, I am going to show you the output of the Hex-Rays decompiler:

[skip]

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

As you can see, Hex-Rays was not helpful in that case. Since IDA and Hex-Rays are highly programmable, one can actually improve the output of the Hex-Rays decompiler and teach it to simplify those expressions (a topic for another time).

So as you can see, unless we approach this function as a blackbox algorithm, we have no real understanding of its operation yet. We are going to use Z3 and see if it can simplify all of those instructions into something approachable.

Quick Z3 Primer

Dennis and Eric did a good job introducing Z3, therefore I will keep my primer very short.

Imagine the following assembly listing:

.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

From 0x040EF04 to 0x040EF0D, we see that eax==c1, edx==c2, ecx==c3, ebx==c4 (4 input arguments). From 0x040EF10 to 0x040EF35, we see some operations taking place and the result is copied to eax at 0x040EF37.

Mathematically speaking, we can translate the above listing into a series of expressions:

.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

Let’s now give those expressions to Z3 (note that Z3 overloads the arithmetic operators):

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)

The final expression is:

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

However, we can still ask Z3 to simplify the expression by calling z3.simplify(eax) and get the following simpler output:

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

Now that we have the final expression, we can evaluate its value like this:

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

Essentially, we are asking the solver to find the result of the expression (eax == result) given that c1 == 1, c2 == 2, c3 == 3 and c4 == 4. The output is result=DB9DC3F1.

Converting the assembly listing to a Z3 expression

Now that we know how to manually build an expression and ask Z3 to simplify and evaluate it, can we automatically generate the expression from the disassembly listing?

The answer is Yes and we are going to use a similar technique to the emulation article from last week. Instead of computing the values, we will simply be doing Z3 arithmetics:

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)

The code above is very similar to what we have seen before, so I will only explain Z3 related code:

  • Lines 3-8: Create 32-bits Z3 variables. These variables correspond to the initial variables values (and the input values)
  • Lines 10-12: Aliases the variables. Those aliases will be updated down the line and will contain more complicated expressions (not just the initial values)
  • Line 44: Get a simplified version of the final expression
  • Lines 46-63: Create a nested function that captures the current context. The evaluate function takes 4 input arguments and returns the evaluation result of the simplified expression. I return a function so that I can cache it and call it to evaluate functions in question.

To test the code, we can do something like:

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

We get 5E6571B0. If the code works correctly, we should also have the same result as running the program:

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

You can download the full script + binary from here:

password: 123

Thanks to all those who are contributing knowledge and code to the infosec community.

You might also like:

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.