[羊城杯 2020]ByteCode writeup

标签：writeup a3 a1 flag a2 2020 ByteCode ord a4

下载附件打开：

 

 可以判断为是Python 字节码，按照逻辑手动反编译出源码来即可，逻辑并不复杂，有不懂的地方可以看参考文献

还原出来的源码为：

# flag = input("please input your flag: ")
flag = ""
en = [3, 37, 72, 9, 6, 132]
output = [101, 96, 23, 68, 112, 42, 107, 62, 96, 53, 176, 179, 98, 53, 67, 29, 41, 120, 60, 106, 51, 101, 178, 189, 101,
          48]

a = len(flag)
if a < 38:
    print("length wrong")
    exit(0)
if 2020 * (ord(flag[0]) + ord(flag[1]) + ord(flag[2]) + ord(flag[3]) + ord(flag[4])) == 1182843538814603:
    print('good!continue\xe2\x80\xa6\xe2\x80\xa6')
else:
    print("byte~")
    exit(0)

x = []
k = 5
for i in range(13):
    b = ord(flag[k])
    c = ord(flag[k + 1])
    a11 = c ^ en[i % 6]
    a22 = b ^ en[i % 6]
    x.append(a11)
    x.append(a22)
    k += 2

if x == output:
    print('good!continue\xe2\x80\xa6\xe2\x80\xa6')
else:
    print('oh,you are wrong!')
    exit(0)

l = len(flag)
a1 = ord(flag[l - 7])
a2 = ord(flag[l - 6])
a3 = ord(flag[l - 5])
a4 = ord(flag[l - 4])
a5 = ord(flag[l - 3])
a6 = ord(flag[l - 2])

if a1 * 3 + a2 * 2 + a3 * 5 == 1003:
    if a1 * 4 + a2 * 7 + a3 * 9 == 2013:
        if a1 + a2 * 8 + a3 * 2 == 1109:
            if a4 * 3 + a5 * 2 + a6 * 5 == 671:
                if a4 * 4 + a5 * 7 + a6 * 9 == 1252:
                    if a4 + a5 * 8 + a6 * 2 == 644:
                        print('congraduation!you get the right flag!')

可以看到最后的判断条件是一个6元一次方程，可以用z3求解：

#!/usr/bin/env python
# coding: utf-8

# In[1]:


import z3


# In[2]:


solver = z3.Solver()


# In[4]:


a1,a2,a3,a4,a5,a6 = z3.Ints('a1 a2 a3 a4 a5 a6')


# In[5]:


solver.add(a1 * 3 + a2 * 2 + a3 * 5 == 1003)
solver.add(a1 * 4 + a2 * 7 + a3 * 9 == 2013)
solver.add(a1 + a2 * 8 + a3 * 2 == 1109)
solver.add(a4 * 3 + a5 * 2 + a6 * 5 == 671)
solver.add(a4 * 4 + a5 * 7 + a6 * 9 == 1252)
solver.add(a4 + a5 * 8 + a6 * 2 == 644)


# In[8]:


if solver.check() == z3.sat:
    ans = solver.model()
    print(ans)


# In[9]:


type(ans)


# In[14]:


flag = [0] * 38


# In[15]:


l = len(flag)


# In[16]:


l


# In[17]:


flag[l - 7] = a1
flag[l - 6] = a2
flag[l - 5] = a3
flag[l - 4] = a4
flag[l - 3] = a5
flag[l - 2] = a6


# In[18]:


output = [101, 96, 23, 68, 112, 42, 107, 62, 96, 53, 176, 179, 98, 53, 67, 29, 41, 120, 60, 106, 51, 101, 178, 189, 101,
          48]


# In[19]:


len(output)


# In[20]:


a11 = []
a22 = []
for i in range(0, len(output), 2):
    a11.append(output[i])
    a22.append(output[i+1])


# In[21]:


en = [3, 37, 72, 9, 6, 132]


# In[23]:


k = 5
for i in range(13):
    flag[k] = a22[i] ^ en[i % 6]
    flag[k+1] = a11[i] ^ en[i % 6]
    k += 2


# In[24]:


flag


# In[33]:


flag[l - 7] = ans[a1].as_long()
flag[l - 6] = ans[a2].as_long()
flag[l - 5] = ans[a3].as_long()
flag[l - 4] = ans[a4].as_long()
flag[l - 3] = ans[a5].as_long()
flag[l - 2] = ans[a6].as_long()


# In[34]:


flag


# In[35]:


"".join(chr(int(x)) for x in flag)

 最后可以拿到flag：

中间字符串就是flag内容，前5个字符和最后一个字符是flag的格式

需要注意的是，z3求解出来的答案类型为z3.z3.IntNumRef，这个参数不能直接当作参数，也不能用int()转换，需要在求解的时候加上.as_long()转化

 

标签：writeup,a3,a1,flag,a2,2020,ByteCode,ord,a4
From： https://www.cnblogs.com/BlackIce416/p/17152326.html