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.68k stars 472 forks source link

Manticore incorrectly reports invalid memory access for an x64 binary #973

Closed aditi-gupta closed 5 years ago

aditi-gupta commented 6 years ago

OS / Environment

Ubuntu 18.04

Manticore version

0.1.10 with some slight changes

rsa_sign.zip rsa_priv.txt

In order to reproduce the issue, you need an example.txt file to sign. It doesn't matter what is in it. You also need the attached rsa_priv.txt file.

from manticore import Manticore

target = 'rsa_sign'
m = Manticore(target, ['example.txt'])
m.verbosity(2)
print "start"

@m.hook(0x400b4d)
def hook(state):
    cpu = state.cpu
    print "hook"

m.run()
print "end"
start
2018-07-11 15:11:01,250: [24938] m.c.executor:INFO: load state 0
2018-07-11 15:11:02,240: [24938] m.p.platform:DEBUG: sys_brk(0x0) -> 7196672(0x6dd000)
2018-07-11 15:11:02,272: [24938] m.p.platform:DEBUG: sys_brk(0x6de1c0) -> 7201216(0x6de1c0)
2018-07-11 15:11:02,345: [24938] m.p.platform:DEBUG: sys_arch_prctl(0x1002, 0x6dd880) -> 0
2018-07-11 15:11:02,426: [24938] m.p.platform:DEBUG: sys_newuname(0x7ffffffffbd0 (Linux)) -> 0
2018-07-11 15:11:02,525: [24938] m.p.platform:DEBUG: sys_readlink(0x4c1d83 (/proc/self/exe), 0x7fffffffed00 (/home/user/mbedtls-2.11.0/progra..), 0x1000) -> 48
2018-07-11 15:11:06,702: [24938] m.p.platform:DEBUG: sys_brk(0x6ff1c0) -> 7336384(0x6ff1c0)
2018-07-11 15:11:06,787: [24938] m.p.platform:DEBUG: sys_brk(0x700000) -> 7340032(0x700000)
2018-07-11 15:11:07,350: [24938] m.p.platform:DEBUG: sys_access(0x4c195a (/etc/ld.so.nohwcap), 0x0) -> -1
hook
2018-07-11 15:11:10,281: [24938] m.p.platform:DEBUG: sys_newfstat(0x1, 0x7fffffffed10) -> 0
2018-07-11 15:11:10,323: [24938] m.p.platform:DEBUG: sys_ioctl(0x1, 0x5401, 0x7fffffffec70) -> -22
2018-07-11 15:11:10,942: [24938] m.p.linux:DEBUG: WRITE(1, 0x006de640, 42) -> <''>
2018-07-11 15:11:10,942: [24938] m.p.linux:DEBUG: WRITE(1, 0x006de640, 42) -> <'  . Reading private key from rsa_priv.txt'>
2018-07-11 15:11:10,945: [24938] m.p.platform:DEBUG: sys_write(0x1, 0x6de640 (  . Reading private key from rs..), 0x2a) -> 42
2018-07-11 15:11:11,519: [24938] m.p.linux:DEBUG: Opening file rsa_priv.txt for real fd 3
2018-07-11 15:11:11,520: [24938] m.p.platform:DEBUG: sys_openat(0xffffff9c, 0x4ac3b6 (rsa_priv.txt), 0x0, 0x0) -> 3
2018-07-11 15:11:12,133: [24938] m.p.platform:DEBUG: sys_newfstat(0x3, 0x7fffffffe900) -> 0
2018-07-11 15:11:12,480: [24938] m.p.platform:DEBUG: sys_read(0x3, 0x6dec80 (N = AE1EC41FDD978C18CB43F9587F9B..), 0x1000) -> 2361(0x939)
2018-07-11 15:14:19,710: [24938] m.p.linux:DEBUG: sys_close(3)
2018-07-11 15:14:19,711: [24938] m.p.platform:DEBUG: sys_close(0x3) -> 0
2018-07-11 15:14:20,936: [24938] m.manticore:INFO: Generated testcase No. 0 - Invalid memory access (mode:r) <18>
2018-07-11 15:14:20,953: [24938] m.manticore:INFO: Results in /home/user/mbedtls-2.11.0/mcore_95hdNG
2018-07-11 15:14:20,953: [24938] m.manticore:INFO: Total time: 199.719868898
2018-07-11 15:14:20,959: [24938] m.c.plugin:INFO: Coverage: 5473 different instructions executed
2018-07-11 15:14:20,960: [24938] m.c.plugin:INFO: Instructions executed: 294977
end
offlinemark commented 6 years ago

I've reproduced the issue, you need a few tweaks to manticore to do it, checkout this branch: https://github.com/trailofbits/manticore/tree/dev-973-dbg

that branch contains the fixes:

offlinemark commented 6 years ago

some notes from trying to debug:

from inspecting the pkl file of the state, we can see the crashing instruction

In [2]: x = pickle.load(open('test_00000000.pkl'))

In [3]: x
Out[3]: <manticore.core.state.State at 0x7fbd881aebd0>

In [4]: print x.cpu
Instruction: 0x000000000043a08f:        cmp     rdx, qword ptr [rax + 0x18]
RAX: 0x0000000000000000
RCX: 0x0000000000000110
RDX: 0x00000000006d98e0
RBX: 0x00000000006d9880
RSP: 0x00007ffffffff3e0
RBP: 0x0000000000000001
RSI: 0x0000000000000000
RDI: 0x00000000006dec70
 R8: 0x00000000006dd880
 R9: 0x0000000000000000
R10: 0x0000000000000009
R11: 0x0000000000000004
R12: 0x00000000006dec70
R13: 0x00000000006dec60
R14: 0x0000000000001010
R15: 0x00000000006dfc70
RIP: 0x000000000043a093
EFLAGS: 0x0000000000000000
CF: 0
SF: 0
ZF: 0
OF: 0
AF: 0
PF: 0
IF: 0
DF: 0
CS: 0, fffff000 (rwx)
DS: 0, fffff000 (rwx)
ES: 0, fffff000 (rwx)
SS: 0, fffff000 (rwx)
FS: 6dd880, 4000 (rw)
GS: 0, fffff000 (rwx)
FP0: (0, 0)
FP1: (0, 0)
FP2: (0, 0)
FP3: (0, 0)
FP4: (0, 0)
FP5: (0, 0)
FP6: (0, 0)
FP7: (0, 0)
TOP: 0

the crashing insn is in free(). RAX is 0 when it shouldn't be.

tested that the bug doesn't go away when using the capstone next branch, it might be a undiscovered bug in capstone, or in manticore.

ideas to try further:

offlinemark commented 6 years ago

nopping out Eventful._publish makes it faster to execute to the crash, but also disables the event infrastructure for generating testcases and reporting "Invalid memory exception" etc

defunctio commented 6 years ago

Some updates;

Stack trace for the issue;

main-
0x0000000000400e20 <+723>:   call   0x429010 <fclose>
  0x0000000000429142 <+306>:   call   0x42e5d0 <_IO_new_file_close_it>
     0x000000000042e6a7 <+215>:   call   0x4306c0 <_IO_setb>
       0x0000000000430706 <+70>:    call   0x439d40 <free>

I noticed fopen on a target statically compiled under Ubuntu 18.04 uses openat vs open when built on 16.04. Recompiling the rsa_sign target under 16.04 appears to have resolved the above issue, it seems that the usage of Linux.sys_openat may be problematic? More testing is needed

https://github.com/trailofbits/manticore/blob/b30966fca7b75c9d1b1c01898b99a57a2108cafa/manticore/platforms/linux.py#L1435

Update; I was not able to reproduce the issue in the original target by compiling a random test example that uses fopen to invoke openat on 18.04. So it is something specific to the rsa_sign target.

offlinemark commented 6 years ago

https://github.com/trailofbits/manticore/issues/940 could be related, it deals with openat also. in fact one of the changes in the dev-973-dbg branch is from there