安卓 hook 的检测绕过，自定义 linker 加固，控制流混淆，z3
非常综合的一道题，收获良多
java 层
static {
System.loadLibrary("suapp");
}
...
this.binding.validateButton.setOnClickListener(new View.OnClickListener() { // from class: com.swdd.suapp.MainActivity.1
@Override // android.view.View.OnClickListener
public void onClick(View v) {
String input = MainActivity.this.binding.inputField.getText().toString().trim();
if (input.isEmpty()) {
MainActivity.this.binding.inputField.setError("输入不能为空");
} else {
String result = MainActivity.this.check(input);
Toast.makeText(MainActivity.this, result, 1).show();
}
}
});设置的回调是 libsuapp.so 中的 check 函数，查看 so
native 层
frida 检测绕过
__int64 Java_com_swdd_suapp_MainActivty_check(__int64 *a1, __int64 a2, __int64 a3)这是一个假的导出函数（activity 少了个 i），故查看 init 和 JNIonload 函数
在 init 段内有新建线程，注册的函数里有一个 hook 检测：
v5 = sub_227F8("/system/lib64/libc.so");
v6 = sub_22A14(v5, "signal");
v7 = fopen("/system/lib64/libc.so", "rb");
ptr = 0LL;
...
v13 = dlopen("/system/lib64/libc.so", 2);
v14 = dlsym(v13, "signal");
v15 = ptr;
v16 = *v14;
dword_4D5CC = ptr != *v14;
sub_229C0(v5);
...
v19 = v15 == v16 ? 0.0 : 1.0;原理是 frida 会 hook 掉 signal 函数以进行良好的错误处理支持，所以这里通过检测文件中的 signal 函数前 8 个字节是否和用过动态库打开的相同，绕过方法是通过把读 libc.so 的时候 hook 了，让它结果返回的就是 frida 的那个版本
获取 frida 版本的 signal 可以通过 Module.findExportByName("libc.so","signal") 获取，之后 hook fread
function hook_fread_interceptor() {
var memcmp_addr = Module.findExportByName("libc.so", "fread");
if (memcmp_addr !== null) {
console.log("fread address: ", memcmp_addr);
Interceptor.attach(memcmp_addr, {
onEnter: function (args) {
this.buffer = args[0];
},
onLeave: function (retval) {
if (this.count.toInt32() == 8) {
Memory.writeByteArray(this.buffer, [0x50, 0x00, 0x00, 0x58, 0x00, 0x02, 0x1f, 0xd6]);
retval.replace(8);
}
}
});
}
}主要加载逻辑
JNI_OnLoad 注册函数：
v22 = ((*v28)->RegisterNatives)(v28, v14, off_4D080, 2LL);指针指向 start 函数，继续跟踪
v28 = (*a1)->GetStaticMethodID(a1, v18, "getAppDirPath", "(Landroid/content/Context;)Ljava/lang/String;");
// 前面加载了文件app文件路径
memcpy(v68, v59, v67);
v68[v67] = 0;
v70 = std::string::append(&v80, "/files/main");
...
sub_225D4(&v80, v77, qword_4D5C0);sub_225D4 函数实现了一个自定义 linker，我们 pull 下来发现 main 并不能解析，仔细查看其逻辑
__int64 __fastcall sub_225D4(__int64 a1, char *a2, __int64 a3)
{
int v5; // w19
__int64 v6; // x22
__int64 v7; // x0
__off_t v8; // x5
__off_t v9; // x26
size_t v10; // x24
size_t v11; // x22
char *v12; // x0
char *v13; // x23
char v15[48]; // [xsp+8h] [xbp-88h] BYREF
__int64 v16; // [xsp+38h] [xbp-58h]
__int64 v17; // [xsp+88h] [xbp-8h]
v17 = *(_ReadStatusReg(ARM64_SYSREG(3, 3, 13, 0, 2)) + 40);
qword_4D5D0 = a3;
v5 = __open_2(a2, 0LL);
if ( (fstat(v5, v15) & 0x80000000) == 0 )
{
v6 = v16;
if ( v16 >= 37361 )
{
v7 = sysconf(40);
if ( v7 != -1 )
{
v8 = -v7 & 0x91F0LL;
v9 = 37360 - v8;
v10 = v6 - 37360; // 文件偏移
v11 = v6 - v8;
v12 = mmap(0LL, v11, 3, 2, v5, v8);
if ( v12 != -1LL )
{
v13 = v12;
*(a1 + 192) = &v12[v9];
if ( sub_21EE4(a1, a2, v5, 37360LL, v10) && (sub_22124(a1) & 1) != 0 && !mprotect(*(a1 + 184), v10, 7) )
{
sub_2140C(*(a1 + 208));
sub_21950(*(a1 + 208));
sub_21E64(*(a1 + 208));
}
munmap(v13, v11);
}
}
}
}
return close(v5);
}
bool __fastcall sub_21EE4(__int64 a1, char *a2, int a3, __int64 a4, __int64 a5)
{
// [COLLAPSED LOCAL DECLARATIONS. PRESS NUMPAD "+" TO EXPAND]
std::string::assign(a1 + 144, a2);
*a1 = a3;
*(a1 + 8) = a4;
*(a1 + 16) = a5;
v9.n128_u64[0] = 0x3C3C3C3C3C3C3C3CLL;
v9.n128_u64[1] = 0x3C3C3C3C3C3C3C3CLL;
v10 = veorq_s8(xmmword_4D2D0, v9); // 向量操作
xmmword_4D2D0 = v10;
xmmword_4D2E0 = veorq_s8(xmmword_4D2E0, v9);
v11 = xmmword_4D2E0;
xmmword_4D2F0 = veorq_s8(xmmword_4D2F0, v9);
xmmword_4D300[0] = veorq_s8(xmmword_4D300[0], v9);
v12 = xmmword_4D2F0;
v13 = xmmword_4D300[0];
*(a1 + 24) = v10;
*(a1 + 40) = v11;
*(a1 + 56) = v12;
v10.n128_u32[0] = *(a1 + 24);
*(a1 + 72) = v13;
v10.n128_u64[0] = vmvn_s8(vceq_s16((vmovl_u8(v10.n128_u64[0]).n128_u64[0] & 0xFF00FF00FF00FFLL), 0x46004C0045007FLL)).n64_u64[0];
v14 = v10.n128_u8[0] & 1 | (2 * (v10.n128_u8[2] & 1)) & 3 | (4 * (v10.n128_u8[4] & 1)) & 7 | (8 * v10.n128_u8[6]) & 0xF;
if ( !(v10.n128_u8[0] & 1 | (2 * (v10.n128_u8[2] & 1)) & 3 | (4 * (v10.n128_u8[4] & 1)) & 7 | (8 * v10.n128_u8[6]) & 0xF) )
{
...
v27 = mmap64(0LL, v25 + v26, 3, 2, v19, v23);
if ( v27 == -1LL )
{
perror("mmap64 failed");
v28 = 0LL;
}
...
v30 = unk_4D0E0;
v31 = xmmword_4D0F0; // 文件修复
v32 = unk_4D100;
*v28 = xmmword_4D0D0;
*(v28 + 16) = v30;
v33 = xmmword_4D110;
v34 = unk_4D120;
*(v28 + 32) = v31;
*(v28 + 48) = v32;
v35 = xmmword_4D130;
v36 = unk_4D140;
*(v28 + 64) = v33;
*(v28 + 80) = v34;
v37 = xmmword_4D150;
v38 = unk_4D160;
*(v28 + 96) = v35;
*(v28 + 112) = v36;
v39 = xmmword_4D170;
v40 = unk_4D180;
*(v28 + 128) = v37;
*(v28 + 144) = v38;
v41 = xmmword_4D190;
v42 = unk_4D1A0;
*(v28 + 160) = v39;
*(v28 + 176) = v40;
v43 = xmmword_4D1B0;
v44 = unk_4D1C0;一个操作是截短了这个文件，之后是解密文件头（veorq_s8 向量异或操作），赋值
head = [0x43, 0x79, 0x70, 0x7A, 0x3E, 0x3D, 0x3D, 0x3C, 0x3C, 0x3C,
0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3F, 0x3C, 0x8B, 0x3C,
0x3D, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C,
0x3C, 0x3C, 0x7C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C,
0x34, 0x20, 0x3E, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C, 0x3C,
0x3C, 0x3C, 0x7C, 0x3C, 0x04, 0x3C, 0x35, 0x3C, 0x7C, 0x3C,
0x25, 0x3C, 0x24, 0x3C]
for i in range(len(head)):
print("{:#08x}".format(head[i]^0x3c)[-2:],end="")
填入这一部分（和 xmmword_4D0F0 那一堆段表），截去前面就能用 IDA 打开
dd if=main of=ex_main skip=0x91f0 bs=1
或者用 hook，不过之后要修复 so，参考别人的脚本如下
/* Frida Hook Script - libsuapp.so Analysis */
const TARGET_LIB = 'libsuapp.so'; // 目标动态库
const DUMP_DIR = '/sdcard/Download/'; // DUMP文件存储目录
const FRIDA_READ_SIZE = 8; // 目标fread读取字节数
const PATCH_BYTES = [ // 内存Patch数据
0x50, 0x00, 0x00, 0x58,
0x00, 0x02, 0x1F, 0xD6
];
let randCodeBuffer = []; // 随机码存储缓冲区
/**
* Hook fread调用并进行内存修改
*/
function hookFread() {
const freadSymbol = Module.findExportByName('libc.so', 'fread');
if (!freadSymbol) {
console.error('[ERROR] fread symbol not found!');
return;
}
console.log(`[+] fread address: ${freadSymbol}`);
Interceptor.attach(freadSymbol, {
onEnter(args) {
// 参数索引：
// 0 - buffer指针, 1 - size, 2 - count, 3 - stream
this.targetBuffer = args[0];
this.readCount = args[2].toInt32();
},
onLeave(retval) {
if (this.readCount === FRIDA_READ_SIZE) {
console.log(`[*] Patching fread buffer at ${this.targetBuffer}`);
Memory.writeByteArray(this.targetBuffer, PATCH_BYTES);
retval.replace(FRIDA_READ_SIZE); // 强制返回成功读取数
}
}
});
}
/**
* Dump指定模块到文件系统
* @param {string} moduleName - 目标模块名
*/
function dumpModule(moduleName) {
const targetModule = Process.getModuleByName(moduleName);
if (!targetModule) {
console.error(`[ERROR] Module ${moduleName} not found!`);
return;
}
console.log(`\n[+] Dumping module: ${targetModule.name}`);
console.log(` Base: ${targetModule.base}`);
console.log(` Size: ${targetModule.size}`);
console.log(` Path: ${targetModule.path}`);
const dumpPath = `${DUMP_DIR}${targetModule.name}_${targetModule.base}_${targetModule.size}.so`;
try {
const fileHandle = new File(dumpPath, 'wb');
Memory.protect(targetModule.base, targetModule.size, 'rwx');
const moduleBuffer = targetModule.base.readByteArray(targetModule.size);
fileHandle.write(moduleBuffer);
fileHandle.flush();
fileHandle.close();
console.log(`[SUCCESS] Module dumped to: ${dumpPath}`);
} catch (e) {
console.error(`[ERROR] Dump failed: ${e.message}`);
}
}
/**
* 主Hook入口：监控动态库加载
*/
function monitorDynamicLoading() {
const dlopenExtSymbol = Module.findExportByName(null, 'android_dlopen_ext');
if (!dlopenExtSymbol) {
console.error('[ERROR] android_dlopen_ext not found!');
return;
}
Interceptor.attach(dlopenExtSymbol, {
onEnter(args) {
const loadedPath = args[0].readCString();
this.shouldHook = loadedPath.includes('suapp');
if (this.shouldHook) {
console.log(`\n[+] Target library loaded: ${loadedPath}`);
}
},
onLeave() {
if (this.shouldHook) {
hookFread();
dumpModule(TARGET_LIB); // 自动Dump目标模块
}
}
});
}
setImmediate(() => {
console.log('[+] Frida script initialized');
monitorDynamicLoading();
});之后修复
./SoFixer-macOS-64 -s ./libsuapp.so_0x7c0230e000_0x25000\ copy.so -o new_fixed_so.so -m 0x7c0230e000 -d
不知道为什么这里我总是修复失败，BL 的时候总是识别不到，还是静态搞定了
ELF 文件层
init 的部分初始化了 S 盒，
v16 = *(_QWORD *)(_ReadStatusReg(ARM64_SYSREG(3, 3, 13, 0, 2)) + 40);
memset(v15, 0, sizeof(v15));
qmemcpy(v15, "SUCTF", 5);
v14 = xmmword_31D0;
memset(v13, 0, sizeof(v13));
__strncpy_chk2(v13, v15, 64LL, 64LL, 256LL);
sub_84B0((int *)&v14, (__int64)v13);
__memset_chk(storedBytes, 0LL, 256LL, 256LL);
for ( i = 0; i <= 15; ++i )
{
if ( i >= 0 )
v0 = i;
else
v0 = i + 3;
storedBytes[i] = *((_DWORD *)&v15[-1] + (v0 >> 2)) >> (8 * (i - (v0 & 0xFC)));
}
for ( j = 0; j <= 15; ++j )
sub_9A68((__int64)&hashString + 2 * j, -1LL, (__int64)"%02x", storedBytes[j]);
byte_23AD0 = 0;
memset(v12, 0, sizeof(v12));
__strcpy_chk(v12, &hashString, 64LL);
v8 = __strlen_chk((const char *)v12, 0x40uLL);
v5 = 0;
memset(v11, 0, sizeof(v11));
for ( k = 0; k <= 255; ++k )
{
Sbox[k] = k;
*((_BYTE *)v11 + k) = *((_BYTE *)v12 + k % v8);
}
for ( m = 0; m <= 255; ++m )
{
v1 = v5 + Sbox[m] + *((unsigned __int8 *)v11 + m);
v2 = v1 + 255;
if ( v1 >= 0 )
v2 = v5 + Sbox[m] + *((unsigned __int8 *)v11 + m);
v5 = v1 - (v2 & 0xFFFFFF00);
v4 = Sbox[m];
Sbox[m] = Sbox[v5];
Sbox[v5] = v4;
}之后通过 RC4 这个 RPG 来生成控制流
这是一个 Java 本地方法实现的校验函数，用于验证输入字符串是否通过动态生成的加密运算链，最终结果与预设值匹配。属于典型的白盒加密验证实现。
-
operation_functions_struct：
- 包含函数指针和参数数量的结构体数组
- 通过
v17 = *((_OWORD *)&operation_functions_struct + v7)获取函数指针 - 通过
v4 = *(&operation_functions_struct + 2 * v7 + 1)获取参数数量
-
results 数组：
- 存储最终比对的标准结果
- 通过
*((_DWORD *)&results + m)进行结果比对
operation_function_struct 长这样：第一个是函数指针，第二个是参数数量
__int64 __fastcall Java_com_swdd_suapp_MainActivity_check(_JNIEnv *a1, __int64 a2, __int64 a3)
{
v34 = *(_QWORD *)(_ReadStatusReg(ARM64_SYSREG(3, 3, 13, 0, 2)) + 40);
ii = 0;
jj = 0;
memset(s, 0, sizeof(s));
StringUTFChars = (const char *)_JNIEnv::GetStringUTFChars(a1, a3, 0LL);
if ( !StringUTFChars )
{
v16 = _JNIEnv::NewStringUTF(a1, "Failed to get input string.");
goto LABEL_34;
}
v12 = __strlen_chk(StringUTFChars, 0xFFFFFFFFFFFFFFFFLL);
if ( v12 >= 64 )
{
v16 = _JNIEnv::NewStringUTF(a1, "Toooooooo Mannnnnny!");
goto LABEL_34;
}
for ( i = 0; i < v12; ++i )
s[i] = (unsigned __int8)StringUTFChars[i];
for ( j = 0; j < 8 * v12; ++j )
{
v20 = sub_A158(); // RC4
v19 = sub_A158();
v18 = sub_A158();
v9 = (int)sub_A158() % v12; // 32
v8 = (int)sub_A158() % v12;
v7 = (unsigned __int8)sub_A158();
v17 = *((_OWORD *)&operation_functions_struct + v7);
v4 = (unsigned int)*(&operation_functions_struct + 2 * v7 + 1);
if ( DWORD2(v17) == 1 )
{
v28 = &ffi_type_uint32;
v29 = &ffi_type_uint32;
v30 = &ffi_type_uint32;
v23 = &v20;
v24 = &s[v9];
v25 = &s[v8];
if ( (unsigned int)ffi_prep_cif(v22, 1LL, 3LL) )
{
_JNIEnv::ReleaseStringUTFChars(a1, a3, StringUTFChars);
v16 = _JNIEnv::NewStringUTF(a1, "Failed to prepare function1 call.");
goto LABEL_34;
}
}
else if ( v4 == 2 )
{
v28 = &ffi_type_uint32;
v29 = &ffi_type_uint32;
v30 = &ffi_type_uint32;
v31 = &ffi_type_uint32;
v23 = &v20;
v24 = &v19;
v25 = &s[v9];
v26 = &s[v8];
if ( (unsigned int)ffi_prep_cif(v22, 1LL, 4LL) )
{
_JNIEnv::ReleaseStringUTFChars(a1, a3, StringUTFChars);
v16 = _JNIEnv::NewStringUTF(a1, "Failed to prepare function2 call.");
goto LABEL_34;
}
}
else
{
if ( v4 != 3 )
{
__android_log_print(4, "SUAPP", "Invalid parameter count: %d", DWORD2(v17));
continue;
}
v28 = &ffi_type_uint32;
v29 = &ffi_type_uint32;
v30 = &ffi_type_uint32;
v31 = &ffi_type_uint32;
v32 = &ffi_type_uint32;
v23 = &v20;
v24 = &v19;
v25 = &v18;
v26 = &s[v9];
v27 = &s[v8];
if ( (unsigned int)ffi_prep_cif(v22, 1LL, 5LL) )
{
_JNIEnv::ReleaseStringUTFChars(a1, a3, StringUTFChars);
v16 = _JNIEnv::NewStringUTF(a1, "Failed to prepare function3 call.");
goto LABEL_34;
}
}
ffi_call(v22, v17, &v21, &v23);
s[v9] = v21;
}
_JNIEnv::ReleaseStringUTFChars(a1, a3, StringUTFChars);
if ( v12 == 32 )
{
for ( m = 0; m < 32; ++m )
{
if ( s[m] != *((_DWORD *)&results + m) )
{
v16 = _JNIEnv::NewStringUTF(a1, "Try Again.");
goto LABEL_34;
}
}
v16 = _JNIEnv::NewStringUTF(a1, "Good Job.");
}
else
{
v16 = _JNIEnv::NewStringUTF(a1, "Nonono!");
}
LABEL_34:
_ReadStatusReg(ARM64_SYSREG(3, 3, 13, 0, 2));
return v16;
}
__int64 sub_9A68(__int64 a1, __int64 a2, __int64 a3, ...)
{
gcc_va_list va1; // [xsp+E0h] [xbp-50h] BYREF
gcc_va_list va; // [xsp+108h] [xbp-28h] BYREF
__int64 v6; // [xsp+128h] [xbp-8h]
va_start(va, a3);
v6 = *(_QWORD *)(_ReadStatusReg(ARM64_SYSREG(3, 3, 13, 0, 2)) + 40);
va_copy(va1, va);
return (unsigned int)__vsprintf_chk(a1, 0LL, a2, a3, va1);
}ffi_prep_cif - 为下文的 ffi_call 准备 ffi_cif structure
我们通过 hook 这个 sub_A158 获取控制流数据
/**
* Hook目标Native函数
*/
function hookNativeFunctions() {
const moduleBase = Module.getBaseAddress(TARGET_LIB);
console.log(`\n[+] ${TARGET_LIB} base: ${moduleBase}`);
// Hook 随机数生成函数
const RAND_GEN_OFFSET = ptr('0xA158');
Interceptor.attach(moduleBase.add(RAND_GEN_OFFSET), {
onLeave(retval) {
randCodeBuffer.push(retval.toInt32());
}
});
// inline Hook 结果处理部分
const RESULT_HANDLER_OFFSET = ptr('0x9FA8');
Interceptor.attach(moduleBase.add(RESULT_HANDLER_OFFSET), {
onEnter() {
console.log('\n[+] Intercepted result handler:');
console.log(` RandCode count: ${randCodeBuffer.length}`);
console.log(JSON.stringify(randCodeBuffer, null, 2));
// 清空缓冲区
randCodeBuffer = [];
}
});
}之后就是 IDA 脚本和苦力时间……不过作者给出了一个相对没这么折磨的思路：
- 可以观察到这些函数不是完全不同的，可以通过检查哈希来去重。可以看到只有 14 种情况（好吧）
- 然后就模拟整个过程把第一个 randnum 映射到 14 种情况中，然后 print 一个正常的语句给 z3
不过我觉得应该可以用 unidbg 这种东西来试试模拟出来整个过程
解题脚本
最后贴出作者给出的脚本吧（好大的代码量）
import idaapi
import idautils
import hashlib
import re # 导入正则表达式模块
# 获取函数的字节码（字节序列）
def get_function_bytes(func_start):
func = idaapi.get_func(func_start)
func_end = func.end_ea # 使用 end_ea 获取函数结束地址
func_bytes = bytearray()
for addr in range(func_start, func_end):
func_bytes.append(idaapi.get_byte(addr)) # 使用 idaapi.get_byte 获取字节
return func_bytes
# 计算字节码的哈希值作为相似度的度量
def get_function_hash(func_start):
func_bytes = get_function_bytes(func_start)
return hashlib.md5(func_bytes).hexdigest()
# 获取所有符合条件（__Z8func_*）函数的哈希值，并提取数字
def get_all_functions():
functions = {}
func_pattern = re.compile(r'func_(\d+)') # 修改正则表达式，匹配 __Z8func_ 后面跟数字
for func_start in idautils.Functions():
func_name = idaapi.get_func_name(func_start)
# 检查函数名是否符合 "__Z8func_*" 格式
match = func_pattern.search(func_name)
if match:
func_number = int(match.group(1)) # 提取函数名中的数字部分
func_hash = get_function_hash(func_start) # 计算哈希值
if func_hash not in functions:
functions[func_hash] = [] # 如果没有该哈希的组，则创建一个新组
functions[func_hash].append(func_number) # 将函数的数字加入对应哈希的组中
return functions
# 输出相同哈希的函数数字组
def print_functions_by_hash(functions):
count = 1
for func_hash, func_numbers in functions.items():
# 输出哈希值和对应的数字数组3
print(f"type{count}: {sorted(func_numbers)}")
count += 1
# 主函数
def main():
functions = get_all_functions() # 获取所有函数并按哈希分组
print_functions_by_hash(functions) # 输出按哈希分组的数字数组
# 运行主函数
if __name__ == "__main__":
main()#include <bits/stdc++.h>
using namespace std;
// 各种类型的操作函数
void type1(int a1, int a2, int a3, int a4) {
// a4 + a3 + a1 + a2;
printf("a[%d] = a[%d] + a[%d] + %d + %d;\n", a3, a4, a3, a1, a2);
}
void type2(int a1, int a2, int a3, int a4, int a5) {
// (a5 ^ (a3 + a1 + a4)) + a2
printf("a[%d] = (a[%d] ^ (%d + %d + a[%d])) + %d;\n", a4, a5, a3, a1, a4, a2);
}
void type3(int a1, int a2, int a3, int a4, int a5) {
// a5 + a4 + a3 + a1 + a2
printf("a[%d] = a[%d] + a[%d] + %d + %d + %d;\n", a4, a5, a4, a3, a2, a1);
}
void type4(int a1, int a2, int a3) {
// (a3 ^ a1) + a2;
printf("a[%d] = (a[%d] ^ %d) + a[%d];\n", a2, a3, a1, a2);
}
void type5(int a1, int a2, int a3, int a4) {
// (a1 ^ (a3 + a4)) + a2
printf("a[%d] = (%d ^ (a[%d] + a[%d])) + %d;\n", a3, a1, a3, a4, a2);
}
void type6(int a1, int a2, int a3, int a4) {
// (a4 ^ a3 ^ a1) + a2;
printf("a[%d] = (a[%d] ^ a[%d] ^ %d) + %d;\n", a3, a4, a3, a1, a2);
}
void type7(int a1, int a2, int a3, int a4) {
// (a4 ^ (a1 + a3)) + a2;
printf("a[%d] = (a[%d] ^ (%d + a[%d])) + %d;\n", a3, a4, a1, a3, a2);
}
void type8(int a1, int a2, int a3) {
// a3 + a1 + a2;
printf("a[%d] = a[%d] + %d + a[%d];\n", a2, a3, a1, a2);
}
void type9(int a1, int a2, int a3, int a4, int a5) {
// (a3 ^ a1 ^ (a4 + a5)) + a2
printf("a[%d] = (%d ^ %d ^ (a[%d] + a[%d])) + %d;\n", a4, a3, a1, a4, a5, a2);
}
void type10(int a1, int a2, int a3, int a4, int a5) {
// (a1 ^ (a4 + a3 + a5)) + a2;
printf("a[%d] = (%d ^ (a[%d] + %d + a[%d])) + %d;\n", a4, a1, a4, a3, a5, a2);
}
void type11(int a1, int a2, int a3, int a4, int a5) {
// ((a4 + a5) ^ (a1 + a3)) + a2;
printf("a[%d] = ((a[%d] + a[%d]) ^ (%d + %d)) + %d;\n", a4, a4, a5, a1, a3, a2);
}
void type12(int a1, int a2, int a3, int a4, int a5) {
// (a5 ^ a4 ^ a3 ^ a1) + a2;
printf("a[%d] = (a[%d] ^ a[%d] ^ %d ^ %d) + %d;\n", a4, a5, a4, a3, a1, a2);
}
void type13(int a1, int a2, int a3, int a4, int a5) {
// (a5 ^ a1 ^ (a3 + a4)) + a2;
printf("a[%d] = (a[%d] ^ %d ^ (%d + a[%d])) + %d;\n", a4, a5, a1, a3, a4, a2);
}
void type14(int a1, int a2, int a3, int a4, int a5) {
// (a5 ^ a4 ^ (a1 + a3)) + a2;
printf("a[%d] = (a[%d] ^ a[%d] ^ (%d + %d)) + %d;\n", a4, a5, a4, a1, a3, a2);
}
vector<int> type1e = {0, 2, 11, 12, 15, 21, 26, 28, 39, 44, 53, 57, 62, 63, 72, 74, 77, 81, 90, 94, 97, 108, 113, 118, 121, 122, 125, 142, 144, 145, 151, 161, 162, 166, 181, 183, 185, 192, 199, 203, 215, 226, 230, 238, 242, 244, 247};
vector<int> type21 = {1, 5, 34, 49, 84, 93, 130, 152, 154, 155, 207, 216, 217};
vector<int> type31 = {3, 20, 24, 38, 42, 64, 70, 71, 73, 82, 124, 132, 176, 189, 196, 209, 220, 223, 224, 225, 237, 255};
vector<int> type41 = {4, 9, 10, 14, 22, 23, 25, 31, 32, 33, 45, 69, 92, 99, 103, 111, 115, 117, 129, 147, 149, 150, 156, 164, 165, 172, 175, 241, 250, 254};
vector<int> type51 = {6, 7, 29, 46, 47, 51, 60, 65, 76, 80, 85, 88, 98, 177, 182, 193, 208, 210, 221, 222, 236};
vector<int> type61 = {8, 50, 54, 89, 126, 133, 198, 219, 240};
vector<int> type71 = {13, 48, 55, 106, 119, 120, 127, 148, 170, 171, 197, 218, 233, 248, 252, 253};
vector<int> type81 = {16, 17, 19, 30, 35, 36, 37, 43, 56, 59, 67, 68, 78, 79, 96, 100, 101, 107, 112, 114, 116, 123, 131, 135, 138, 139, 143, 158, 159, 160, 163, 167, 168, 169, 173, 178, 180, 188, 191, 194, 195, 204, 205, 211, 212, 227, 228, 229, 234, 235, 245, 249, 251};
vector<int> type91 = {18, 134, 136, 140, 174, 213, 232};
vector<int> type101 = {27, 58, 86, 104, 110, 146, 157, 179, 184, 202, 239, 243, 246};
vector<int> type111 = {40, 52, 66, 95, 109, 128, 141, 153, 206, 231};
vector<int> type121 = {41, 87, 200, 201};
vector<int> type131 = {61, 91, 102, 137, 186, 187, 190, 214};
vector<int> type141 = {75, 83, 105};
// 类型查找函数，根据opcode选择对应的类型
int getType(int opcode) {
if (find(type1e.begin(), type1e.end(), opcode) != type1e.end()) return 1;
if (find(type21.begin(), type21.end(), opcode) != type21.end()) return 2;
if (find(type31.begin(), type31.end(), opcode) != type31.end()) return 3;
if (find(type41.begin(), type41.end(), opcode) != type41.end()) return 4;
if (find(type51.begin(), type51.end(), opcode) != type51.end()) return 5;
if (find(type61.begin(), type61.end(), opcode) != type61.end()) return 6;
if (find(type71.begin(), type71.end(), opcode) != type71.end()) return 7;
if (find(type81.begin(), type81.end(), opcode) != type81.end()) return 8;
if (find(type91.begin(), type91.end(), opcode) != type91.end()) return 9;
if (find(type101.begin(), type101.end(), opcode) != type101.end()) return 10;
if (find(type111.begin(), type111.end(), opcode) != type111.end()) return 11;
if (find(type121.begin(), type121.end(), opcode) != type121.end()) return 12;
if (find(type131.begin(), type131.end(), opcode) != type131.end()) return 13;
if (find(type141.begin(), type141.end(), opcode) != type141.end()) return 14;
return -1; // 未找到类型
}
unsigned char opcode[9999] = {
197, 209, 172, 235, 111, 151, 86, 73, 250, 217, 100, 170, 148, 158, 131, 38, 12, 91, 144, 225, 179, 115, 215, 28, 179, 62, 108, 138, 151, 151, 187, 180, 121, 23, 144, 41, 58, 174, 213, 108, 23, 86, 95, 152, 140, 85, 168, 160, 126, 128, 125, 129, 83, 19, 219, 109, 9, 68, 177, 83, 60, 167, 228, 182, 146, 173, 109, 238, 105, 46, 30, 2, 72, 123, 40, 146, 148, 254, 10, 45, 146, 143, 152, 220, 23, 51, 201, 211, 238, 50, 140, 155, 78, 110, 148, 51, 89, 209, 57, 149, 77, 50, 187, 168, 180, 117, 19, 238, 47, 229, 177, 104, 182, 57, 159, 248, 46, 100, 172, 210, 27, 137, 255, 61, 211, 110, 93, 198, 226, 103, 80, 168, 206, 11, 188, 164, 12, 61, 33, 141, 229, 136, 231, 197, 178, 150, 8, 184, 203, 194, 35, 97, 45, 205, 72, 116, 215, 169, 230, 243, 183, 38, 201, 126, 174, 101, 27, 100, 107, 185, 68, 124, 19, 235, 111, 196, 48, 186, 220, 75, 132, 101, 111, 172, 60, 164, 163, 152, 192, 128, 99, 25, 117, 27, 167, 48, 163, 227, 84, 217, 28, 160, 24, 54, 211, 217, 68, 51, 189, 214, 29, 42, 80, 152, 13, 160, 228, 37, 117, 142, 92, 189, 208, 62, 141, 137, 246, 93, 202, 90, 175, 126, 59, 72, 0, 126, 7, 84, 136, 111, 57, 129, 105, 60, 65, 98, 210, 217, 96, 47, 92, 68, 79, 177, 85, 78, 42, 1, 123, 175, 81, 177, 183, 139, 146, 255, 228, 254, 242, 28, 84, 120, 50, 57, 1, 183, 55, 102, 1, 212, 15, 152, 154, 169, 10, 134, 55, 252, 15, 104, 98, 165, 255, 46, 250, 125, 215, 225, 68, 165, 255, 177, 86, 210, 104, 0, 249, 168, 101, 207, 53, 224, 218, 128, 152, 0, 222, 95, 94, 241, 65, 69, 82, 180, 98, 170, 194, 105, 128, 25, 166, 46, 65, 239, 165, 179, 206, 32, 29, 250, 72, 107, 104, 45, 175, 116, 36, 59, 144, 115, 254, 215, 196, 168, 202, 81, 201, 191, 183, 96, 160, 241, 68, 220, 244, 114, 94, 235, 60, 101, 87, 189, 50, 253, 190, 122, 99, 162, 149, 19, 128, 38, 177, 171, 34, 198, 195, 159, 103, 162, 35, 249, 222, 210, 148, 8, 65, 253, 109, 90, 241, 17, 237, 142, 143, 106, 139, 28, 7, 167, 247, 249, 152, 132, 22, 190, 233, 163, 113, 54, 234, 119, 132, 144, 89, 79, 231, 9, 172, 253, 39, 189, 230, 211, 123, 225, 37, 147, 51, 55, 152, 34, 196, 224, 252, 161, 68, 209, 67, 74, 119, 212, 130, 17, 43, 55, 88, 72, 141, 254, 137, 54, 30, 38, 71, 232, 74, 72, 229, 3, 118, 115, 110, 233, 45, 60, 241, 101, 178, 141, 197, 244, 73, 217, 142, 230, 241, 231, 202, 222, 82, 242, 138, 185, 226, 8, 191, 201, 154, 183, 7, 50, 137, 34, 138, 139, 114, 162, 49, 117, 173, 168, 197, 209, 172, 235, 111, 151, 86, 73, 250, 217, 100, 170, 148, 158, 131, 38, 12, 91, 144, 225, 179, 115, 215, 28, 179, 62, 108, 138, 151, 151, 187, 180, 121, 23, 144, 41, 58, 174, 213, 108, 23, 86, 95, 152, 140, 85, 168, 160, 126, 128, 125, 129, 83, 19, 219, 109, 9, 68, 177, 83, 60, 167, 228, 182, 146, 173, 109, 238, 105, 46, 30, 2, 72, 123, 40, 146, 148, 254, 10, 45, 146, 143, 152, 220, 23, 51, 201, 211, 238, 50, 140, 155, 78, 110, 148, 51, 89, 209, 57, 149, 77, 50, 187, 168, 180, 117, 19, 238, 47, 229, 177, 104, 182, 57, 159, 248, 46, 100, 172, 210, 27, 137, 255, 61, 211, 110, 93, 198, 226, 103, 80, 168, 206, 11, 188, 164, 12, 61, 33, 141, 229, 136, 231, 197, 178, 150, 8, 184, 203, 194, 35, 97, 45, 205, 72, 116, 215, 169, 230, 243, 183, 38, 201, 126, 174, 101, 27, 100, 107, 185, 68, 124, 19, 235, 111, 196, 48, 186, 220, 75, 132, 101, 111, 172, 60, 164, 163, 152, 192, 128, 99, 25, 117, 27, 167, 48, 163, 227, 84, 217, 28, 160, 24, 54, 211, 217, 68, 51, 189, 214, 29, 42, 80, 152, 13, 160, 228, 37, 117, 142, 92, 189, 208, 62, 141, 137, 246, 93, 202, 90, 175, 126, 59, 72, 0, 126, 7, 84, 136, 111, 57, 129, 105, 60, 65, 98, 210, 217, 96, 47, 92, 68, 79, 177, 85, 78, 42, 1, 123, 175, 81, 177, 183, 139, 146, 255, 228, 254, 242, 28, 84, 120, 50, 57, 1, 183, 55, 102, 1, 212, 15, 152, 154, 169, 10, 134, 55, 252, 15, 104, 98, 165, 255, 46, 250, 125, 215, 225, 68, 165, 255, 177, 86, 210, 104, 0, 249, 168, 101, 207, 53, 224, 218, 128, 152, 0, 222, 95, 94, 241, 65, 69, 82, 180, 98, 170, 194, 105, 128, 25, 166, 46, 65, 239, 165, 179, 206, 32, 29, 250, 72, 107, 104, 45, 175, 116, 36, 59, 144, 115, 254, 215, 196, 168, 202, 81, 201, 191, 183, 96, 160, 241, 68, 220, 244, 114, 94, 235, 60, 101, 87, 189, 50, 253, 190, 122, 99, 162, 149, 19, 128, 38, 177, 171, 34, 198, 195, 159, 103, 162, 35, 249, 222, 210, 148, 8, 65, 253, 109, 90, 241, 17, 237, 142, 143, 106, 139, 28, 7, 167, 247, 249, 152, 132, 22, 190, 233, 163, 113, 54, 234, 119, 132, 144, 89, 79, 231, 9, 172, 253, 39, 189, 230, 211, 123, 225, 37, 147, 51, 55, 152, 34, 196, 224, 252, 161, 68, 209, 67, 74, 119, 212, 130, 17, 43, 55, 88, 72, 141, 254, 137, 54, 30, 38, 71, 232, 74, 72, 229, 3, 118, 115, 110, 233, 45, 60, 241, 101, 178, 141, 197, 244, 73, 217, 142, 230, 241, 231, 202, 222, 82, 242, 138, 185, 226, 8, 191, 201, 154, 183, 7, 50, 137, 34, 138, 139, 114, 162, 49, 117, 173, 168, 197, 209, 172, 235, 111, 151, 86, 73, 250, 217, 100, 170, 148, 158, 131, 38, 12, 91, 144, 225, 179, 115, 215, 28, 179, 62, 108, 138, 151, 151, 187, 180, 121, 23, 144, 41, 58, 174, 213, 108, 23, 86, 95, 152, 140, 85, 168, 160, 126, 128, 125, 129, 83, 19, 219, 109, 9, 68, 177, 83, 60, 167, 228, 182, 146, 173, 109, 238, 105, 46, 30, 2, 72, 123, 40, 146, 148, 254, 10, 45, 146, 143, 152, 220, 23, 51, 201, 211, 238, 50, 140, 155, 78, 110, 148, 51, 89, 209, 57, 149, 77, 50, 187, 168, 180, 117, 19, 238, 47, 229, 177, 104, 182, 57, 159, 248, 46, 100, 172, 210, 27, 137, 255, 61, 211, 110, 93, 198, 226, 103, 80, 168, 206, 11, 188, 164, 12, 61, 33, 141, 229, 136, 231, 197, 178, 150, 8, 184, 203, 194, 35, 97, 45, 205, 72, 116, 215, 169, 230, 243, 183, 38, 201, 126, 174, 101, 27, 100, 107, 185, 68, 124, 19, 235, 111, 196, 48, 186, 220, 75, 132, 101, 111, 172, 60, 164, 163, 152, 192, 128, 99, 25, 117, 27, 167, 48, 163, 227, 84, 217, 28, 160, 24, 54, 211, 217, 68, 51, 189, 214, 29, 42, 80, 152, 13, 160, 228, 37, 117, 142, 92, 189, 208, 62, 141, 137, 246, 93, 202, 90, 175, 126, 59, 72, 0, 126, 7, 84, 136, 111, 57, 129, 105, 60, 65, 98, 210, 217, 96, 47, 92, 68, 79, 177, 85, 78, 42, 1, 123, 175, 81, 177, 183, 139, 146, 255, 228, 254, 242, 28, 84, 120, 50, 57, 1, 183, 55, 102, 1, 212, 15, 152, 154, 169, 10, 134, 55, 252, 15, 104, 98, 165, 255, 46, 250, 125, 215, 225, 68, 165, 255, 177, 86, 210, 104, 0, 249, 168, 101, 207, 53, 224, 218, 128, 152, 0, 222, 95, 94, 241, 65, 69, 82, 180, 98, 170, 194, 105, 128, 25, 166, 46, 65, 239, 165, 179, 206, 32, 29, 250, 72, 107, 104, 45, 175, 116, 36, 59, 144, 115, 254, 215, 196, 168, 202, 81, 201, 191, 183, 96, 160, 241, 68, 220, 244, 114, 94, 235, 60, 101, 87, 189, 50, 253, 190, 122, 99, 162, 149, 19, 128, 38, 177, 171, 34, 198, 195, 159, 103, 162, 35, 249, 222, 210, 148, 8, 65, 253, 109, 90, 241, 17, 237, 142, 143, 106, 139, 28, 7, 167, 247, 249, 152, 132, 22, 190, 233, 163, 113, 54, 234, 119, 132, 144, 89, 79, 231, 9, 172, 253, 39, 189, 230, 211, 123, 225, 37, 147, 51, 55, 152, 34, 196, 224, 252, 161, 68, 209, 67, 74, 119, 212, 130, 17, 43, 55, 88, 72, 141, 254, 137, 54, 30, 38, 71, 232, 74, 72, 229, 3, 118, 115, 110, 233, 45, 60, 241, 101, 178, 141, 197, 244, 73, 217, 142, 230, 241, 231, 202, 222, 82, 242, 138, 185, 226, 8, 191, 201, 154, 183, 7, 50, 137, 34, 138, 139, 114, 162, 49, 117, 173, 168
};
int main() {
for (int i = 0; i < 1536; i += 6) {
int a = opcode[i], b = opcode[i + 1], c = opcode[i + 2];
int indexA = opcode[i + 3] % 32;
int indexB = opcode[i + 4] % 32;
int logic = opcode[i + 5];
switch (getType(logic)) {
case 1:
type1(a, b, indexA, indexB);
break;
case 2:
type2(a, b, c, indexA, indexB);
break;
case 3:
type3(a, b, c, indexA, indexB);
break;
case 4:
type4(a, indexA, indexB);
break;
case 5:
type5(a, b, indexA, indexB);
break;
case 6:
type6(a, b, indexA, indexB);
break;
case 7:
type7(a, b, indexA, indexB);
break;
case 8:
type8(a, indexA, indexB);
break;
case 9:
type9(a, b, c, indexA, indexB);
break;
case 10:
type10(a, b, c, indexA, indexB);
break;
case 11:
type11(a, b, c, indexA, indexB);
break;
case 12:
type12(a, b, c, indexA, indexB);
break;
case 13:
type13(a, b, c, indexA, indexB);
break;
case 14:
type14(a, b, c, indexA, indexB);
break;
default:
cout << "Unknown logic type: " << logic << endl;
}
}
}import re
from z3 import *
def translate_transformation(line):
"""
Translates a single C++ transformation line into a Python Z3 constraint.
Args:
line (str): A line of C++ code representing a transformation.
Returns:
str: A line of Python code formatted for Z3.
"""
# Remove any trailing semicolon and whitespace
line = line.strip().rstrip(';')
# Match the pattern a[index] = expression
match = re.match(r'a\[(\d+)\]\s*=\s*(.+)', line)
if not match:
raise ValueError(f"Invalid transformation line: {line}")
index = match.group(1)
expression = match.group(2)
# Function to replace integers with BitVecVal(x, 32), excluding indices in a[index]
def replace_int_literals(match):
num = match.group(0)
# If the number is part of 'a[number]', return as is
if match.group(1):
return num
else:
return f'BitVecVal({num}, 32)'
# Regular expression to find integer literals not preceded by 'a['
# This uses a negative lookbehind to ensure numbers inside a[...] are not matched
int_literal_pattern = re.compile(r'(?<!a\[)\b(0x[0-9a-fA-F]+|\d+)\b')
# Replace all integer literals not inside a[...] with BitVecVal(x, 32)
processed_expression = int_literal_pattern.sub(replace_int_literals, expression)
# Construct the Python assignment statement
python_line = f'a[{index}] = {processed_expression}'
return python_line
def translate_transformations(cpp_transformations):
"""
Translates multiple C++ transformation lines into Python Z3 constraints.
Args:
cpp_transformations (str): Multiline string of C++ transformation lines.
Returns:
list: List of Python Z3 constraint lines.
"""
python_constraints = []
for line in cpp_transformations.strip().split('\n'):
# Remove comments
line = line.split('//')[0]
# Skip empty lines or lines that do not contain transformations
if not line.strip() or not line.strip().startswith('a['):
continue
python_line = translate_transformation(line)
python_constraints.append(python_line)
return python_constraints
def generate_z3_script(transformation_constraints, results, input_size=32):
"""
Generates the complete Z3 Python script with the given constraints.
Args:
transformation_constraints (list): List of Python Z3 constraint lines.
results (list): List of expected result values.
input_size (int): Size of the input array.
Returns:
str: The complete Python Z3 script as a string.
"""
script_lines = [
"from z3 import *",
"",
"# Initialize Z3 solver",
"s = Solver()",
"",
"# Define input characters as 8-bit BitVec variables",
f"input_vars = [BitVec(f'c{{i}}', 8) for i in range({input_size})]",
"",
"# Initialize array 'a' with {0} elements, initially set to input characters".format(input_size),
f"a = [ZeroExt(24, input_vars[i]) for i in range({input_size})]",
"",
"# Translated Python Z3 Constraints"
]
# Add transformation constraints
for constraint in transformation_constraints:
script_lines.append(constraint)
# Define the results array
script_lines.extend([
"",
"# Define the results array",
"results = [",
])
# Format results as hex for readability
for res in results:
script_lines.append(f" 0x{res:x},")
script_lines.append("]")
# Add constraints that a[i] == results[i]
script_lines.append("")
script_lines.append("# After all transformations, set constraints that a[i] == results[i]")
script_lines.append("for i in range({0}):".format(input_size))
script_lines.append(" s.add(a[i] == results[i])")
# Add constraints for input characters to be printable ASCII (optional)
script_lines.append("")
script_lines.append("# Add constraints for input characters to be printable ASCII (optional)")
script_lines.append("for c in input_vars:")
script_lines.append(" s.add(c >= 32, c <= 126) # Printable ASCII range")
# Add the solver check and model extraction
script_lines.extend([
"",
"# Check if the constraints are satisfiable",
"if s.check() == sat:",
" model = s.model()",
" # Extract the input string",
" input_string = ''.join([chr(model[c].as_long()) for c in input_vars])",
" print(f\"Found input: {input_string}\")",
"else:",
" print(\"No solution found.\")",
""
])
return '\n'.join(script_lines)
# Example usage
if __name__ == "__main__":
cpp_transformations = """
a[11] = a[15] + a[11] + 197 + 209;
a[25] = (a[4] ^ (86 + a[25])) + 73;
...
a[2] = a[10] + 7 + a[2];
a[21] = a[13] + 114 + a[21];
"""
results = [
0xd7765, 0x11ebd, 0x32d12, 0x13778, 0x8a428,
0xb592, 0x3fa57, 0x1616, 0x3659e, 0x2483a,
0x2882, 0x508f4, 0xbad, 0x27920, 0xf821,
0x19f83, 0xf97, 0x33904, 0x170d5, 0x16c,
0xcf5d, 0x280d2, 0xa8ade, 0x9eaa, 0x9dab,
0x1f45e, 0x3214, 0x52fa, 0x6d57a, 0x460ed,
0x124ff, 0x13936
]
translated_constraints = translate_transformations(cpp_transformations)
z3_script = generate_z3_script(translated_constraints, results, input_size=32)
with open('z3_solver.py', 'w') as f:
f.write(z3_script)
print("Z3 solver script 'z3_solver.py' has been generated.")python ./z3_solver.py
Found input: SUCTF{Y0u_Ar3_Andr0id_M4st3r!!!}