25年Re例会作业

例会作业

2025.11.10

test1:蛇年的本命语言

根据课上的提示，我们逆向得到原py文件

不难看出是z3约束，写出脚本

Python
from z3 import *


x = [Int('x_%i' % i) for i in range(30)]

s = Solver()


s.add(7 * x[0] == 504)
s.add(9 * x[0] - 5 * x[1] == 403)
s.add((2 * x[0] - 5 * x[1]) + 10 * x[2] == 799)
s.add(3 * x[0] + 8 * x[1] + 15 * x[2] + 20 * x[3] == 2938)
s.add((5 * x[0] + 15 * x[1] + 20 * x[2] - 19 * x[3]) + 1 * x[4] == 2042)
s.add((7 * x[0] + 1 * x[1] + 9 * x[2] - 11 * x[3]) + 2 * x[4] + 5 * x[5] == 1225)
s.add(11 * x[0] + 22 * x[1] + 33 * x[2] + 44 * x[3] + 55 * x[4] + 66 * x[5] - 77 * x[6] == 7975)
s.add(((21 * x[0] + 23 * x[1] + 3 * x[2] + 24 * x[3] - 55 * x[4]) + 6 * x[5] - 7 * x[6]) + 15 * x[7] == 229)
s.add((2 * x[0] + 26 * x[1] + 13 * x[2] + 0 * x[3] - 65 * x[4]) + 15 * x[5] + 29 * x[6] + 1 * x[7] + 20 * x[8] == 2107)
s.add((10 * x[0] + 7 * x[1] + -9 * x[2] + 6 * x[3] + 7 * x[4] + 1 * x[5] + 22 * x[6] + 21 * x[7] - 22 * x[8]) + 30 * x[9] == 4037)
s.add((15 * x[0] + 59 * x[1] + 56 * x[2] + 66 * x[3] + 7 * x[4] + 1 * x[5] - 122 * x[6]) + 21 * x[7] + 32 * x[8] + 3 * x[9] - 10 * x[10] == 4950)
s.add((((13 * x[0] + 66 * x[1] + 29 * x[2] + 39 * x[3] - 33 * x[4]) + 13 * x[5] - 2 * x[6]) + 42 * x[7] + 62 * x[8] + 1 * x[9] - 10 * x[10]) + 11 * x[11] == 12544)
s.add((((23 * x[0] + 6 * x[1] + 29 * x[2] + 3 * x[3] - 3 * x[4]) + 63 * x[5] - 25 * x[6]) + 2 * x[7] + 32 * x[8] + 1 * x[9] - 10 * x[10]) + 11 * x[11] - 12 * x[12] == 6585)
s.add(((((223 * x[0] + 6 * x[1] - 29 * x[2] - 53 * x[3] - 3 * x[4]) + 3 * x[5] - 65 * x[6]) + 0 * x[7] + 36 * x[8] + 1 * x[9] - 15 * x[10]) + 16 * x[11] - 18 * x[12]) + 13 * x[13] == 6893)
s.add(((((29 * x[0] + 13 * x[1] - 9 * x[2] - 93 * x[3]) + 33 * x[4] + 6 * x[5] + 65 * x[6] + 1 * x[7] - 36 * x[8]) + 0 * x[9] - 16 * x[10]) + 96 * x[11] - 68 * x[12]) + 33 * x[13] - 14 * x[14] == 1883)
s.add((((69 * x[0] + 77 * x[1] - 93 * x[2] - 12 * x[3]) + 0 * x[4] + 0 * x[5] + 1 * x[6] + 16 * x[7] + 36 * x[8] + 6 * x[9] + 19 * x[10] + 66 * x[11] - 8 * x[12]) + 38 * x[13] - 16 * x[14]) + 15 * x[15] == 8257)
s.add(((((23 * x[0] + 2 * x[1] - 3 * x[2] - 11 * x[3]) + 12 * x[4] + 24 * x[5] + 1 * x[6] + 6 * x[7] + 14 * x[8] - 0 * x[9]) + 1 * x[10] + 68 * x[11] - 18 * x[12]) + 68 * x[13] - 26 * x[14]) + 15 * x[15] - 16 * x[16] == 5847)
s.add((((((24 * x[0] + 0 * x[1] - 1 * x[2] - 15 * x[3]) + 13 * x[4] + 4 * x[5] + 16 * x[6] + 67 * x[7] + 146 * x[8] - 50 * x[9]) + 16 * x[10] + 6 * x[11] - 1 * x[12]) + 69 * x[13] - 27 * x[14]) + 45 * x[15] - 6 * x[16]) + 17 * x[17] == 18257)
s.add(((((25 * x[0] + 26 * x[1] - 89 * x[2]) + 16 * x[3] + 19 * x[4] + 44 * x[5] + 36 * x[6] + 66 * x[7] - 150 * x[8] - 250 * x[9]) + 166 * x[10] + 126 * x[11] - 11 * x[12]) + 690 * x[13] - 207 * x[14]) + 46 * x[15] + 6 * x[16] + 7 * x[17] - 18 * x[18] == 12591)
s.add((((((5 * x[0] + 26 * x[1] + 8 * x[2] + 160 * x[3] + 9 * x[4] - 4 * x[5]) + 36 * x[6] + 6 * x[7] - 15 * x[8] - 20 * x[9]) + 66 * x[10] + 16 * x[11] - 1 * x[12]) + 690 * x[13] - 20 * x[14]) + 46 * x[15] + 6 * x[16] + 7 * x[17] - 18 * x[18]) + 19 * x[19] == 52041)
s.add(((((((29 * x[0] - 26 * x[1]) + 0 * x[2] + 60 * x[3] + 90 * x[4] - 4 * x[5]) + 6 * x[6] + 6 * x[7] - 16 * x[8] - 21 * x[9]) + 69 * x[10] + 6 * x[11] - 12 * x[12]) + 69 * x[13] - 20 * x[14] - 46 * x[15]) + 65 * x[16] + 0 * x[17] - 1 * x[18]) + 39 * x[19] - 20 * x[20] == 20253)
s.add((((((((45 * x[0] - 56 * x[1]) + 10 * x[2] + 650 * x[3] - 900 * x[4]) + 44 * x[5] + 66 * x[6] - 6 * x[7] - 6 * x[8] - 21 * x[9]) + 9 * x[10] - 6 * x[11] - 12 * x[12]) + 69 * x[13] - 2 * x[14] - 406 * x[15]) + 651 * x[16] + 2 * x[17] - 10 * x[18]) + 69 * x[19] - 0 * x[20]) + 21 * x[21] == 18768)
s.add((((((555 * x[0] - 6666 * x[1]) + 70 * x[2] + 510 * x[3] - 90 * x[4]) + 499 * x[5] + 66 * x[6] - 66 * x[7] - 610 * x[8] - 221 * x[9]) + 9 * x[10] - 23 * x[11] - 102 * x[12]) + 6 * x[13] + 2050 * x[14] - 406 * x[15]) + 665 * x[16] + 333 * x[17] + 100 * x[18] + 609 * x[19] + 777 * x[20] + 201 * x[21] - 22 * x[22] == 111844)
s.add((((((((1 * x[0] - 22 * x[1]) + 333 * x[2] + 4444 * x[3] - 5555 * x[4]) + 6666 * x[5] - 666 * x[6]) + 676 * x[7] - 660 * x[8] - 22 * x[9]) + 9 * x[10] - 73 * x[11] - 107 * x[12]) + 6 * x[13] + 250 * x[14] - 6 * x[15]) + 65 * x[16] + 39 * x[17] + 10 * x[18] + 69 * x[19] + 777 * x[20] + 201 * x[21] - 2 * x[22]) + 23 * x[23] == 159029)
s.add((((520 * x[0] - 222 * x[1]) + 333 * x[2] + 4 * x[3] - 56655 * x[4]) + 6666 * x[5] + 666 * x[6] + 66 * x[7] - 60 * x[8] - 220 * x[9]) + 99 * x[10] + 73 * x[11] + 1007 * x[12] + 7777 * x[13] + 2500 * x[14] + 6666 * x[15] + 605 * x[16] + 390 * x[17] + 100 * x[18] + 609 * x[19] + 99999 * x[20] + 210 * x[21] + 232 * x[22] + 23 * x[23] - 24 * x[24] == 2762025)
s.add(((((1323 * x[0] - 22 * x[1]) + 333 * x[2] + 4 * x[3] - 55 * x[4]) + 666 * x[5] + 666 * x[6] + 66 * x[7] - 660 * x[8] - 220 * x[9]) + 99 * x[10] + 3 * x[11] + 100 * x[12] + 777 * x[13] + 2500 * x[14] + 6666 * x[15] + 605 * x[16] + 390 * x[17] + 100 * x[18] + 609 * x[19] + 9999 * x[20] + 210 * x[21] + 232 * x[22] + 23 * x[23] - 24 * x[24]) + 25 * x[25] == 1551621)
s.add((((((777 * x[0] - 22 * x[1]) + 6969 * x[2] + 4 * x[3] - 55 * x[4]) + 666 * x[5] - 6 * x[6]) + 96 * x[7] - 60 * x[8] - 220 * x[9]) + 99 * x[10] + 3 * x[11] + 100 * x[12] + 777 * x[13] + 250 * x[14] + 666 * x[15] + 65 * x[16] + 90 * x[17] + 100 * x[18] + 609 * x[19] + 999 * x[20] + 21 * x[21] + 232 * x[22] + 23 * x[23] - 24 * x[24]) + 25 * x[25] - 26 * x[26] == 948348)
s.add(((((((97 * x[0] - 22 * x[1]) + 6969 * x[2] + 4 * x[3] - 56 * x[4]) + 96 * x[5] - 6 * x[6]) + 96 * x[7] - 60 * x[8] - 20 * x[9]) + 99 * x[10] + 3 * x[11] + 10 * x[12] + 707 * x[13] + 250 * x[14] + 666 * x[15] + -9 * x[16] + 90 * x[17] + -2 * x[18] + 609 * x[19] + 0 * x[20] + 21 * x[21] + 2 * x[22] + 23 * x[23] - 24 * x[24]) + 25 * x[25] - 26 * x[26]) + 27 * x[27] == 777044)
s.add((((((177 * x[0] - 22 * x[1]) + 699 * x[2] + 64 * x[3] - 56 * x[4] - 96 * x[5] - 66 * x[6]) + 96 * x[7] - 60 * x[8] - 20 * x[9]) + 99 * x[10] + 3 * x[11] + 10 * x[12] + 707 * x[13] + 250 * x[14] + 666 * x[15] + -9 * x[16] + 0 * x[17] + -2 * x[18] + 69 * x[19] + 0 * x[20] + 21 * x[21] + 222 * x[22] + 23 * x[23] - 224 * x[24]) + 25 * x[25] - 26 * x[26]) + 27 * x[27] - 28 * x[28] == 185016)
s.add(((((((77 * x[0] - 2 * x[1]) + 6 * x[2] + 6 * x[3] - 96 * x[4] - 9 * x[5] - 6 * x[6]) + 96 * x[7] - 0 * x[8] - 20 * x[9]) + 99 * x[10] + 3 * x[11] + 10 * x[12] + 707 * x[13] + 250 * x[14] + 666 * x[15] + -9 * x[16] + 0 * x[17] + -2 * x[18] + 9 * x[19] + 0 * x[20] + 21 * x[21] + 222 * x[22] + 23 * x[23] - 224 * x[24]) + 26 * x[25] - -58 * x[26]) + 27 * x[27] - 2 * x[28]) + 29 * x[29] == 130106)

if s.check() == sat:
    m = s.model()
    for i in range(30):
        print(f"x[{i}] = {m[x[i]]}")
else:
    print("无解")

得到原x对应的ASCII码，再转成字符即可

再分析py文件

1 2	111111116257645365477364777645752361 以上这串数字分别对应的是字符的出现次数,比如HZNUCTF各出现一次

根据以上规律可以得到最后的flag

1	HZNUCTF{ad7fa-76a7-ff6a-fffa-7f7d6a}

test2:水果忍者

dnspy打开Assembly-CSharp.dll,寻找核心加密，发现是AES，直接Cyberchef一把梭

test3:easyGo

字符串查找flag，寻找可疑字符串，连续两次调用发现判断逻辑
输入处下断点后步行，发现右上角直接出现flag

当然，也可以判断出加密函数，发现是base64加密，寻找字母表

test4:rustapp

查找字符串，动态调试，找到核心判断,得到，当v2为0时，输入正确
又有v2=0,v2=v2|(v15^0x21)
推断出v15^0x21为0,即v15=0x21，即input[i]^rust[i]=0x21
写出脚本

#include <bits/stdc++.h>
#include <string>
using namespace std;
int main()
{
    
    char rust[]="rust_library_core_assert";
    char flag[24];
    for(int i=0;i<24;i++)
    {
        flag[i]=rust[i]^0x21;
        cout<<flag[i];
    }
}

1	STRU~MHCS@SX~BNSD~@RRDSU

2025.11.17

test1:re1

入口是简单的花指令，去掉花指令，看伪代码
加密两部分，前后换位，异或加密，写出脚本即可

#include <stdio.h>
#include <string.h>
int main()
{
    unsigned char arr[]="c~scvdzKCEoDEZ[^roDICUMC";
   
    for(int i=0;i<12;i++)
    {
        int temp=arr[2*i];
        arr[2*i]=arr[2*i+1];
        arr[2*i+1]=temp;
    }
     
    for(int i=0;i<strlen(arr);i++)
    {
        arr[i]^=0x30;
        printf("%c",arr[i]);
    }
}