Open GreenieQwQ opened 3 months ago
It appears that the MemoryAccess information stored in instruction might only contain concrete access information,
Have you tried to use MemoryAccess::getLeaAst()
? That should return the symbolic memory access.
It appears that the MemoryAccess information stored in instruction might only contain concrete access information,
Have you tried to use
MemoryAccess::getLeaAst()
? That should return the symbolic memory access.
Much appreciated! By digging out MemoryAccess::getLeaAst() and its related documentation, I've learned a lot from Triton's memory modeling procedure.
However, I'm still confused about how to symbolize memory before their initial access. I attempted a simple test case as shown below, yet I realized that I may not be able to retrieve the very memory access until having processed the instruction (e.g., I've tried using disassembly
before processing the instruction, but the memory access information in getOperands
is incomplete until having the instruction processed).
def test(self):
self.ctx = TritonContext(ARCH.X86_64)
self.ctx.setMode(MODE.MEMORY_ARRAY, True)
self.ctx.setMode(MODE.SYMBOLIZE_LOAD, True)
self.ctx.setMode(MODE.SYMBOLIZE_STORE, True)
code = [
(1, b"\x8b\x0c\x18"), # mov ecx, dword ptr [rax + rbx]
(2, b"\x48\x81\xf9\xad\xde\x00\x00"), # cmp rcx, 0xdead
]
self.ctx.symbolizeRegister(self.ctx.registers.rax, 's_rax')
self.ctx.symbolizeRegister(self.ctx.registers.rbx, 's_rbx')
self.ctx.symbolizeRegister(self.ctx.registers.rcx, 's_rcx')
count = 0 # counter for symbolized memory
for i, op in code:
i= Instruction(op)
self.ctx.processing(i)
if i.isMemoryRead():
a = i.getLoadAccess()
readMemory = a[0][0]
if not self.ctx.isMemorySymbolized(readMemory):
memAlias = f'mem_{count}'
self.ctx.symbolizeMemory(readMemory, memAlias)
print(f"symbolize memory {readMemory} with {memAlias}")
count += 1
if i.isMemoryWrite():
# similar to memory read
zf = self.ctx.getRegisterAst(self.ctx.registers.zf)
m = self.ctx.getModel(zf == 1)
print(m)
Ideally, a model where [rax+rbx]
is set to 0xdead
will be printed. However, since the memory is symbolized after its initial access, m
is empty in actual.
I recently embarked on a project utilizing Triton's Python interface for AArch64 binary analysis and I must express my gratitude for providing such a user-friendly tool.
My current task involves generating a mapping of all registers and memory used within a function to their symbolic states at the end of the function, symbolizing all registers and memory states automatically upon their initial access. As a newcomer to Triton, I've referred to the
SeedCoverage
class withinsrc/testers/unittests/test_simulation.py
to perform dynamic symbolic execution and set a boundary for visiting the same address to mitigate path explosion.Below is a snippet of the Python code I've been utilizing to symbolize registers and conduct emulation (returning only x0 for test):
However, when trying to collect all the referenced symbolic address in
seed_emulate
, I encountered a challenge. It appears that theMemoryAccess
information stored ininstruction
might only contain concrete access information, even with SYMBOLIC_STORE and SYMBOLIC_LOAD modes enabled. Consequently, I am curious about the following:It's been an excellent experience for using Triton! Any help would be greatly appreciated!