You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A Use-after-free problem was discovered in car function in btorsmt.c in src/parser. A crafted input can cause segment faults and I have confirmed them with address sanitizer too.
Here are the POC files. Please use ./boolector $POC to reproduce the bug. POC.zip
Note that similar issues were reported (#28 and #29) in the past, which is fixed. But this bug can still reproduce on the master branch.
$ git log
commit 0874a185cd98711b3e4a0b1a0c10e858ff4a23e6
Author: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri Mar 22 19:39:12 2019 -0700
btoruntrace: Fix mem leak.
The ASAN dumps the stack trace as follows:
=================================================================
==31295==ERROR: AddressSanitizer: heap-use-after-free on address 0x60300000e0b0 at pc 0x7f17e08cbb00 bp 0x7ffe777fdf20 sp 0x7ffe777fdf18
READ of size 8 at 0x60300000e0b0 thread T0
#0 0x7f17e08cbaff in car /boolector/src/parser/btorsmt.c:236:16
#1 0x7f17e08cbaff in recursively_delete_smt_node /boolector/src/parser/btorsmt.c:383
#2 0x7f17e08ca6c3 in release_smt_nodes /boolector/src/parser/btorsmt.c:443:5
#3 0x7f17e08ca6c3 in release_smt_internals /boolector/src/parser/btorsmt.c:449
#4 0x7f17e08c1de1 in parse_smt_parser /boolector/src/parser/btorsmt.c:2956:3
#5 0x7f17e0674ff1 in parse_aux /boolector/src/btorparse.c:68:15
#6 0x7f17e0673e81 in btor_parse /boolector/src/btorparse.c:230:9
#7 0x4f5138 in boolector_main /boolector/src/btormain.c:1462:19
#8 0x7f17df44882f in __libc_start_main /build/glibc-Cl5G7W/glibc-2.23/csu/../csu/libc-start.c:291
#9 0x419c58 in _start (/boolector/build/bin/boolector+0x419c58)
0x60300000e0b0 is located 0 bytes inside of 24-byte region [0x60300000e0b0,0x60300000e0c8)
freed by thread T0 here:
#0 0x4b9c00 in __interceptor_cfree.localalias.0 (/boolector/build/bin/boolector+0x4b9c00)
#1 0x7f17e08cc2e7 in recursively_delete_smt_node /boolector/src/parser/btorsmt.c:394:5
#2 0x7f17e08ca6c3 in release_smt_nodes /boolector/src/parser/btorsmt.c:443:5
#3 0x7f17e08ca6c3 in release_smt_internals /boolector/src/parser/btorsmt.c:449
#4 0x7f17e08c1de1 in parse_smt_parser /boolector/src/parser/btorsmt.c:2956:3
#5 0x7f17e0674ff1 in parse_aux /boolector/src/btorparse.c:68:15
#6 0x7f17e0673e81 in btor_parse /boolector/src/btorparse.c:230:9
#7 0x4f5138 in boolector_main /boolector/src/btormain.c:1462:19
#8 0x7f17df44882f in __libc_start_main /build/glibc-Cl5G7W/glibc-2.23/csu/../csu/libc-start.c:291
previously allocated by thread T0 here:
#0 0x4b9d88 in __interceptor_malloc (/boolector/build/bin/boolector+0x4b9d88)
#1 0x7f17e09f1d6b in btor_mem_malloc /boolector/src/utils/btormem.c:75:12
#2 0x7f17e08c151f in cons /boolector/src/parser/btorsmt.c:255:3
#3 0x7f17e08c151f in parse /boolector/src/parser/btorsmt.c:2889
#4 0x7f17e08c151f in parse_smt_parser /boolector/src/parser/btorsmt.c:2955
#5 0x7f17e0674ff1 in parse_aux /boolector/src/btorparse.c:68:15
#6 0x7f17e0673e81 in btor_parse /boolector/src/btorparse.c:230:9
#7 0x4f5138 in boolector_main /boolector/src/btormain.c:1462:19
#8 0x7f17df44882f in __libc_start_main /build/glibc-Cl5G7W/glibc-2.23/csu/../csu/libc-start.c:291
SUMMARY: AddressSanitizer: heap-use-after-free /boolector/src/parser/btorsmt.c:236:16 in car
Shadow bytes around the buggy address:
0x0c067fff9bc0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c067fff9bd0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c067fff9be0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
0x0c067fff9bf0: fa fa fa fa fa fa fa fa 00 00 00 fa fa fa 00 00
0x0c067fff9c00: 00 fa fa fa fd fd fd fd fa fa 00 00 00 fa fa fa
=>0x0c067fff9c10: fd fd fd fa fa fa[fd]fd fd fa fa fa fd fd fd fd
0x0c067fff9c20: fa fa 00 00 00 05 fa fa 00 00 07 fa fa fa fd fd
0x0c067fff9c30: fd fd fa fa 00 00 00 00 fa fa fd fd fd fd fa fa
0x0c067fff9c40: 00 00 00 00 fa fa 00 00 00 00 fa fa 00 00 00 00
0x0c067fff9c50: fa fa 00 00 00 00 fa fa 00 00 00 00 fa fa 00 00
0x0c067fff9c60: 00 00 fa fa fd fd fd fd fa fa fd fd fd fd fa 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
==31295==ABORTING
The text was updated successfully, but these errors were encountered:
This issue concerns the SMT-LIB v1 parser. SMT-LIB v1 is outdated, SMT-LIB v2 is the current standard. We do not actively support and maintain Boolector's parser for SMT-LIB v1 and thus won't fix this issue. Support for parsing SMT-LIB v1 input will be removed some time in the future.
Hi, there.
A Use-after-free problem was discovered in car function in btorsmt.c in src/parser. A crafted input can cause segment faults and I have confirmed them with address sanitizer too.
Here are the POC files. Please use
./boolector $POC
to reproduce the bug.POC.zip
Note that similar issues were reported (#28 and #29) in the past, which is fixed. But this bug can still reproduce on the master branch.
$ git log
The ASAN dumps the stack trace as follows:
The text was updated successfully, but these errors were encountered: