Use After Free in btor_delete
bugs-syssec opened this issue · 1 comments
bugs-syssec commented
While fuzzing boolector,
this input file
(assert(bvcomp#xe#x5))
(check-sat)
(get-unsat-assumptions)
The attached file contains more lines leading to the same crash, the above file contains the minimal version.
ASAN trace
=================================================================
==25480==ERROR: AddressSanitizer: heap-use-after-free on address 0x602000009490 at pc 0x000000569948 bp 0x7ffe250893f0 sp 0x7ffe250893e8
READ of size 8 at 0x602000009490 thread T0
#0 0x569947 in btor_delete /home/user/boolector-master/src/btorcore.c:933:9
#1 0x5263d6 in btormain_delete_btormain /home/user/boolector-master/src/btormain.c:457:3
#2 0x5263d6 in boolector_main /home/user/boolector-master/src/btormain.c:1625
#3 0x7fc17c831b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310
#4 0x4367a9 in _start (/home/user/boolector-asan+0x4367a9)
0x602000009490 is located 0 bytes inside of 8-byte region [0x602000009490,0x602000009498)
freed by thread T0 here:
#0 0x4e5bc8 in __interceptor_free.localalias.0 (/home/user/boolector-asan+0x4e5bc8)
#1 0x68525b in read_command_smt2 /home/user/boolector-master/src/parser/btorsmt2.c:4706:7
#2 0x682a27 in parse_smt2_parser /home/user/boolector-master/src/parser/btorsmt2.c:4828:10
#3 0x5a033a in parse_aux /home/user/boolector-master/src/btorparse.c:68:15
#4 0x59f55a in btor_parse /home/user/boolector-master/src/btorparse.c:230:9
#5 0x52531e in boolector_main /home/user/boolector-master/src/btormain.c:1454:19
#6 0x7fc17c831b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310
previously allocated by thread T0 here:
#0 0x4e61a5 in realloc (/home/user/boolector-asan+0x4e61a5)
#1 0x6cd24e in btor_mem_realloc /home/user/boolector-master/src/utils/btormem.c:104:12
#2 0x52bc11 in boolector_get_failed_assumptions /home/user/boolector-master/src/boolector.c:633:3
#3 0x6851db in read_command_smt2 /home/user/boolector-master/src/parser/btorsmt2.c:4700:28
#4 0x682a27 in parse_smt2_parser /home/user/boolector-master/src/parser/btorsmt2.c:4828:10
#5 0x5a033a in parse_aux /home/user/boolector-master/src/btorparse.c:68:15
#6 0x59f55a in btor_parse /home/user/boolector-master/src/btorparse.c:230:9
#7 0x52531e in boolector_main /home/user/boolector-master/src/btormain.c:1454:19
#8 0x7fc17c831b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310
SUMMARY: AddressSanitizer: heap-use-after-free /home/user/boolector-master/src/btorcore.c:933:9 in btor_delete
Shadow bytes around the buggy address:
0x0c047fff9240: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c047fff9250: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c047fff9260: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c047fff9270: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c047fff9280: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
=>0x0c047fff9290: fa fa[fd]fa fa fa fd fa fa fa fd fd fa fa fd fa
0x0c047fff92a0: fa fa fd fd fa fa fd fd fa fa fd fd fa fa fd fd
0x0c047fff92b0: fa fa fd fd fa fa fd fd fa fa fd fd fa fa fd fa
0x0c047fff92c0: fa fa fd fd fa fa fd fd fa fa fd fa fa fa fd fa
0x0c047fff92d0: fa fa fd fd fa fa fd fd fa fa 00 00 fa fa fd fd
0x0c047fff92e0: fa fa fd fd fa fa fd fd fa fa fd fa fa fa fd fa
Shadow byte legend (one shadow byte represents 8 application bytes):
Addressable: 00
Partially addressable: 01 02 03 04 05 06 07
Heap left redzone: fa
Heap right redzone: fb
Freed heap region: fd
Stack left redzone: f1
Stack mid redzone: f2
Stack right redzone: f3
Stack partial redzone: f4
Stack after return: f5
Stack use after scope: f8
Global redzone: f9
Global init order: f6
Poisoned by user: f7
Container overflow: fc
Array cookie: ac
Intra object redzone: bb
ASan internal: fe
Left alloca redzone: ca
Right alloca redzone: cb
==25480==ABORTING
Valgrind trace
==25740== Memcheck, a memory error detector
==25740== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==25740== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==25740== Command: ./boolector-plain btor_delete.txt
==25740==
==25740== Invalid read of size 8
==25740== at 0x14BC53: btor_delete (in /home/user/boolector-plain)
==25740== by 0x127EC9: boolector_main (in /home/user/boolector-plain)
==25740== by 0x541AB96: (below main) (libc-start.c:310)
==25740== Address 0x580a420 is 0 bytes inside a block of size 8 free'd
==25740== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain)
==25740== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==25740== by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==25740== by 0x128F87: boolector_main (in /home/user/boolector-plain)
==25740== by 0x541AB96: (below main) (libc-start.c:310)
==25740== Block was alloc'd at
==25740== at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain)
==25740== by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==25740== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==25740== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==25740== by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==25740== by 0x128F87: boolector_main (in /home/user/boolector-plain)
==25740== by 0x541AB96: (below main) (libc-start.c:310)
==25740==
==25740== Invalid free() / delete / delete[] / realloc()
==25740== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x14BC8E: btor_delete (in /home/user/boolector-plain)
==25740== by 0x127EC9: boolector_main (in /home/user/boolector-plain)
==25740== by 0x541AB96: (below main) (libc-start.c:310)
==25740== Address 0x580a420 is 0 bytes inside a block of size 8 free'd
==25740== at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain)
==25740== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==25740== by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==25740== by 0x128F87: boolector_main (in /home/user/boolector-plain)
==25740== by 0x541AB96: (below main) (libc-start.c:310)
==25740== Block was alloc'd at
==25740== at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==25740== by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain)
==25740== by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==25740== by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==25740== by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==25740== by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==25740== by 0x128F87: boolector_main (in /home/user/boolector-plain)
==25740== by 0x541AB96: (below main) (libc-start.c:310)
==25740==
==25740==
==25740== HEAP SUMMARY:
==25740== in use at exit: 0 bytes in 0 blocks
==25740== total heap usage: 1,193 allocs, 1,194 frees, 47,978 bytes allocated
==25740==
==25740== All heap blocks were freed -- no leaks are possible
==25740==
==25740== For counts of detected and suppressed errors, rerun with: -v
==25740== ERROR SUMMARY: 2 errors from 2 contexts (suppressed: 0 from 0)
Used version
$ boolector --version
3.0.1-pre
Steps to reproduce
boolector btor_delete.txt