dslab-epfl / chef-symbex-lua

Lua interpreter modded to support symbolic execution
7 stars 3 forks source link

chef segfaults when trying lua examples #1

Open fbanados opened 9 years ago

fbanados commented 9 years ago

the script run_qemu.py sym segfaults when running any of the examples that do symbolic execution. This issue is related to the bug "mr ->ops in memory_region_access_valid may be NULL and causes crashes" shown in the mailing list, but applying the commit from the thread does not solve the issue.

example: ./lua_runner.py targets/test_json_sym.lua generates the following console output:

54 [State 0] ***** CONCOLIC SESSION - START *****
54 [State 0] Inserting symbolic data at 0xbf9b430c of size 0xa with name 'json'
55 [State 0] Forking state 0 at pc = 0x8064c67
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
56 [State 0] Forking state 0 at pc = 0xb74e9f5f
57 [State 0] Processing test case for Concolics[ json=>"**********" ]
57 [State 0] New CFG fragment discovered!
57 [State 0] New HL tree path!
=== Starting CFG analysis ===
1 total instructions to process.
Extracted 1 basic blocks
Extracted 0 branch opcodes.
Identified 0 potential uncovered branching points.
=== CFG analysis complete ===
57 [State 1] Switched to state Concolics[ json=>"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ]
57 [State 0] Switching to state 1
57 [State 0] Switching from state 0 to state 1
57 [State 1] Forking state 1 at pc = 0x8064c67
Segmentation fault (core dumped)
Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x00007f4dede35ab1 in memory_region_access_valid (mr=0x7f4df154f580, 
    addr=176, size=4, is_write=true) at /home/nested/s2e/qemu/memory.c:836
836     if (mr->ops->valid.accepts
(gdb) bt
#0  0x00007f4dede35ab1 in memory_region_access_valid (mr=0x7f4df154f580, 
    addr=176, size=4, is_write=true) at /home/nested/s2e/qemu/memory.c:836
#1  0x00007f4dede3500e in memory_region_dispatch_write (mr=0x7f4df154f580, 
    addr=176, data=0, size=4) at /home/nested/s2e/qemu/memory.c:914
#2  0x00007f4dede34fcb in io_mem_write (mr=0x7f4df154f580, addr=176, val=0, 
    size=4) at /home/nested/s2e/qemu/memory.c:1514
#3  0x00007f4dede5ab4e in io_writel_mmu_symb (physaddr=176, val=0, 
    addr=4294946992, retaddr=0x41b65911)
    at /home/nested/s2e/qemu/softmmu_template.h:465
#4  0x00007f4dede5ab89 in io_write_chkl_mmu_symb (
    physaddr=18446744069414604819, val=0, addr=4294946992, retaddr=0x41b65911)
    at /home/nested/s2e/qemu/softmmu_template.h:483
#5  0x00007f4dede5acd8 in __stl_mmu_symb (addr=4294946992, val=0, mmu_idx=0)
    at /home/nested/s2e/qemu/softmmu_template.h:584
#6  0x0000000041b65912 in ?? ()
#7  0x00007f4dc6b476e0 in ?? ()
#8  0x00007f4dede8e535 in std::pair<klee::MemoryObject const*, klee::ObjectHolder>::~pair (
    this=<error reading variable: Cannot access memory at address 0xc3df5f98>)
    at /usr/lib/gcc/x86_64-linux-gnu/4.6/../../../../include/c++/4.6/bits/stl_pair.h:87
Backtrace stopped: previous frame inner to this frame (corrupt stack?)
stefanbucur commented 9 years ago

I was not able to reproduce the issue. Moreover, this crash does not seem to be related to the Chef functionality. What operating system are you using?

One issue I can think of is related to Qemu's network stack. I heard reports that it is unstable in conjunction with S2E and it causes random crashes. I suggest running the VM with no networking enabled (use the -net none argument) and checking if you're still getting the crashes.