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
335 stars 62 forks source link

Null Pointer Dereference in btor_bv_to_char() #166

Closed kinzhong closed 3 years ago

kinzhong commented 3 years ago

Hi,

There is a null pointer dereference in btor_bv_to_char() from btorbv.c.

To recreate: compile with ASAN enabled ./boolector poc

poc.zip

ASAN Logs: ==19782==ERROR: AddressSanitizer: SEGV on unknown address 0x602100004d4e (pc 0x7fc8ec1ec260 bp 0x7ffe0e3ccf60 sp 0x7ffe0e3ccf20 T0) ==19782==The signal is caused by a WRITE memory access.

0 0x7fc8ec1ec25f in btor_bv_to_char /home/kinzhong/Downloads/boolector/src/btorbv.c:660

#1 0x7fc8ec4a93eb in parse_consth /home/kinzhong/Downloads/boolector/src/parser/btorbtor.c:593
#2 0x7fc8ec4af0c0 in parse_btor_parser /home/kinzhong/Downloads/boolector/src/parser/btorbtor.c:1950
#3 0x7fc8ec308e70 in parse_aux /home/kinzhong/Downloads/boolector/src/btorparse.c:68
#4 0x7fc8ec308e70 in btor_parse /home/kinzhong/Downloads/boolector/src/btorparse.c:235
#5 0x55bbe7d121f4 in boolector_main /home/kinzhong/Downloads/boolector/src/btormain.c:1440
#6 0x7fc8ebcf7bf6 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21bf6)
#7 0x55bbe7cfc099 in _start (/home/kinzhong/Downloads/boolector/build/bin/boolector+0x5099)

AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV /home/kinzhong/Downloads/boolector/src/btorbv.c:660 in btor_bv_to_char ==19782==ABORTING

Please let me know if you have any issues with recreating the vulnerability. Thank you!

Best regards, Kin Zhong

aniemetz commented 3 years ago

I can't reproduce on master (configured with ./configure.sh --asan, and not with ./configure.sh -g --asan -- neither with gcc or clang). Which version of Boolector did you compile? If it was master, which commit? How did you configure Boolector?

kinzhong commented 3 years ago

This is strange, I tried recreating it again on the latest commit (aa1ff92c51df47ba6f4100cac10d32bc7041ab1a) of master and it works on my side. I used gcc version 7.5.0.

./configure.sh --asan cd build make

I have attached all the relevant logs for your reference. Thank you.

boolector-null-pointer-recreation.log

aniemetz commented 3 years ago

I'm an idiot, I had it parsed as smt2. Now I can reproduce, too.

aniemetz commented 3 years ago

Fixed in https://github.com/Boolector/boolector/commit/d2949abad6f81c4f0ed3b322787a2a54c7b5e3ef.