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

[Bug Report] Heap buffer-overflow in prase function in btoruntrace.c #42

Closed wcventure closed 5 years ago

wcventure commented 5 years ago

Hi, there.

A Heap-buffer-overflow in prase function in btoruntrace.c. A crafted input can cause segment faults and I have confirmed them with address sanitizer too.

Here are the POC files. Please use ./btoruntrace $POC to reproduce the bug. POC.zip

$ 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:

=================================================================
==9237==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x60400000a6f8 at pc 0x0000004f08a2 bp 0x7ffe219c03b0 sp 0x7ffe219c03a8
WRITE of size 1 at 0x60400000a6f8 thread T0
    #0 0x4f08a1 in parse /home/wencheng/Documents/FuzzingObject/boolector/src/btoruntrace.c:539:45
    #1 0x50ed8f in main /home/wencheng/Documents/FuzzingObject/boolector/src/btoruntrace.c:1867:3
    #2 0x7fef504ab82f in __libc_start_main /build/glibc-Cl5G7W/glibc-2.23/csu/../csu/libc-start.c:291
    #3 0x41c628 in _start (/home/wencheng/Documents/FuzzingObject/boolector/build/bin/btoruntrace+0x41c628)

0x60400000a6f8 is located 0 bytes to the right of 40-byte region [0x60400000a6d0,0x60400000a6f8)
allocated by thread T0 here:
    #0 0x4bc8e0 in calloc (/home/wencheng/Documents/FuzzingObject/boolector/build/bin/btoruntrace+0x4bc8e0)
    #1 0x7fef51a5566f in btor_mem_calloc /home/wencheng/Documents/FuzzingObject/boolector/src/utils/btormem.c:134:12
    #2 0x4ee4b8 in parse /home/wencheng/Documents/FuzzingObject/boolector/src/btoruntrace.c:442:3
    #3 0x50ed8f in main /home/wencheng/Documents/FuzzingObject/boolector/src/btoruntrace.c:1867:3
    #4 0x7fef504ab82f in __libc_start_main /build/glibc-Cl5G7W/glibc-2.23/csu/../csu/libc-start.c:291

SUMMARY: AddressSanitizer: heap-buffer-overflow /home/wencheng/Documents/FuzzingObject/boolector/src/btoruntrace.c:539:45 in parse
Shadow bytes around the buggy address:
  0x0c087fff9480: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c087fff9490: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c087fff94a0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c087fff94b0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c087fff94c0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
=>0x0c087fff94d0: fa fa fa fa fa fa fa fa fa fa 00 00 00 00 00[fa]
  0x0c087fff94e0: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x0c087fff94f0: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x0c087fff9500: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x0c087fff9510: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
  0x0c087fff9520: fa fa 00 00 00 00 00 00 fa fa 00 00 00 00 00 00
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
==9237==ABORTING
Aborted
mpreiner commented 5 years ago

@wcventure Thanks for reporting the bug! What tools did you use to find it?

wcventure commented 5 years ago

Hi @mpreiner

I Use AddressSanitizer(https://clang.llvm.org/docs/AddressSanitizer.html) to dump the backtrace. This tool is integrated in LLVM.

You can compile the program with ASAN, and then reproduce the bug with the test case I gave you.

change the line in confiugre.sh.

#!/bin/sh
#--------------------------------------------------------------------------#

BUILDDIR=build

#--------------------------------------------------------------------------#

asan=yes
debug=yes
check=no
log=no
shared=no
prefix=

asan=no -> asan=yes

mpreiner commented 5 years ago

Yes, I know about ASAN (you can configure Boolector with ./configure.sh --asan for that). What I actually meant was what input fuzzer/tool did you use to craft the failing inputs?

wcventure commented 5 years ago

I use AFL, a well-known fuzzing tool.