enumerate()
enumerate(obj) # 迭代器，输入可迭代对象，返回索引和迭代元素
for i, char in enumerate(chars):
fromhex()
bytes.fromhex(hex_char) # 输入十六进制，按两位转换为byte数据
join()
separator.join(iterable)
# 将可迭代对象中的元素连接成一个新的字符串。
# separator：连接符，通常是一个字符串，表示元素之间的分隔符。
# iterable：一个可迭代对象（如列表、元组、字符串等）要求元素是字符串。
chars = "".join(chr(i) for i in range(32,127))
get()
dict.get(key, default=None)
# 获取字典中指定键对应的值。
# key：要查找的键。
# default：当指定的 key 不在字典中时返回的默认值。如果未指定，默认返回 None。
plaintext += mp.get(bytes([b]), '?') # 用get获取键的值，如果没有匹配，使用占位符
localtime()
time_local = time.localtime(timestamp) # 把时间戳转化为时间
dt = time.strftime("%Y-%m-%d %H:%M:%S", time_local) # 把时间按格式输出
base64
import base64
base64.decodebytes(bflag) # 输入byte数据，解码base64
unhexlify()
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()
int.to_bytes(length, byteorder, *, signed=False)
# length：指定返回的字节串的长度（即字节数）。如果整数需要更多的字节才能表示，它会抛出 OverflowError。
# byteorder：字节顺序，决定了多字节数值的字节排列顺序。可以是：
# 'big'：大端字节顺序（高位字节在前）。
# 'little'：小端字节顺序（低位字节在前）。
# signed：是否考虑符号位，默认为 False，表示无符号整数。如果设置为 True，则允许转换负数。
.hex()
.hex(bytes) #可以把byte数据直接转为hex
unsigned()
unsigned(int) #可以把有符号整数转为无符号，以便转为bytes数据
flag=b"" # 打印集体的十六进制
for i in result:
result = unsigned(i).to_bytes(4, 'little') #小端序输出,前面的参数为字节大小
flag += result
print(flag.hex())
ord()
ord(str) #可以把字符转为ASCII值
int.from_bytes()
int.from_bytes(bytes) #把bytes转为int
map()
map(func,arr) #把arr中的每一个元素为参数调用func函数 ->以func函数返回值组成的可迭代对象
bytearry()
bytearry(bytes) #把bytes数据按1字节转为byte数组 ->byte数组
z3求解器
pip install z3-solver
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整数，以便进行数据处理
一些脚本
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}")
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}}}")