紧张刺激的端午节打了场紧张刺激的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上了。