Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use after Free in get_failed_assumptions #29

Closed
bugs-syssec opened this issue Jan 15, 2019 · 1 comment
Closed

Use after Free in get_failed_assumptions #29

bugs-syssec opened this issue Jan 15, 2019 · 1 comment
Assignees
@aniemetz

Comments

@bugs-syssec
Copy link

While fuzzing boolector,

this input file 
(assert#b0)
(check-sat)
(get-unsat-assumptions)
(get-unsat-assumptions)

was found, which leads to a use after free in get_failed_assumptions.

The input file looks like this is related to #28, but the backtrace produced by ASAN is different, which is why this is filed as a separate issue.

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

ASAN trace 
=================================================================
==9780==ERROR: AddressSanitizer: heap-use-after-free on address 0x602000009710 at pc 0x00000052bd1c bp 0x7ffd2e8c9eb0 sp 0x7ffd2e8c9ea8
READ of size 8 at 0x602000009710 thread T0
    #0 0x52bd1b in boolector_get_failed_assumptions /home/user/boolector-master/src/boolector.c:624:12
    #1 0x6851db in read_command_smt2 /home/user/boolector-master/src/parser/btorsmt2.c:4700:28
    #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 0x7f53f5a65b96 in __libc_start_main /build/glibc-OTsEL5/glibc-2.27/csu/../csu/libc-start.c:310
    #7 0x4367a9 in _start (/home/user/boolector-asan+0x4367a9)

0x602000009710 is located 0 bytes inside of 8-byte region [0x602000009710,0x602000009718)
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 0x7f53f5a65b96 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 0x7f53f5a65b96 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/boolector.c:624:12 in boolector_get_failed_assumptions
Shadow bytes around the buggy address:
  0x0c047fff9290: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff92a0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff92b0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff92c0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff92d0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
=>0x0c047fff92e0: fa fa[fd]fa fa fa 00 fa fa fa fd fd fa fa fd fa
  0x0c047fff92f0: fa fa fd fd fa fa fd fd fa fa fd fa fa fa fd fa
  0x0c047fff9300: fa fa fd fa fa fa fd fa fa fa 04 fa fa fa 04 fa
  0x0c047fff9310: fa fa 05 fa fa fa 03 fa fa fa 06 fa fa fa 06 fa
  0x0c047fff9320: fa fa 00 01 fa fa 00 01 fa fa 00 01 fa fa 00 01
  0x0c047fff9330: fa fa 00 fa fa fa 06 fa fa fa 07 fa fa fa 07 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
==9780==ABORTING
Valgrind trace 
==9802== Memcheck, a memory error detector
==9802== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==9802== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==9802== Command: ./boolector-plain boolector_get_failed_assumptions.txt
==9802== 
==9802== Invalid read of size 8
==9802==    at 0x12B0AD: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==9802==    by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Address 0x5809830 is 0 bytes inside a block of size 8 free'd
==9802==    at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Block was alloc'd at
==9802==    at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain)
==9802==    by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==9802==    by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802== 
==9802== Invalid free() / delete / delete[] / realloc()
==9802==    at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x12B10A: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==9802==    by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Address 0x5809830 is 0 bytes inside a block of size 8 free'd
==9802==    at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Block was alloc'd at
==9802==    at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain)
==9802==    by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==9802==    by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802== 
==9802== Invalid read of size 8
==9802==    at 0x14BC53: btor_delete (in /home/user/boolector-plain)
==9802==    by 0x127EC9: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Address 0x5809880 is 0 bytes inside a block of size 8 free'd
==9802==    at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Block was alloc'd at
==9802==    at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain)
==9802==    by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==9802==    by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802== 
==9802== Invalid free() / delete / delete[] / realloc()
==9802==    at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x14BC8E: btor_delete (in /home/user/boolector-plain)
==9802==    by 0x127EC9: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Address 0x5809880 is 0 bytes inside a block of size 8 free'd
==9802==    at 0x4C30D3B: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1CA705: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802==  Block was alloc'd at
==9802==    at 0x4C2FA3F: malloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x4C31D84: realloc (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so)
==9802==    by 0x1D906D: btor_mem_realloc (in /home/user/boolector-plain)
==9802==    by 0x12B1B2: boolector_get_failed_assumptions (in /home/user/boolector-plain)
==9802==    by 0x1CA6D2: read_command_smt2 (in /home/user/boolector-plain)
==9802==    by 0x1CC289: parse_smt2_parser (in /home/user/boolector-plain)
==9802==    by 0x16C6FD: btor_parse (in /home/user/boolector-plain)
==9802==    by 0x128F87: boolector_main (in /home/user/boolector-plain)
==9802==    by 0x541AB96: (below main) (libc-start.c:310)
==9802== 
==9802== 
==9802== HEAP SUMMARY:
==9802==     in use at exit: 0 bytes in 0 blocks
==9802==   total heap usage: 1,164 allocs, 1,166 frees, 46,991 bytes allocated
==9802== 
==9802== All heap blocks were freed -- no leaks are possible
==9802== 
==9802== For counts of detected and suppressed errors, rerun with: -v
==9802== ERROR SUMMARY: 4 errors from 4 contexts (suppressed: 0 from 0)

Used version

$ boolector --version
3.0.1-pre

Steps to reproduce

boolector  boolector_get_failed_assumptions.txt
@aniemetz
Copy link
Member

Related to #28. Fixed in 8d979d0.

@aniemetz aniemetz self-assigned this Jan 15, 2019
@wcventure wcventure mentioned this issue Mar 27, 2019
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@aniemetz aniemetz

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@aniemetz @bugs-syssec