How to synchronize the memory value between setConcereteMemoryValue and the instructions.

[vancaho]

Hi, recently I'm analysis a execution trace with libtriton. However I found that the memory value set by setConcreteMemoryValue is not synchronized with the instruction expressions, even with the concretizeMemory function. Here is my example code:

---

from triton import *
import struct


#first, we set ESP to 0x10000000
#1. push 0x31323334   ;after this, esp should be 0xfffffffc, and [0x10000000]=0x31323334
#;setConcreteMemoryValue(MemoryAccess(0x10000000, 4, 0x77787974)); after this [0x10000000] shoould be 0x77787874
#2. ret               ;after this eip should be 0x77787974, esp should be 0x10000000
#

setArchitecture(ARCH.X86) 

print '[+] Setting value of ESP to 0x10000000'
setConcreteRegisterValue(Register(REG.ESP, 0x10000000)) #set esp to 0x10000000

inst1 = Instruction()
inst1.setOpcodes('\x68\x34\x33\x32\x31')    #0x00400000: push 0x31323334
inst1.setAddress(0x00400000)
processing(inst1)
print inst1
for expr in inst1.getSymbolicExpressions():
    print '\t', expr 

print '[+] After pushing value    0x31323334, esp=', hex(getConcreteRegisterValue(REG.ESP)), ', Memory value at 0x10000000 is:', hex(struct.unpack('I', getConcreteMemoryAreaValue(0x10000000, 4))[0])

print '[+] Setting value of 0x10000000 to 0x77787974'
setConcreteMemoryValue(MemoryAccess(0x10000000, 4, 0x77787974))
concretizeMemory(0x10000000)


print '[+] After Setting value at 0x10000000, esp=', hex(getConcreteRegisterValue(REG.ESP)), ', Memory value at 0x10000000 is:', hex(struct.unpack('I', getConcreteMemoryAreaValue(0x10000000, 4))[0])

inst2 = Instruction()
inst2.setOpcodes('\xc3')                    #0x00400000: ret
inst2.setAddress(0x00400005)
processing(inst2)
print inst2
for expr in inst2.getSymbolicExpressions():
    print '\t', expr 
print '[+] After executing ret instruction,   esp=', hex(getConcreteRegisterValue(REG.ESP)), ', eip =', hex(getConcreteRegisterValue(REG.EIP))

---

Executing above script, it outputs:

[+] Setting value of ESP to 0x10000000
0x400000: push 0x31323334
	ref!0 = ((_ zero_extend 0) (bvsub (_ bv268435456 32) (_ bv4 32))) ; Stack alignment
	ref!1 = ((_ extract 31 24) ((_ zero_extend 0) (_ bv825373492 32))) ; Byte reference - PUSH operation
	ref!2 = ((_ extract 23 16) ((_ zero_extend 0) (_ bv825373492 32))) ; Byte reference - PUSH operation
	ref!3 = ((_ extract 15 8) ((_ zero_extend 0) (_ bv825373492 32))) ; Byte reference - PUSH operation
	ref!4 = ((_ extract 7 0) ((_ zero_extend 0) (_ bv825373492 32))) ; Byte reference - PUSH operation
	ref!5 = (concat ((_ extract 31 24) ((_ zero_extend 0) (_ bv825373492 32))) ((_ extract 23 16) ((_ zero_extend 0) (_ bv825373492 32))) ((_ extract 15 8) ((_ zero_extend 0) (_ bv825373492 32))) ((_ extract 7 0) ((_ zero_extend 0) (_ bv825373492 32)))) ; Temporary concatenation reference - PUSH operation
	ref!6 = ((_ zero_extend 0) (_ bv4194309 32)) ; Program Counter
[+] After pushing value    0x31323334, esp= 0xffffffcL , Memory value at 0x10000000 is: 0x0
[+] Setting value of 0x10000000 to 0x77787974
[+] After Setting value at 0x10000000, esp= 0xffffffcL , Memory value at 0x10000000 is: 0x77787974
0x400005: ret
	ref!7 = ((_ zero_extend 0) (concat ((_ extract 7 0) ref!1) ((_ extract 7 0) ref!2) ((_ extract 7 0) ref!3) ((_ extract 7 0) ref!4))) ; Program Counter
	ref!8 = ((_ zero_extend 0) (bvadd ((_ extract 31 0) ref!0) (_ bv4 32))) ; Stack alignment
[+] After executing ret instruction,   esp= 0x10000000L , eip = 0x31323334L

It seems that the value we set with setConcreteMemoryValue has no effect, as the eip after ret instruction is still 0x31323334, which is pushed in the first instruction.

By observation the output, we can see another interesting result: the memory value at 0x10000000 after the pushing instruction is 0x00000000. However after we setting the memory value with setConcreteMemoryValue, it works

So my questions are:1) Why the value output by getConcreteMermoryValue is still 0x0?
2)if I want to modify the memory value after one instruction and use it in the following instructions, how to write the codes?

Thanks very much

[JonathanSalwan]

Everything is working.

So my questions are

1. Why the value output by getConcreteMermoryValue is still 0x0?

Because you are getting the value at the wrong place... See how a push instruction works.

ELSE IF OperandSize = 32
  THEN
    ESP ← ESP – 4;
    Memory[SS:ESP] ← SRC;   (* push dword *)

So, if you want to see your pushed value you have to target 0xffffffc. That's also why the ret instruction works perfectly =).