BuckeyCTF - square cipher

(lambda x=int(input('> '),16):
(all((int(bin(y).translate(str.maketrans('1b','fx')),0)&x).bit_count()==15 for y in
[511,261632,1838599,14708792,117670336,133955584,68585259008,35115652612096,246772580483072,1974180643864576,15793445150916608,17979214137393152,9205357638345293824,4713143110832790437888,4731607904558235517441,9463215809116471034882,18926431618232942069764,33121255085135066300416,37852863236465884139528,75705726472931768279056,151411452945863536558112,264970040681080530403328,302822905891727073116224,605645811783454146232448,1211291623566908292464896,2119760325448644243226624,2413129272746388704198656])
and x&2135465562637171390290201561322170738230609084732268110734985633502584038857972308065155558608880
==1271371190459412480076309932821732439054921890752535035282222258816851982409101952239053178406432 
or print('incorrect'))and print(__import__('os').environ.get('FLAG','bctf{fake_flag}')))()

程序会对数据的输入进行两类对比：

• 首先将列表中的每一个数字转换成 0b 格式后，变成十六进制，1 -> f, 0 -> 0 ， 最后和每一个数字 and 后的1数量有15个
• 和一个大整数 and 后得到另一个

首先估计位数：

# max bit_count
bit_count = 0

for y in [511,261632,1838599,14708792,117670336,133955584,68585259008,35115652612096,246772580483072,1974180643864576,15793445150916608,17979214137393152,9205357638345293824,4713143110832790437888,4731607904558235517441,9463215809116471034882,18926431618232942069764,33121255085135066300416,37852863236465884139528,75705726472931768279056,151411452945863536558112,264970040681080530403328,302822905891727073116224,605645811783454146232448,1211291623566908292464896,2119760325448644243226624,2413129272746388704198656]:
    bin_str = str(bin(int(bin(y).translate(str.maketrans('1b','fx')),0) ))[2:]
    bit_count = max([len(bin_str), bit_count])
    print(bit_count)

for y in [2135465562637171390290201561322170738230609084732268110734985633502584038857972308065155558608880,
          1271371190459412480076309932821732439054921890752535035282222258816851982409101952239053178406432 ]:
    bin_str = str(bin(y))[2:]
    bit_count = max([len(bin_str), bit_count])
    print(bit_count)

有324位，然后尝试用z3求解。自动生成z3代码：

import math

bit_count = 324     # each bit: 0/1, create a variable


group = []
bit_a = str(bin(2135465562637171390290201561322170738230609084732268110734985633502584038857972308065155558608880))[2:][::-1]
bit_b = str(bin(1271371190459412480076309932821732439054921890752535035282222258816851982409101952239053178406432))[2:][::-1]
for y in [511,261632,1838599,14708792,117670336,133955584,68585259008,35115652612096,246772580483072,1974180643864576,15793445150916608,17979214137393152,9205357638345293824,4713143110832790437888,4731607904558235517441,9463215809116471034882,18926431618232942069764,33121255085135066300416,37852863236465884139528,75705726472931768279056,151411452945863536558112,264970040681080530403328,302822905891727073116224,605645811783454146232448,1211291623566908292464896,2119760325448644243226624,2413129272746388704198656]:
    bin_str = str(bin(int(bin(y).translate(str.maketrans('1b','fx')),0) ))[2:]
    group.append(bin_str[::-1])

# create constraint code

code = """
from z3 import *\n
s = Solver()\n

"""

# define variable
for i in range(324):
    code+=f'x{i} = Int(\'x{i}\')\n'

for i in range(324):
    code += f's.add(x{i} <= 1)\n'
    code += f's.add(x{i} >= 0)\n'


# create constraint for part1
for bin_str in group:
    
    equation = ''
    for i in range(len(bin_str)):
        if bin_str[i] == '1':
            equation += f'x{i}+'
    equation = equation[:-1] + ' == 15'
    
    code+= f's.add({equation})\n'
            
# create constraint for part2
for i in range(len(bit_a)):
    if bit_a[i] == '1':
        code+= f's.add(x{i} == {bit_b[i]})\n'

code += f"""
model = 0
if s.check() == sat:\n
    model = s.model()
else:
    exit(-1)\n
"""

            
code += 'bin_str = \'\'\n'
for i in range(324):
    code += f'bin_str += str(model[x{i}].as_long())\n'

code += """
bin_str = bin_str[::-1]
print(hex(int(bin_str, 2)))
"""

print(code)

运行后获得auto.py, 再运行即可

(venv13) woc@myarch:buckeyCTF/square-cipher $ python code_gen.py > auto.py
(venv13) woc@myarch:buckeyCTF/square-cipher $ python auto.py
0x986227f143f97038053257287030750a23b61047f988f6106146504e61f0878b9426e05e30e8062b
(venv13) woc@myarch:buckeyCTF/square-cipher $ ncat --ssl square-cipher.challs.pwnoh.io 1337
> 986227f143f97038053257287030750a23b61047f988f6106146504e61f0878b9426e05e30e8062b
bctf{5um_0f_f1r57_n_0dd_numb3r5_c1ph3r_025165aa}

z3中的BitVec会实现自然溢出，刚开始使用1bit类型的时候，相加等于15的约束一直无法满足。后来换成int再加上[0, 1]约束才通过