enumerate()

1
2
enumerate(obj)  # 迭代器，输入可迭代对象，返回索引和迭代元素
for i, char in enumerate(chars):

fromhex()

1
bytes.fromhex(hex_char) # 输入十六进制，按两位转换为byte数据

join()

1
2
3
4
5
separator.join(iterable) 
# 将可迭代对象中的元素连接成一个新的字符串。
# separator：连接符，通常是一个字符串，表示元素之间的分隔符。
# iterable：一个可迭代对象（如列表、元组、字符串等）要求元素是字符串。
chars = "".join(chr(i) for i in range(32,127))

get()

1
2
3
4
5
dict.get(key, default=None)
# 获取字典中指定键对应的值。
# key：要查找的键。
# default：当指定的 key 不在字典中时返回的默认值。如果未指定，默认返回 None。
plaintext += mp.get(bytes([b]), '?')  # 用get获取键的值，如果没有匹配，使用占位符

localtime()

1
2
time_local = time.localtime(timestamp) # 把时间戳转化为时间
dt = time.strftime("%Y-%m-%d %H:%M:%S", time_local) # 把时间按格式输出

base64

1
2
import base64
base64.decodebytes(bflag) # 输入byte数据，解码base64

unhexlify()

1
2
3
4
5
6
7
8
9
10
import binascii
binascii.unhexlify(string) 
# string：一个包含十六进制字符的字符串。这个字符串的长度应该是偶数
# 返回一个字节对象（bytes），表示解码后的原始二进制数据。
# ！！！unhexlify() 不接受带有空格的十六进制字符串，所以需要先将空格去掉。
hex_string = "68 65 6c 6c 6f"
result = binascii.unhexlify(hex_string.replace(" ", ""))
print(result)  # 输出: b'hello'

list(binascii.unhexlify("13141516"))   #直接按2个十六进制字符生成列表，值为十进制

to_bytes()

1
2
3
4
5
6
int.to_bytes(length, byteorder, *, signed=False)
# length：指定返回的字节串的长度（即字节数）。如果整数需要更多的字节才能表示，它会抛出 OverflowError。
# byteorder：字节顺序，决定了多字节数值的字节排列顺序。可以是：
# 'big'：大端字节顺序（高位字节在前）。
# 'little'：小端字节顺序（低位字节在前）。
# signed：是否考虑符号位，默认为 False，表示无符号整数。如果设置为 True，则允许转换负数。

.hex()

1
.hex(bytes)   #可以把byte数据直接转为hex

unsigned()

1
2
3
4
5
6
7
unsigned(int) #可以把有符号整数转为无符号，以便转为bytes数据

flag=b""  # 打印集体的十六进制
for i in result:
    result = unsigned(i).to_bytes(4, 'little')  #小端序输出,前面的参数为字节大小
    flag += result
print(flag.hex())

ord()

1
ord(str)  #可以把字符转为ASCII值

int.from_bytes()

1
int.from_bytes(bytes) #把bytes转为int

map()

1
map(func,arr) #把arr中的每一个元素为参数调用func函数 ->以func函数返回值组成的可迭代对象

bytearry()

1
bytearry(bytes) #把bytes数据按1字节转为byte数组 ->byte数组

z3求解器

pip install z3-solver

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
v5,v6, v7, v8, v9, v10= Ints('v5 v6 v7 v8 v9 v10') #定义多个整数变量
x = z3.Real('x')  #创建实数变量
x = z3.BitVec('x', 32) #创建向量变量，用于计算机位运算，第二个参数是大小，32位，即4字节
p = z3.Bool(name = 'p') #创建布尔变量

s = z3.Solver() #获取求解器实例
s.add() #添加约束条件
And() #与
Or() #或
Not() #否
Implies() #依赖
s.check() #检查解，有解为sat，无解为unsat
s.model() #获取结果
s.model()[x] #获取特定的解
s.model()[x].as_long() #把值转为python整数，以便进行数据处理

一些脚本

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
from z3 import *

v5,v6, v7, v8, v9, v10= Ints('v5 v6 v7 v8 v9 v10')  #定义未知数

a = Solver()
a.add()   #方程组

che = a.check()
res = a.model()
print(f"求解结果{res}")

variable_names = [v5, v6, v7, v8, v9, v10]  #输出的变量，按顺序排
result_list = [res[var].as_long() for var in variable_names]
print(f"结果字符串{result_list}")

flag = ""

for i in result_list:
    result = i.to_bytes(4, 'little')  #小端序输出,前面的参数为字节大小
    flag += result.decode('utf-8')

print(f"flag: {flag}")

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
from z3 import*

flag =""
for i in range(0, 8, 2):
    data = []

    v12 = BitVec("input", 32)
    s = Solver()
    dt = ((v12 << 4) & 4198170623) + (v12 >> 28)

    s.add(And(data[i] - 0x10 <= dt, dt <= data[i] + 0x10))

    while s.check() == sat:
        module = s.model()
        result = module[v12].as_long()
        result_hex = hex(result)[2:]       
        print(f"{result_hex}")
        flag += result_hex
print(f"flag{{{flag}}}")

shell数据提取发送

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
from functools import cmp_to_key
import re
from pwn import *


r = remote("node2.anna.nssctf.cn", 28376)

for i in range(100):
    read = r.recvline()
    data = read.split(b": ")[1].strip().decode() #以：分隔数据，取后面的字符串得到数字的字符串形式

    strs = data.split(' ') #以空格分割成数组
    n = len(strs) #字符串个数
   ...
    r.sendline(senddata) # 发送结果
    print(r.recvline())# 跳过一行，以便读取下一行
print(r.recv())# 读取结果

add矩阵

1
2
3
4
var = list([Int(f"{i}_{j}") for j in range(8)] for i in range(8))
for i in range(8):
     for j in range(8):
         s.add(Sum([tableB[i][k] * var[k][j] for k in range(8)]) == mm1[i][j])