Open ek0 opened 1 year ago
To elaborate on how the state of the memory cell is checked, here is the underlying code:
bool Emulator::IsSymbolic(const triton::arch::Register& reg) const
{
return ctx_.isRegisterSymbolized(reg);
}
// Is the specified register symbolic
bool Emulator::IsSymbolic(const triton::arch::register_e reg) const
{
const triton::arch::Register& r = ctx_.getRegister(reg);
return IsSymbolic(r);
}
bool Emulator::IsSymbolic(const triton::arch::MemoryAccess& mem) const
{
return ctx_.isMemorySymbolized(mem);
}
Yes, this is because with an array logic, memory cells contain their whole historic of memory accesses.
Below, an unit test that can be used to verify this behaviour.
diff --git a/src/testers/unittests/test_symbolic_array.py b/src/testers/unittests/test_symbolic_array.py
index 627da824..52d3ace3 100644
--- a/src/testers/unittests/test_symbolic_array.py
+++ b/src/testers/unittests/test_symbolic_array.py
@@ -199,3 +199,36 @@ class TestSymbolicArray(unittest.TestCase):
x = self.ctx.getMemoryAst(MemoryAccess(0x1000, 4))
self.assertEqual(x.evaluate(), 0xdeadbeef)
+
+ def test_11(self):
+ code = [
+ (1, b"\x48\xc7\xc0\x00\x10\x00\x00"), # mov rax, 0x1000
+ (2, b"\x48\xc7\xc3\x32\x00\x00\x00"), # mov rbx, 0x32
+ (3, b"\x89\x34\x18"), # mov dword ptr [rax + rbx], esi
+ (4, b"\x48\xc7\xc3\x64\x00\x00\x00"), # mov rbx, 0x64
+ (5, b"\x8b\x0c\x18"), # mov ecx, dword ptr [rax + rbx]
+ ]
+
+ self.ctx.symbolizeRegister(self.ctx.registers.esi, 's_esi')
+
+ for i, op in code:
+ inst = Instruction(op)
+ self.ctx.processing(inst)
+
+ self.assertFalse(self.ctx.isRegisterSymbolized(self.ctx.registers.ecx))
+
+ def test_12(self):
+ code = [
+ (1, b"\x48\xc7\xc0\x00\x10\x00\x00"), # mov rax, 0x1000
+ (2, b"\x48\xc7\xc3\x32\x00\x00\x00"), # mov rbx, 0x32
+ (3, b"\x89\x34\x18"), # mov dword ptr [rax + rbx], esi
+ (4, b"\x8b\x0c\x18"), # mov ecx, dword ptr [rax + rbx]
+ ]
+
+ self.ctx.symbolizeRegister(self.ctx.registers.esi, 's_esi')
+
+ for i, op in code:
+ inst = Instruction(op)
+ self.ctx.processing(inst)
+
+ self.assertTrue(self.ctx.isRegisterSymbolized(self.ctx.registers.ecx))
Evening,
I was recently making use of
triton::modes::SYMBOLIC_STORE
,triton::modes::SYMBOLIC_LOAD
withtriton::modes::MEMORY_ARRAY
as it seemed to be perfect when acting in arbitrary context. Except that when attempting to concretize a previously symbolized memory cell, triton fails to properly reset theisSymbolized
state.Context Configuration
Issue
Emulating the following code works perfectly (with opcode in case you need to test):
Checking
[rsp]
value gives me the proper concrete0x123b
value.However, if
[rsp]
was written with a symbolic variable before, overwriting said memory cell doesn't concretize the memory. Here is an example ASM snippets that shows the issue:Results:
I'm not sure if this is intended, but it seems that when overwriting memory in the memory array, triton fails to properly set the state of referenced memory to concrete.
Expected Behaviour
[rsp]
should have the concreterbp
value.