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:
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
evaluatefunction 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:
Thanks to all those who are contributing knowledge and code to the infosec community.
You might also like: