Rolling back symbolic state after concrete write

[0xdeaddc0de]

Hello o/ I have a callback that is used to check if the accessed address is mapped. If not i manually perform the logic of a signal handler. ex: movabs rax, qword ptr [0xcafebabe], will be handled by python code.

To trigger the callback, the instruction needs to be consumed by triton, and will overwrite with a concrete value the symbolic expression of rax. This is a problem as i would like to continue to use the symbolic expression in rax after my logic to handle the sigsegv.

Is there a way to rollback the symbolic expression or cancel the execution of the last instruction ?

Ty in advance

[mecrii9191]

just asking, how did you symbolize also the memoryaccess so you can know when rax is keep getting used, be able to track back the user back to this memory access address. because when i'm trying to track back a register to its origin memory address, looking at the AST it only captures reference nodes after the dereference.. could you show me how you done it if you did?

[mecrii9191]

also, you could use snapshots for that (but its not a really good solution but works), look at ttexplore source code, there is a part where it snapshots the context (and brings it back). you can use it within RAII wrapper in project

https://github.com/JonathanSalwan/ttexplore/blob/8f03397e1b4f1d9314898cb367d01a5d15bfc5e7/lib/ttexplore.cpp#L183

[0xdeaddc0de]

just asking, how did you symbolize also the memoryaccess so you can know when rax is keep getting used, be able to track back the user back to this memory access address. because when i'm trying to track back a register to its origin memory address, looking at the AST it only captures reference nodes after the dereference.. could you show me how you done it if you did?

I might have said something wrong in my issue. For example i'm just doing

    for i in range(255):
        ctx.symbolizeMemory(MemoryAccess(OFFSET_BUFFER + i, CPUSIZE.BYTE))

The symbol will be spread when an instruction read from this memory area and the register will be symbolic. To check if the instruction is symbolic i just perform a

ctx.processing(instr)

if instr.isSymbolized():
     print(instr)

I'm not doing any backward slicing. Maybe something like this would be good for you ?

            rax_sym = ctx.getSymbolicRegisters(ctx.registers.rax)
           
            slc = ctx.sliceExpressions(rax_sym)
            for k, v in sorted(slc.items()):
                print(v.getComment())

[JonathanSalwan]

@0xdeaddc0de

Maybe something like this:

from triton import *

ctx = TritonContext(ARCH.X86_64)

code = [
    b"\x48\xc7\xc0\xad\xde\x00\x00", # mov rax, 0xdead
    b"\x48\xc1\xe0\x10", # shl rax, 16
    b"\x48\xc7\xc3\xef\xbe\x00\x00", # mov rbx, 0xbeef
    b"\x48\x8b\x3c\x18", # mov rdi, qword ptr [rax + rbx]
]

for c in code:
    inst = Instruction(c)
    ctx.disassembly(inst)

    op = inst.getOperands()[1]
    if op.getType() == OPERAND.MEM:
        # Initialize the effective address of the memory access. It does not update any engine.
        ctx.initLeaAst(op)

        # Print the effective address
        print(hex(op.getAddress()))

        # Do whatever you want here. Engines are not updated yet.

    # Build the semantic, it will update engines.
    ctx.buildSemantics(inst)

Maybe you can first disassemble instruction, then use initLeaAst. It will compute the effective address of a memory cell without updating engines. So you can easily know if the dereference is mapped or not. Once everything is okay, you can then call buildSemantics to spread semantics and update engines.

[0xdeaddc0de]

This is really interesting, i will try this, ty !