Mismatching Leave States (Trace vs. Symbolic Execution)

cyber-defence-campus / morion

Morion is a PoC tool to experiment with symbolic execution on real-word (ARMv7) binaries.

Apache License 2.0

6 stars 1 forks source link

Mismatching Leave States (Trace vs. Symbolic Execution) #2

Closed pdamian closed 2 years ago

pdamian commented 2 years ago

Investigate the hijack_indirect_callsitetest case. Why is the leave state of the GDB trace different than the leave state of the symbolic execution?

pdamian commented 2 years ago

Library functions (such as strlen) that we skip, can change values on the stack. Therefore, in the leave state, everything on the stack but outside of [fp, sp] is fine to mismatch.
Similarly, skipped library functions might lead to some mismatching registers. However, we should not have any mismatches in callee-save registers (i.e. r4-r8, r9?, r10-r11).

Therefore, the test case hijack_indirect_callsiteshould not be buggy.