trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.67k stars 472 forks source link

Incorrect invalid memory access due to capstone bug #560

Closed offlinemark closed 6 years ago

offlinemark commented 6 years ago

This is a follow up issue to #537.

The attached programs simply aims to cause a libc malloc error with a bad free(). Manticore should successfully execute to a clean exit, however it reports an invalid memory access in __libc_malloc.

2017-11-13 18:35:25,527: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc20:  mov rax, qword ptr [rdx - 8]
2017-11-13 18:35:25,529: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc24:  test    al, 2
2017-11-13 18:35:25,531: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc26:  jne 0x41dc47
2017-11-13 18:35:25,532: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc28:  test    al, 4
2017-11-13 18:35:25,534: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc2a:  mov ecx, 0x6ca800
2017-11-13 18:35:25,535: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc2f:  je  0x41dc3e
2017-11-13 18:35:25,537: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc31:  lea rax, qword ptr [rdx - 0x10]
2017-11-13 18:35:25,539: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc35:  and rax, 0xfc000000
2017-11-13 18:35:25,541: [67131] m.c.c.abstractcpu:DEBUG: INSTRUCTION: 0x000000000041dc3b:  mov rcx, qword ptr [rax]
2017-11-13 18:35:26,227: [67131] m.manticore:INFO: Generated testcase No. 0 - Invalid memory access (mode:r) <f8000000>
2017-11-13 18:35:26,248: [67131] m.manticore:INFO: Results in /mnt/hgfs/code/manticore/examples/linux/mcore_NzXjgF
2017-11-13 18:35:26,249: [67131] m.manticore:INFO: Total time: 149.902643919

537.log 537.zip

offlinemark commented 6 years ago

Bounty

catenacyber commented 6 years ago

Quick answer : update to capstone 4.0.alpha2

Long answer : Problem comes with instruction and rax, 0xfc000000 or "48 25 00 00 00 FC" Immediate operand does not get sign extended So rax which was before 0x00007ffff80008b0 becomes 0x00000000f8000000 instead of 0x00007ffff8000000 Therefore, mov rcx, qword ptr [rax] accesses the wrong memory, which happens to be invalid in this case. Doing something similar as operand sign-extension in ADC instruction, I found out that capstone was telling that immediate operand was 8-byte sized. I guess that the commit which fixed it was https://github.com/aquynh/capstone/commit/de8dd26780efc2fd32fe4329ddc8f11769b4d238 You can test capstone with cstool -d x64 "48 25 00 00 00 FC" and see if you get and rax, 0xfffffffffc000000or and rax, 0xfc000000

offlinemark commented 6 years ago

hi @catenacyber, thank you so much for helping us debug this! these emulation bugs are some of the most painful to look at, so we really appreciate your help here ❤️ it's somewhat of a relief that it appears the bug is not in our code, but in capstone. unfortunately it seems the newest capstone available in pypi is still 3.0.5rc2 (https://pypi.python.org/pypi/capstone) , which is somewhat problematic for us because we then cannot easily, automatically install the dep for our users..

disconnect3d commented 6 years ago

@mossberg We had similar problem in pwndbg, see https://github.com/aquynh/capstone/issues/866

catenacyber commented 6 years ago

@mossberg you can temporary hack around to sign-extend AND source operand.

It would be something like :

diff --git a/manticore/core/cpu/x86.py b/manticore/core/cpu/x86.py
index 174a33b..676dac0 100644
--- a/manticore/core/cpu/x86.py
+++ b/manticore/core/cpu/x86.py
@@ -887,7 +887,11 @@ class X86Cpu(Cpu):
         :param dest: destination operand.
         :param src: source operand.
         '''
-        res = dest.write(dest.read() & src.read())
+        if src.size == 64 and src.type == 'immediate' and dest.size == 64:
+            arg1 = Operators.SEXTEND(src.read(), 32, 64)
+        else:
+            arg1 = src.read()
+        res = dest.write(dest.read() & arg1)
         #Defined Flags: szp
         cpu._calculate_logic_flags(dest.size, res)