search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Out of Bounds write in pusht_bfr #30

Closed bugs-syssec closed 5 years ago

bugs-syssec commented 5 years ago

While fuzzing boolector,

this input file ``` 2147483649 sort ```

was found, which leads to an out of bounds write, according to valgrind.

The attached file contains more lines leading to the same crash, the above file contains the minimal version.

ASAN trace (probably not useful, since it does not find the write) ``` ==25988==ERROR: AddressSanitizer failed to allocate 0x800002000 (34359746560) bytes of LargeMmapAllocator (error code: 12) ==25988==Process memory map follows: 0x000000400000-0x0000007e2000 /home/user/boolector-asan 0x0000009e2000-0x0000009e3000 /home/user/boolector-asan 0x0000009e3000-0x000000a07000 /home/user/boolector-asan 0x000000a07000-0x0000016fa000 0x00007fff7000-0x00008fff7000 0x00008fff7000-0x02008fff7000 0x02008fff7000-0x10007fff8000 0x600000000000-0x602000000000 0x602000000000-0x602000010000 0x602000010000-0x603000000000 0x603000000000-0x603000010000 0x603000010000-0x604000000000 0x604000000000-0x604000010000 0x604000010000-0x606000000000 0x606000000000-0x606000010000 0x606000010000-0x607000000000 0x607000000000-0x607000010000 0x607000010000-0x608000000000 0x608000000000-0x608000010000 0x608000010000-0x60b000000000 0x60b000000000-0x60b000010000 0x60b000010000-0x60c000000000 0x60c000000000-0x60c000010000 0x60c000010000-0x60e000000000 0x60e000000000-0x60e000010000 0x60e000010000-0x611000000000 0x611000000000-0x611000010000 0x611000010000-0x615000000000 0x615000000000-0x615000020000 0x615000020000-0x616000000000 0x616000000000-0x616000020000 0x616000020000-0x619000000000 0x619000000000-0x619000020000 0x619000020000-0x61d000000000 0x61d000000000-0x61d000020000 0x61d000020000-0x621000000000 0x621000000000-0x621000020000 0x621000020000-0x622000000000 0x622000000000-0x622000020000 0x622000020000-0x624000000000 0x624000000000-0x624000030000 0x624000030000-0x625000000000 0x625000000000-0x625000020000 0x625000020000-0x629000000000 0x629000000000-0x629000010000 0x629000010000-0x62d000000000 0x62d000000000-0x62d000020000 0x62d000020000-0x631000000000 0x631000000000-0x631000040000 0x631000040000-0x640000000000 0x640000000000-0x640000003000 0x7f5e91ee2000-0x7f6291ee4000 0x7f6691e00000-0x7f6691f00000 0x7f6692000000-0x7f6692100000 0x7f6692200000-0x7f6692300000 0x7f6692400000-0x7f6692500000 0x7f6692533000-0x7f6694885000 0x7f6694885000-0x7f6694a6c000 /lib/x86_64-linux-gnu/libc-2.27.so 0x7f6694a6c000-0x7f6694c6c000 /lib/x86_64-linux-gnu/libc-2.27.so 0x7f6694c6c000-0x7f6694c70000 /lib/x86_64-linux-gnu/libc-2.27.so 0x7f6694c70000-0x7f6694c72000 /lib/x86_64-linux-gnu/libc-2.27.so 0x7f6694c72000-0x7f6694c76000 0x7f6694c76000-0x7f6694c8d000 /lib/x86_64-linux-gnu/libgcc_s.so.1 0x7f6694c8d000-0x7f6694e8c000 /lib/x86_64-linux-gnu/libgcc_s.so.1 0x7f6694e8c000-0x7f6694e8d000 /lib/x86_64-linux-gnu/libgcc_s.so.1 0x7f6694e8d000-0x7f6694e8e000 /lib/x86_64-linux-gnu/libgcc_s.so.1 0x7f6694e8e000-0x7f6694e91000 /lib/x86_64-linux-gnu/libdl-2.27.so 0x7f6694e91000-0x7f6695090000 /lib/x86_64-linux-gnu/libdl-2.27.so 0x7f6695090000-0x7f6695091000 /lib/x86_64-linux-gnu/libdl-2.27.so 0x7f6695091000-0x7f6695092000 /lib/x86_64-linux-gnu/libdl-2.27.so 0x7f6695092000-0x7f6695099000 /lib/x86_64-linux-gnu/librt-2.27.so 0x7f6695099000-0x7f6695298000 /lib/x86_64-linux-gnu/librt-2.27.so 0x7f6695298000-0x7f6695299000 /lib/x86_64-linux-gnu/librt-2.27.so 0x7f6695299000-0x7f669529a000 /lib/x86_64-linux-gnu/librt-2.27.so 0x7f669529a000-0x7f66952b4000 /lib/x86_64-linux-gnu/libpthread-2.27.so 0x7f66952b4000-0x7f66954b3000 /lib/x86_64-linux-gnu/libpthread-2.27.so 0x7f66954b3000-0x7f66954b4000 /lib/x86_64-linux-gnu/libpthread-2.27.so 0x7f66954b4000-0x7f66954b5000 /lib/x86_64-linux-gnu/libpthread-2.27.so 0x7f66954b5000-0x7f66954b9000 0x7f66954b9000-0x7f6695656000 /lib/x86_64-linux-gnu/libm-2.27.so 0x7f6695656000-0x7f6695855000 /lib/x86_64-linux-gnu/libm-2.27.so 0x7f6695855000-0x7f6695856000 /lib/x86_64-linux-gnu/libm-2.27.so 0x7f6695856000-0x7f6695857000 /lib/x86_64-linux-gnu/libm-2.27.so 0x7f6695857000-0x7f66959d0000 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 0x7f66959d0000-0x7f6695bd0000 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 0x7f6695bd0000-0x7f6695bda000 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 0x7f6695bda000-0x7f6695bdc000 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 0x7f6695bdc000-0x7f6695be0000 0x7f6695be0000-0x7f6695c07000 /lib/x86_64-linux-gnu/ld-2.27.so 0x7f6695cdd000-0x7f6695df4000 0x7f6695df4000-0x7f6695e07000 0x7f6695e07000-0x7f6695e08000 /lib/x86_64-linux-gnu/ld-2.27.so 0x7f6695e08000-0x7f6695e09000 /lib/x86_64-linux-gnu/ld-2.27.so 0x7f6695e09000-0x7f6695e0a000 0x7ffde7145000-0x7ffde7166000 [stack] 0x7ffde71ea000-0x7ffde71ed000 [vvar] 0x7ffde71ed000-0x7ffde71ef000 [vdso] 0xffffffffff600000-0xffffffffff601000 [vsyscall] ==25988==End of process memory map. ==25988==AddressSanitizer CHECK failed: /build/llvm-toolchain-3.9-GZwVE7/llvm-toolchain-3.9-3.9.1/projects/compiler-rt/lib/sanitizer_common/sanitizer_common.cc:120 "((0 && "unable to mmap")) != (0)" (0x0, 0x0) ==25988==WARNING: failed to fork (errno 12) ==25988==WARNING: failed to fork (errno 12) ==25988==WARNING: failed to fork (errno 12) ==25988==WARNING: failed to fork (errno 12) ==25988==WARNING: failed to fork (errno 12) ==25988==WARNING: Failed to use and restart external symbolizer! #0 0x4efc65 (/home/user/boolector-asan+0x4efc65) #1 0x50a375 (/home/user/boolector-asan+0x50a375) #2 0x4f9aa2 (/home/user/boolector-asan+0x4f9aa2) #3 0x503a15 (/home/user/boolector-asan+0x503a15) #4 0x4425b9 (/home/user/boolector-asan+0x4425b9) #5 0x43c7d6 (/home/user/boolector-asan+0x43c7d6) #6 0x4e6178 (/home/user/boolector-asan+0x4e6178) #7 0x42aa0a (/home/user/boolector-asan+0x42aa0a) #8 0x42ab61 (/home/user/boolector-asan+0x42ab61) #9 0x6f4720 (/home/user/boolector-asan+0x6f4720) #10 0x65b591 (/home/user/boolector-asan+0x65b591) #11 0x5a033a (/home/user/boolector-asan+0x5a033a) #12 0x59f55a (/home/user/boolector-asan+0x59f55a) #13 0x52531e (/home/user/boolector-asan+0x52531e) #14 0x7f66948a6b96 (/lib/x86_64-linux-gnu/libc.so.6+0x21b96) #15 0x4367a9 (/home/user/boolector-asan+0x4367a9) ```
Valgrind trace ``` ==26039== Memcheck, a memory error detector ==26039== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al. ==26039== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info ==26039== Command: ./boolector-plain pusht_bfr.btor2 ==26039== ==26039== Warning: set address range perms: large range [0x15bf0028, 0x25bf0058) (noaccess) ==26039== Warning: set address range perms: large range [0x79e43040, 0x99e43040) (undefined) ==26039== Warning: set address range perms: large range [0x25bf1028, 0x45bf1058) (noaccess) ==26039== Warning: set address range perms: large range [0xd9e44040, 0x119e44040) (undefined) ==26039== Warning: set address range perms: large range [0x59e43028, 0x99e43058) (noaccess) ==26039== Warning: set address range perms: large range [0x199e45040, 0x219e45040) (undefined) ==26039== Warning: set address range perms: large range [0x99e44028, 0x119e44058) (noaccess) ==26039== Warning: set address range perms: large range [0x319e46040, 0x419e46040) (undefined) ==26039== Warning: set address range perms: large range [0x119e45028, 0x219e45058) (noaccess) ==26039== Warning: set address range perms: large range [0x619e47040, 0x819e47040) (undefined) ==26039== Warning: set address range perms: large range [0x219e46028, 0x419e46058) (noaccess) ==26039== Invalid write of size 8 ==26039== at 0x1197DA: pusht_bfr (in /home/user/boolector-plain) ==26039== by 0x11991C: new_line_bfr (in /home/user/boolector-plain) ==26039== by 0x1E9730: btor2parser_read_lines (in /home/user/boolector-plain) ==26039== by 0x1BB013: parse_btor2_parser (in /home/user/boolector-plain) ==26039== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==26039== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==26039== by 0x541AB96: (below main) (libc-start.c:310) ==26039== Address 0x400000000 is 8,155,537,344 bytes inside a block of size 8,589,934,592 free'd ==26039== at 0x4C31D2F: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==26039== by 0x1197C5: pusht_bfr (in /home/user/boolector-plain) ==26039== by 0x11991C: new_line_bfr (in /home/user/boolector-plain) ==26039== by 0x1E9730: btor2parser_read_lines (in /home/user/boolector-plain) ==26039== by 0x1BB013: parse_btor2_parser (in /home/user/boolector-plain) ==26039== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==26039== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==26039== by 0x541AB96: (below main) (libc-start.c:310) ==26039== Block was alloc'd at ==26039== at 0x4C31D2F: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==26039== by 0x1197C5: pusht_bfr (in /home/user/boolector-plain) ==26039== by 0x11991C: new_line_bfr (in /home/user/boolector-plain) ==26039== by 0x1E9730: btor2parser_read_lines (in /home/user/boolector-plain) ==26039== by 0x1BB013: parse_btor2_parser (in /home/user/boolector-plain) ==26039== by 0x16C6FD: btor_parse (in /home/user/boolector-plain) ==26039== by 0x128F87: boolector_main (in /home/user/boolector-plain) ==26039== by 0x541AB96: (below main) (libc-start.c:310) ==26039== boolector: line 5: expected tag ==26039== ==26039== HEAP SUMMARY: ==26039== in use at exit: 17,179,869,328 bytes in 3 blocks ==26039== total heap usage: 870 allocs, 867 frees, 68,719,507,815 bytes allocated ==26039== ==26039== LEAK SUMMARY: ==26039== definitely lost: 120 bytes in 1 blocks ==26039== indirectly lost: 24 bytes in 1 blocks ==26039== possibly lost: 17,179,869,184 bytes in 1 blocks ==26039== still reachable: 0 bytes in 0 blocks ==26039== suppressed: 0 bytes in 0 blocks ==26039== Rerun with --leak-check=full to see details of leaked memory ==26039== ==26039== For counts of detected and suppressed errors, rerun with: -v ==26039== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0) ```

Used version

$ boolector --version
3.0.1-pre

Steps to reproduce

boolector  pusht_bfr.btor2.txt
aniemetz commented 5 years ago

Good catch! This is actually a bug in the BTOR2 parser at https://github.com/Boolector/btor2tools. Fixed in https://github.com/Boolector/btor2tools/commit/c38dd5dc89f6bfa35810e3f648bb10f8ad824b39.