c4f3b4b3 - vm
type: channel
link: https://blog.hxzzz.asia/tag/vm/
items: [RCTF 2024] Re

[RCTF 2024] Re
type: item
date: 2024-05-30T16:08:00+08:00
description: PPTT首先，通过Hook VirtualProtect函数，可以注意到程序有动态代码段修改行为，且调用者是RCTF.exe（主程序段），再通过栈回溯可以注意到，strcmp函数被修改，后续调用的strcmp会让第二个参数的一个确定的字节+1。通过IDA里面的分析，可以了解到，在最后的大IF语句中，有一个strcmp，Str2是用户输入经过打乱后的值（只取11个字节以后），Str1则是字符串常量值，经过动态调试（IDA里面静态无法进行观察），可以发现strcmp对Str1进行了一些修改，通过反着打乱值，并且通过RCTF{}这样的模式，我们可以确定flag是RCTF{sj***emqrp****tyua}，注意，s字符是r字符在strcmp函数中+1而来的。所以我们可以了解，flag只有7位需要知道了，由于在已知中没有大写字符和数字，我们推测全部都是小写字符（并且如果加上所有字符，那么复杂度是非常大的），下面我们观察对于flag的其他判定规则。经过反复动态调试和确认后，我们可以注意到上下两个图，v10的LODWORD和HIDWORD分别表示了两个开关，当v10不为0但是v10低位为0的时候，才能通过最后的IF判定，所以我们可以确定，下图第一个if的条件是假的，不能成立的。拿到打乱的顺序列表后，我们有z3-solverfrom z3 import * from Crypto.Util.number import * from copy import deepcopy from typing import List def solve(): s = Solver() x = z3_create_bvs("x", 3, 64) v23 = x[0] v24 = x[1] v25 = x[2] v20 = v24 & v23 v19 = (v24 & v23 | v25 & v23) + 65670 v18 = (v25 & v23 ^ v25 & v24) - 1131796 v17 = v24 & v23 ^ v25 & v23 s.add((v24 & v23 & (~(v24 | v23) | v25 & v23 | v25 & v24 & ~v18) | v25 & v24 & v18) != 1732474390) s.add((v23 ^ (v20 & ~v18 | v20 & ~v19 | v17 & v19 | v25 & v23 & ~v18)) == 0x400010000622000) s.add((v18 ^ (v19 - v20)) == 0x2100A0203EFBB8B) s.add((v17 ^ v19 ^ v20) == 0x4083102108E) s.add((v19 ^ v17) - v18 == 0x1551566F3C6485ED) s.add((v18 ^ v19 ^ v25 & v24) == 0x40836ECAB9A) s.add((v17 ^ v20) - v18 == 0x3E51566F3C718563) s.add(v23 - v24 == 0x1AEFF6FDFC121BF1) s.add((v25 + v24 + v23) % 10 == 8) z3_all_bv_is_printable(s, [v23, v24, v25]) v23_s = '*p*qyeam' v24_s = 'sT*u{**R' v25_s = '}CtF*js*' for i in range(8): if v23_s[i] != '*': s.add(v23 & (0xff << (i*8)) == ord(v23_s[i]) << (i*8)) if v24_s[i] != '*': s.add(v24 & (0xff << (i*8)) == ord(v24_s[i]) << (i*8)) if v25_s[i] != '*': s.add(v25 & (0xff << (i*8)) == ord(v25_s[i]) << (i*8)) # answers while s.check() == sat: m = s.model() z3_exclude(s, x, m) result = z3_concat_bv_aslong(x, m).decode() sbox = [15, 17, 9, 19, 12, 8, 21, 23, 13, 20, 5, 7, 3, 22, 1, 2, 0, 10, 14, 18, 4, 11, 6, 16] assert(len(sbox) == len(result)) for i in range(len(result)): print(result[…