NSSCTF-RoundX easy_z3

NSSCTF-RoundX easy_z3

分析

首先查壳，发现是UPX，但是直接手动去壳不行，发现是魔改的UPX，更改一下三个值再去脱壳就行了

然后放入IDA中分析

根据每个函数分析出了大致的解题过程，那么先用z3解出我们要的吧

from z3 import *

a1 = [BitVec("num[%d]" % i, 32) for i in range(20)]
s = Solver()
s.add(
    20 * a1[19] * 19 * a1[18]
    + 14 * a1[13]
    + 13 * a1[12]
    + 11 * a1[10] * 10 * a1[9]
    + 30 * a1[5]
    + 5 * a1[4]
    + a1[0]
+ 2 * a1[1]
- 3 * a1[2]
- 4 * a1[3]
- 7 * a1[6]
+ 8 * a1[7]
- 9 * a1[8]
- 12 * a1[11]
- 16 * a1[15] * 15 * a1[14]
- 17 * a1[16]
- 18 * a1[17] == 2582239)
s.add(
    20 * a1[19] * 19 * a1[18]
    + 14 * a1[13]
    + 13 * a1[12]
    + 11 * a1[10] * 10 * a1[9]
    + 30 * a1[5]
    - 7 * a1[6]
    + 8 * a1[7]
    - 9 * a1[8]
    + 5 * a1[4]
    + 3 * a1[2]
    + 2 * a1[1] * a1[0]
    - 4 * a1[3]
    - 12 * a1[11]
    - 16 * a1[15] * 15 * a1[14]
    - (18 * a1[17]
       + 17 * a1[16]) == 2602741)
s.add(19 * a1[18]
     + 18 * a1[17]
     + 14 * a1[13] * 13 * a1[12]
     + 12 * a1[11] * 11 * a1[10]
     + 9 * a1[8]
     + 7 * a1[6] * 30 * a1[5]
     + a1[0]
     - 2 * a1[1]
     - 4 * a1[3] * 3 * a1[2]
     - 5 * a1[4]
     + 8 * a1[7]
     - 10 * a1[9]
     - 15 * a1[14]
     - 17 * a1[16] * 16 * a1[15]
     - 20 * a1[19] == 2668123)
s.add(20 * a1[19] * 19 * a1[18]
     + 14 * a1[13]
     + (13 * a1[12] + 11 * a1[10] - 12 * a1[11]) * 10 * a1[9]
     + 30 * a1[5]
     + 5 * a1[4]
     + a1[0]
     + 2 * a1[1]
     - 3 * a1[2]
     - 4 * a1[3]
     - 7 * a1[6]
     + 8 * a1[7]
     - 9 * a1[8]
     - 16 * a1[15] * 15 * a1[14]
     - 17 * a1[16]
     - 18 * a1[17] == 2520193)
s.add(
    18 * a1[17]
    + 17 * a1[16]
    + 15 * a1[14]
    + 13 * a1[12] * 12 * a1[11]
    + 10 * a1[9]
    + 9 * a1[8] * 8 * a1[7]
    + 3 * a1[2] * 2 * a1[1] * a1[0]
    - 4 * a1[3]
    - 5 * a1[4]
    - 30 * a1[5]
    - 7 * a1[6]
    - 11 * a1[10]
    - 14 * a1[13]
    - 16 * a1[15]
    - 19 * a1[18]
    - 20 * a1[19] == 8904587)
s.add(
    18 * a1[17]
    + 7 * a1[6] * 30 * a1[5] * 5 * a1[4]
    + 4 * a1[3]
    + 8 * a1[7]
    + a1[0]
- 2 * a1[1]
- 3 * a1[2]
- 9 * a1[8]
- 11 * a1[10] * 10 * a1[9]
- 16 * a1[15] * (13 * a1[12] + 12 * a1[11] - 14 * a1[13] - 15 * a1[14])
- 17 * a1[16]
- 19 * a1[18]
- 20 * a1[19] == 1227620874)
s.add(20 * a1[19] * 19 * a1[18]
     + 17 * a1[16]
     + 14 * a1[13]
     + 13 * a1[12]
     + 12 * a1[11] * 11 * a1[10] * 10 * a1[9]
     + 7 * a1[6] * 30 * a1[5]
     + 5 * a1[4]
     + 3 * a1[2]
     + a1[0]
     + 2 * a1[1]
     + 4 * a1[3]
     + 8 * a1[7]
     - 9 * a1[8]
     - 16 * a1[15] * 15 * a1[14]
     - 18 * a1[17] == 1836606059)
s.add(
    20 * a1[19] * 19 * a1[18]
    + 16 * a1[15] * 15 * a1[14]
    + 14 * a1[13]
    + 13 * a1[12]
    + 12 * a1[11]
    + 7 * a1[6] * 30 * a1[5]
    + 5 * a1[4]
    + 2 * a1[1] * a1[0]
    - 3 * a1[2]
    + 4 * a1[3]
    + 8 * a1[7]
    - 9 * a1[8]
    - 10 * a1[9]
    - 11 * a1[10]
    - 17 * a1[16]
    - 18 * a1[17] == 8720560)
s.add(20 * a1[19] * 19 * a1[18]
     + 14 * a1[13]
     + 13 * a1[12]
     + 11 * a1[10] * (10 * a1[9] + 30 * a1[5] + 5 * a1[4] + 4 * a1[3] - 7 * a1[6] + 8 * a1[7] - 9 * a1[8])
     + a1[0]
     + 2 * a1[1]
     - 3 * a1[2]
     - 12 * a1[11]
     - (16 * a1[15] - 17 * a1[16] - 18 * a1[17]) * 15 * a1[14] == 11387045)
s.add(
    20 * a1[19] * 19 * a1[18]
    + 16 * a1[15] * 15 * a1[14]
    + 14 * a1[13]
    + 11 * a1[10] * 10 * a1[9]
    + 9 * a1[8]
    + 3 * a1[2]
    + a1[0]
- 2 * a1[1]
+ 4 * a1[3]
- 5 * a1[4]
- 30 * a1[5]
- 7 * a1[6]
+ 8 * a1[7]
- 12 * a1[11]
- 13 * a1[12]
- 17 * a1[16]
- 18 * a1[17] == 7660269)
s.add(20 * a1[19] * 19 * a1[18]
     + 14 * a1[13]
     + 13 * a1[12]
     + 11 * a1[10] * 10 * a1[9]
     - 12 * a1[11]
     + a1[0]
     + 2 * a1[1]
     - (4 * a1[3] * 3 * a1[2]
      - 5 * a1[4]
      - 30 * a1[5])
     - 7 * a1[6]
     + 8 * a1[7]
     - 9 * a1[8]
     - 16 * a1[15] * 15 * a1[14]
     - 17 * a1[16]
     - 18 * a1[17] == 2461883)
s.add(
    14 * a1[13]
    + 11 * a1[10] * 10 * a1[9]
    + 9 * a1[8] * 8 * a1[7]
    + 7 * a1[6]
    + 2 * a1[1] * a1[0]
    - 4 * a1[3] * 3 * a1[2]
    - 5 * a1[4]
    - 30 * a1[5]
    - 12 * a1[11]
    - 13 * a1[12]
    - 15 * a1[14]
    - 17 * a1[16] * 16 * a1[15]
    - 18 * a1[17]
    - 19 * a1[18]
    - 20 * a1[19] == -966296)

s.add(
14 * a1[13]
     + 13 * a1[12]
     + (11 * a1[10] * 10 * a1[9] + 30 * a1[5] + 5 * a1[4] + 3 * a1[2] + 4 * a1[3] - 7 * a1[6] + 8 * a1[7] - 9 * a1[8])
     * 2
     * a1[1]
     + a1[0]
     - 12 * a1[11]
     - 15 * a1[14]
     - 16 * a1[15]
     - 17 * a1[16]
     - 18 * a1[17]
     - 20 * a1[19] * 19 * a1[18] == 254500223
    )
s.add(
16 * a1[15] * 15 * a1[14]
     + 14 * a1[13]
     + 11 * a1[10] * 10 * a1[9]
     + 7 * a1[6] * 30 * a1[5]
     + a1[0]
     - 2 * a1[1]
     - 3 * a1[2]
     - 5 * a1[4] * 4 * a1[3]
     + 8 * a1[7]
     - 9 * a1[8]
     - 12 * a1[11]
     - 13 * a1[12]
     - 17 * a1[16]
     - 18 * a1[17]
     - 19 * a1[18]
     - 20 * a1[19] == 6022286
    )
s.add(
18 * a1[17]
     + 16 * a1[15]
     - 17 * a1[16]
     + 14 * a1[13]
     + 12 * a1[11]
     + 11 * a1[10] * 10 * a1[9]
     + 30 * a1[5]
     + 5 * a1[4]
     + 4 * a1[3] * 3 * a1[2]
     + 2 * a1[1] * a1[0]
     - 9 * a1[8] * 8 * a1[7] * 7 * a1[6]
     - 13 * a1[12]
     - 15 * a1[14]
     - 19 * a1[18]
     - 20 * a1[19] == -636956022
    )
s.add(
20 * a1[19] * 19 * a1[18]
     + 13 * a1[12]
     + 12 * a1[11]
     + 11 * a1[10] * 10 * a1[9]
     + 7 * a1[6]
     + 30 * a1[5]
     + 5 * a1[4]
     + 3 * a1[2] * 2 * a1[1] * a1[0]
     - 4 * a1[3]
     - 9 * a1[8] * 8 * a1[7]
     - 14 * a1[13]
     - 15 * a1[14]
     - 16 * a1[15]
     - 17 * a1[16]
     - 18 * a1[17] == 10631829
)
s.add(
20 * a1[19] * 19 * a1[18]
     + 16 * a1[15]
     - 17 * a1[16]
     - 18 * a1[17]
     + 15 * a1[14] * 14 * a1[13]
     + 13 * a1[12]
     + 11 * a1[10] * 10 * a1[9]
     - 12 * a1[11]
     + 7 * a1[6]
     + (4 * a1[3] - 5 * a1[4] - 30 * a1[5]) * 3 * a1[2]
     + a1[0]
     + 2 * a1[1]
     + 8 * a1[7]
     - 9 * a1[8] == 6191333
)
s.add(
14 * a1[13]
     + 10 * a1[9] * 9 * a1[8] * 8 * a1[7]
     + 5 * a1[4]
     + 4 * a1[3] * 3 * a1[2]
     + 2 * a1[1] * a1[0]
     - 7 * a1[6] * 30 * a1[5]
     - 11 * a1[10]
     - 13 * a1[12] * 12 * a1[11]
     - 16 * a1[15] * 15 * a1[14]
     - 18 * a1[17] * 17 * a1[16]
     - 20 * a1[19] * 19 * a1[18] == 890415359
)
s.add(
20 * a1[19]
     + 19 * a1[18]
     + 18 * a1[17]
     + 16 * a1[15]
     - 17 * a1[16]
     + 12 * a1[11]
     + 11 * a1[10]
     + 10 * a1[9]
     + 9 * a1[8]
     + 30 * a1[5]
     + a1[0]
     + 4 * a1[3] * 3 * a1[2] * 2 * a1[1]
     - 5 * a1[4]
     - 7 * a1[6]
     + 8 * a1[7]
     - 13 * a1[12]
     - 14 * a1[13]
     - 15 * a1[14] == 23493664
)
s.add(
20 * a1[19] * 19 * a1[18]
     + 13 * a1[12]
     + 12 * a1[11]
     + 10 * a1[9]
     + 3 * a1[2] * 2 * a1[1]
     + a1[0]
     - 4 * a1[3]
     - 5 * a1[4]
     + 8 * a1[7] * 7 * a1[6] * 30 * a1[5]
     - 9 * a1[8]
     - 11 * a1[10]
     - 14 * a1[13]
     - 16 * a1[15] * 15 * a1[14]
     - 17 * a1[16]
     - 18 * a1[17] == 1967260144
)
print(s.check())
for i in a1:
    print(s.model()[i].as_long(), end=",")
#跑出来的结果是[104,97,104,97,104,97,116,104,105,115,105,115,102,97,99,107,102,108,97,103]
#有点丑，将就用    

既然所以参数都能求出来，那么就可以直接写一个脚本跑flag了

#include<stdio.h>
#include<string.h>
#include<windows.h>

DWORD Get_254D0(DWORD d254D0[20])
{
	int i = 0;
	DWORD d25050[20] = {0X1207,0X4CA0,0X4F21,0X39,0X1A523,0X23A,0X926,0X4CA7,
						0X6560,0X36,0X1A99B,0X4CA8,0X1BBE0,0X3705,0X926,0X77D3,
						0X9A98,0X657B,0X18,0X0B11};
	for( i ; i < 20 ; i++)
	{
		d254D0[i] = d25050[i];
	}	
}

DWORD Get_25520(DWORD d25520[20], DWORD d254D0[20],DWORD a[20])
{
	for ( int i = 0; ; ++i )
  {
   int v2 = i;
    if ( v2 >= 20 )
      break;
   int v3 = i;
    d25520[v3] = *(a + 20 - i - 1) ^ d254D0[i]; 
  }
}

DWORD sub_1124E(DWORD a1, DWORD a2)
{
	unsigned int v3; 
  	v3 = 1;
  	while ( a2 )
  	{
    	if ( (a2 & 1) != 0 )
     	 v3 *= a1;
    	a1 = a1 * a1 % 1000;
    	a2 >>= 2;
  	}
  return v3;
}

int main()
{
	DWORD a[20] = {104,97,104,97,104,97,116,104,105,115,105,115,102,97,99,107,102,108,97,103};
	DWORD d254D0[20] = {0};
	DWORD d25520[20] = {0};
	DWORD d25000[20] = { 0x07, 0x07, 0x07, 0x09, 0x05, 0x06, 0x07, 0x07, 0x07, 
						 0x09, 0x07, 0x07, 0x05, 0x07, 0x07, 0x07, 0x05, 0x07,
						 0x09, 0x07};
	DWORD Str[20];
	DWORD v3;
	
	Get_254D0(d254D0);
	Get_25520(d25520,d254D0,a);
	
    //这里用的是爆破的方法
	for(DWORD p = 0 ; p < 20 ; p++)
	{
		for( DWORD k = 0 ; k < 127 ; k++)
		{
			Str[p] = k;
			if( d25520[p] == sub_1124E(Str[p], d25000[p]) )
			{
				printf("%c",k);
				break; 
			}
			
		}
	}	
	
}
//T1e_z3_1s_v1r9_3asy!