|
|
|---|---|
|
|
|
|
|
|
|
|
内存也是全部符号化的，只不过因为性能问题，我没有像寄存器那样直接枚举所有寄存器再一个个去符号化，而是判断指令的内存读记录再去符号化。triton 的 ctx.isConcreteMemoryValueDefined() 就是来判断一处内存地址是否已定义，如果被具体化或者被符号化它都会返回 true，但如果返回 false 就说明这处内存什么都没定义，此时我们就符号化它 |
|
|
感谢大佬的回复，我读了你的文章学习了很多，我现在正在用triton恢复一个arm下的ollvm的混淆，但是我发现triton的行为可能存在问题，不知道你之前是否遇到过 具体来说就是以下三条指令 0x4007be40:adrp x8, #0xb5000 0x4007be44:ldr x8, [x8, #0x988] 0x4007be48:ldr w8, [x8] 第二条和第三条都是load内存的指令，我也是用trace把指令读内存的区域全部符号化了，但是第二条指令读完w8是符号化的，第三条读完w8就不是符号化的了(w8是x8的低32位)，两条指令执行完打出来的AST是下面的两条 第二条执行完：(define-fun ref!55 () (_ BitVec 64) (concat ref!54 ref!52 ref!50 ref!48 ref!46 ref!44 ref!42 ref!40)) ; LDR operation - LOAD access 第三条执行完：(define-fun ref!65 () (_ BitVec 64) (concat (_ bv0 8) (_ bv0 8) (_ bv0 8) (_ bv0 8) (_ bv0 8) (_ bv0 8) (_ bv0 8) (_ bv0 8))) ; LDR operation - LOAD access 然后符号化就全部断掉了，请问你之前遇到过这个问题吗 |
|
|
你是怎么符号化的，有没有试过开 MODE.SYMBOLIZE_LOAD、MODE.SYMBOLIZE_STORE、MODE.MEMORY_ARRAY
最后于 2026-3-25 16:52
被LingMo0412编辑
，原因：
|
|
|
for line in ori_instructions: addr_str, inst_text, registers_mems = line.split(':') inst = Instruction() inst.setAddress(int(addr_str, 16)) inst.setOpcode(assemble(inst_text.strip())) if "memoryread=((" in line: # 提取 addr:0x..., size:... # 简单的正则或 split 提取 import re reads = re.findall(r"addr-(0x[0-9a-fA-F]+),value-(0x[0-9a-fA-F]+),size-(\d+)", line) for mem_addr_str, mem_value_str, mem_size_str in reads: m_addr = int(mem_addr_str, 16) m_value = int(mem_value_str, 16) m_size = int(mem_size_str) print(f"[*] Detected memory read in instruction at {hex(inst.getAddress())} with address {hex(m_addr)}, value {hex(m_value)}, and size {m_size} bytes") for i in range(m_size): memi = MemoryAccess(m_addr + i, CPUSIZE.BYTE) #if (ctx.isConcreteMemoryValueDefined(m_addr, m_size)): ctx.setConcreteMemoryValue(m_addr + i, 0) ctx.symbolizeMemory(memi, f"mem_{m_addr + i}") print(f"[*] Memory at {hex(m_addr + i)} symb: {ctx.getSymbolicMemory(m_addr + i)}") #print(f"[*] Found memory read at {hex(m_addr)} with size {m_size} bytes") # 符号化内存 #set_memory_bytes(ctx, m_addr, m_value, m_size) # 初始化内存值为0 #ctx.symbolizeMemory(MemoryAccess(m_addr, m_size), f"mem_at_{hex(m_addr)}") ctx.processing(inst) #w8_expr = ctx.getSymbolicRegister(ctx.getRegister("w8")).getAst() #print("W8 AST Structure:", w8_expr) #ctx.symbolizeRegister(ctx.getRegister("x8"), "x8") # 强制检查 w8 w8_reg = ctx.getRegister("w8") w8_ast = ctx.getSymbolicRegister(w8_reg) print(w8_ast) 这段是模拟执行的代码，就是边执行边把trace里的memory按字节符号化，然后在模拟执行之前把所有寄存器都先赋好了concrete值再符号化，我看了一下和你文章里的逻辑基本都是一样的，这几个mode前两个我之家了第一个 |
|
|
额 你有没有最小可执行的py例子代码来，发成文件看看 |
|
|
读了下triton，发现问题了，就是少了MODE.MEMORY_ARRAY 这个导致的，不开这个用的就是vertor模式，直接就常量化了 |
