紧张刺激的端午节打了场紧张刺激的R3CTF,逆向题目质量真高。弄了一天半做出来两道题,哎水平还是差很多。然后在端午节写这篇blog。
leannum
这道题根据题目介绍来看就是使用写lean4的一个数独程序,lean编译成c++之后确实很抽象啊。给了c++源代码跟ida也没什么区别。然后这道题所给文件起不动调试,需要patch一下链接文件。
然后能调试之后就做起来很舒服,没去符号根据函数名称判断lean_main是主逻辑,然后进入lean_main可以看到printf以及get_stdin,然后就是如下图的函数,所以可以判断就是读取输入,然后由字符串输入转换成另一种type,然后进入check。
使用调试查看函数的参数以及返回值,可以发现是将输入字符串转换成数字。
check内部的前三个比较函数。也是使用调试查看比较函数的内部调用的判断函数的参数,因为程序实现的是数独逻辑,所以比较函数会先将输入转换成9×9的矩阵然后使用判断函数判断是否符合数独。
如下是判断函数
调试判断数独主要验证横,竖,以及所有的左斜对角线。
最后一步验证就是对于输入是否满足程序给的目标数独,目标数独就在l_target全局变量里面储存,调试可以看到。
所以这道题可以起动态调试之后就是很简单的题目,然后麻烦的地方就是跑数独的答案。我第一次尝试的时候就是只有递归进行枚举爆破,然后一旦加入斜行的判断需要的时间就暴增。然后队里的老学长answer告诉我z3是可以跑数独的,悲,白跑半天脚本。
from z3 import*
# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]
# each cell contains a value in {1, ..., 9}
cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]
# each row contains a digit at most once
rows_c = [ Distinct(X[i]) for i in range(9) ]
# each column contains a digit at most once
cols_c = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]
#diagonal
diagonal_c=[ Distinct([X[(0+j)%9][(i+j)%9] for j in range(9) ])
for i in range(9) ]
sudoku_c = cells_c+rows_c+cols_c+diagonal_c
# sudoku instance, we use '0' for empty cells
instance = ((7,0,2,0,0,0,0,0,0),
(0,0,0,0,0,0,0,0,0),
(0,0,0,0,6,0,0,0,0),
(5,0,6,0,3,0,0,0,0),
(0,0,0,0,0,0,1,3,0),
(0,0,0,0,0,0,8,0,6),
(0,4,0,0,0,0,5,0,0),
(0,0,8,5,0,2,0,0,0),
(0,5,0,0,0,0,0,0,0))
instance_c = [ If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9) ]
s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print ("failed to solve")
a=[[7, 6, 2, 8, 1, 9, 3, 5, 4],
[8, 2, 5, 9, 7, 6, 4, 1, 3],
[4, 3, 1, 7, 6, 5, 9, 8, 2],
[5, 9, 6, 4, 3, 8, 2, 7, 1],
[6, 8, 7, 2, 9, 4, 1, 3, 5],
[2, 7, 9, 1, 5, 3, 8, 4, 6],
[9, 4, 3, 6, 8, 1, 5, 2, 7],
[3, 1, 8, 5, 4, 2, 7, 6, 9],
[1, 5, 4, 3, 2, 7, 6, 9, 8]]
for i in range(9):
for j in range(9):
print(a[i][j]-1,end="")
nSMC
一道难得的逆向容器题,刚开始我的网有些问题,网页都打不开。然后第二天是接着mantle的师傅思路往下写的。首先这是个根据用户输入进行自修改的程序,只有正确的flag才能自修改成输出correct,其余的都是Wrong。然后网页由两分钟的定时刷新,会更换程序文件。
对于smc的部分,肯定是要模拟执行让他跑到正确的逻辑,然后mantle提出了可以用idapython跑自动化的脚本。然后我看了一下汇编,是完全可行的。
首先他的每一步smc都是jnz,jmp的分发,所以我可以通过patch jnz与jmp来绕过分发。然后再进入被修改函数时会有一个固定的mov eax,0的标志,所以我可以根据这个标志单步进入,其他的call都是单步步过。然后还有麻烦的点是就要就给他不断的进行输入,所以我们也可以patch绕过一下scanf。思路明确开写脚本。
from idaapi import *
start_process("","","")
continue_process()
wait_for_next_event(WFNE_SUSP, -1)
i=0
while 1:
rip=get_reg_value("RIP")
code=ida_bytes.get_byte(rip)
if code==0x75:
ida_bytes.patch_byte(rip,0x90)
ida_bytes.patch_byte(rip+1,0x90) #patch jnz
if code == 0xEb:
ida_bytes.patch_byte(rip,0x90)
ida_bytes.patch_byte(rip+1,0x90)
if code == 0xE9:
ida_bytes.patch_byte(rip,0x90)
ida_bytes.patch_byte(rip+1,0x90) #patch jmp
ida_bytes.patch_byte(rip+2,0x90)
ida_bytes.patch_byte(rip+3,0x90)
ida_bytes.patch_byte(rip+4,0x90)
if code == 0xFF:
if ida_bytes.get_dword(rip+1)==0x1a4f8225: #根据scanf的地址修改
ida_bytes.patch_byte(rip,0xc3)
step_until_ret()
if code ==0xE8 and ida_bytes.get_byte(rip-5)==0xb8 and ida_bytes.get_byte(rip-4)==0:
step_into()
else :
step_over()
wait_for_next_event(WFNE_SUSP, -1)
i+=1
print(i)
if i>45000: #丑陋的停止
break
print("done")
然后jmp有长jmp跟短jmp,patch的长短不同。然后根据scanf的地址来判断是scanf然后给patch成ret。其实正常判断结束的话可以获取puts的参数然后判断是不是Correct。但是idapython还是不熟,不会写。所以就草率的结束一下,这么跑两分钟是肯定不够的,就需要过一下两分钟的限制。所以这部分就是要用burpsuite把定时器发送请求给丢掉就好了。这个脚本是在第一个scanf后下断点然后执行脚本。
其实队里有个idapython大师学姐写了个两分钟之内就可以跑完的脚本,非常完美,调试都不需要用。但是不是我写的就不贴blog上了。
idapython大师😍