search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Double-free vulnerability in Z3 #2022

Closed nbars closed 5 years ago

nbars commented 5 years ago

Version: Z3 version 4.8.3

Description: Z3 suffers from a double-free vulnerability, that might be abused to hijack the control flow by exploiting the heap allocator.

Steps to reproduce (payload is attached): z3 [payload]

ASAN-Report

==3962==ERROR: AddressSanitizer: attempting double-free on 0x618000009880 in thread T0:
    #0 0x7fc7fb536c19 in __interceptor_free /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cc:66
    #1 0x560ab6234f9f in memory::deallocate(void*) (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x23e2f9f)
    #2 0x560ab61dcdbe in mpz_manager<false>::del(mpz&) (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x238adbe)
    #3 0x560ab62203b9 in mpq_manager<false>::~mpq_manager() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x23ce3b9)
    #4 0x560ab6015873 in ~imp ../src/nlsat/nlsat_solver.cpp:194
    #5 0x560ab5fdf29b in void dealloc<nlsat::solver::imp>(nlsat::solver::imp*) ../src/util/memory_manager.h:96
    #6 0x560ab5fdf29b in ~solver ../src/nlsat/nlsat_solver.cpp:3060
    #7 0x560ab490a99b in qe::nlqsat::~nlqsat() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0xab899b)
    #8 0x560ab5acc113 in or_else_tactical::~or_else_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c7a113)
    #9 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #10 0x560ab5acb938 in and_then_tactical::~and_then_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79938)
    #11 0x560ab5acb938 in and_then_tactical::~and_then_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79938)
    #12 0x560ab5acb938 in and_then_tactical::~and_then_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79938)
    #13 0x560ab5acbc0f in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c0f)
    #14 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #15 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #16 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #17 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #18 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #19 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #20 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #21 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #22 0x560ab5acbc40 in cond_tactical::~cond_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79c40)
    #23 0x560ab5acb938 in and_then_tactical::~and_then_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c79938)
    #24 0x560ab5acb8bf in using_params_tactical::~using_params_tactical() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1c798bf)
    #25 0x560ab599aa88 in (anonymous namespace)::tactic2solver::~tactic2solver() (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x1b48a88)
    #26 0x560ab59ba038 in void dealloc<check_sat_result>(check_sat_result*) ../src/util/memory_manager.h:96
    #27 0x560ab59ba038 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:49
    #28 0x560ab59ba038 in ref<solver>::dec_ref() ../src/util/ref.h:34
    #29 0x560ab59ba038 in ref<solver>::~ref() ../src/util/ref.h:55
    #30 0x560ab59ba038 in ~combined_solver ../src/solver/combined_solver.cpp:45
    #31 0x560ab5858a5f in void dealloc<check_sat_result>(check_sat_result*) ../src/util/memory_manager.h:96
    #32 0x560ab5858a5f in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:49
    #33 0x560ab5858a5f in ref<solver>::dec_ref() ../src/util/ref.h:34
    #34 0x560ab5858a5f in ref<solver>::operator=(solver*) ../src/util/ref.h:81
    #35 0x560ab5858a5f in cmd_context::reset(bool) ../src/cmd_context/cmd_context.cpp:1319
    #36 0x560ab5855dac in ~cmd_context ../src/cmd_context/cmd_context.cpp:501
    #37 0x560ab3f4d755 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:108
    #38 0x560ab3f59cbf in main ../src/shell/main.cpp:353
    #39 0x7fc7faed5222 in __libc_start_main (/usr/lib/libc.so.6+0x24222)
    #40 0x560ab3f2251d in _start (/home/nils/git/z3-crash-triage/z3-master/build/z3+0xd051d)

0x618000009880 is located 0 bytes inside of 832-byte region [0x618000009880,0x618000009bc0)
freed by thread T0 here:
    #0 0x7fc7fb536c19 in __interceptor_free /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cc:66
    #1 0x560ab6234f9f in memory::deallocate(void*) (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x23e2f9f)

previously allocated by thread T0 here:
    #0 0x7fc7fb537019 in __interceptor_malloc /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cc:86
    #1 0x560ab6234fe1 in memory::allocate(unsigned long) (/home/nils/git/z3-crash-triage/z3-master/build/z3+0x23e2fe1)

SUMMARY: AddressSanitizer: double-free /build/gcc/src/gcc/libsanitizer/asan/asan_malloc_linux.cc:66 in __interceptor_free

Payload: bug.zip

Credits: Tim Blazytko Cornelius Aschermann Sergej Schumilo Nils Bars

nunoplopes commented 5 years ago

I'm unable to reproduce this with valgrind. Which options did you use for compilation?

nunoplopes commented 5 years ago

BTW, of course we are interested in solving this bug, but calling it an exploitable vulnerability is a bit of a stretch.. We are not getting a CVE report for this for sure.

nbars commented 5 years ago

It seems like something went wrong while minimizing this test case. This test case only crashes if z3 is compiled with afl-clang-fast.

LDFLAGS='-ldl -lgomp' CPPFLAGS="-g -DDEBUG" CXX=afl-clang-fast++  ./configure

Here is the not minimized test case: bug01.zip

Compiling:

LDFLAGS='-ldl -lgomp' CPPFLAGS="-g -DDEBUG" CXX=clang  ./configure

Valgrind output:

./valgrind z3 bug01
==4176== Memcheck, a memory error detector
==4176== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==4176== Using Valgrind-3.14.0 and LibVEX; rerun with -h for copyright info
==4176== Command: ./z3 /tmp/bug01
==4176== 
==4176== Use of uninitialised value of size 8
==4176==    at 0x11925C7: sexpr::display(std::ostream&) const (sexpr.cpp:204)
==4176==    by 0x26452E: sexpr_cmd::set_next_arg(cmd_context&, sexpr*) (dbg_cmds.cpp:245)
==4176==    by 0xAC3D53: smt2::parser::parse_next_cmd_arg() (smt2parser.cpp:2879)
==4176==    by 0xAC476B: smt2::parser::parse_ext_cmd(int, int) (smt2parser.cpp:2937)
==4176==    by 0xAC6172: parse_cmd (smt2parser.cpp:3026)
==4176==    by 0xAC6172: smt2::parser::operator()() (smt2parser.cpp:3138)
==4176==    by 0xAB330F: parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (smt2parser.cpp:3187)
==4176==    by 0x25557B: read_smtlib2_commands(char const*) (smtlib_frontend.cpp:95)
==4176==    by 0x237598: main (main.cpp:353)
==4176== 
==4176== Invalid read of size 4
==4176==    at 0x11925C7: sexpr::display(std::ostream&) const (sexpr.cpp:204)
==4176==    by 0x26452E: sexpr_cmd::set_next_arg(cmd_context&, sexpr*) (dbg_cmds.cpp:245)
==4176==    by 0xAC3D53: smt2::parser::parse_next_cmd_arg() (smt2parser.cpp:2879)
==4176==    by 0xAC476B: smt2::parser::parse_ext_cmd(int, int) (smt2parser.cpp:2937)
==4176==    by 0xAC6172: parse_cmd (smt2parser.cpp:3026)
==4176==    by 0xAC6172: smt2::parser::operator()() (smt2parser.cpp:3138)
==4176==    by 0xAB330F: parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (smt2parser.cpp:3187)
==4176==    by 0x25557B: read_smtlib2_commands(char const*) (smtlib_frontend.cpp:95)
==4176==    by 0x237598: main (main.cpp:353)
==4176==  Address 0x100000001 is not stack'd, malloc'd or (recently) free'd
==4176== 
==4176== 
==4176== Process terminating with default action of signal 11 (SIGSEGV): dumping core
==4176==  Access not within mapped region at address 0x100000001
==4176==    at 0x11925C7: sexpr::display(std::ostream&) const (sexpr.cpp:204)
==4176==    by 0x26452E: sexpr_cmd::set_next_arg(cmd_context&, sexpr*) (dbg_cmds.cpp:245)
==4176==    by 0xAC3D53: smt2::parser::parse_next_cmd_arg() (smt2parser.cpp:2879)
==4176==    by 0xAC476B: smt2::parser::parse_ext_cmd(int, int) (smt2parser.cpp:2937)
==4176==    by 0xAC6172: parse_cmd (smt2parser.cpp:3026)
==4176==    by 0xAC6172: smt2::parser::operator()() (smt2parser.cpp:3138)
==4176==    by 0xAB330F: parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (smt2parser.cpp:3187)
==4176==    by 0x25557B: read_smtlib2_commands(char const*) (smtlib_frontend.cpp:95)
==4176==    by 0x237598: main (main.cpp:353)
==4176==  If you believe this happened as a result of a stack
==4176==  overflow in your program's main thread (unlikely but
==4176==  possible), you can try to increase the size of the
==4176==  main thread stack using the --main-stacksize= flag.
==4176==  The main thread stack size used in this run was 8388608.
==4176== 
==4176== HEAP SUMMARY:
==4176==     in use at exit: 2,942,347 bytes in 10,825 blocks
==4176==   total heap usage: 34,454 allocs, 23,629 frees, 10,591,095 bytes allocated
==4176== 
==4176== LEAK SUMMARY:
==4176==    definitely lost: 0 bytes in 0 blocks
==4176==    indirectly lost: 0 bytes in 0 blocks
==4176==      possibly lost: 2,912,587 bytes in 10,801 blocks
==4176==    still reachable: 29,760 bytes in 24 blocks
==4176==         suppressed: 0 bytes in 0 blocks
==4176== Rerun with --leak-check=full to see details of leaked memory
==4176== 
==4176== For counts of detected and suppressed errors, rerun with: -v
==4176== Use --track-origins=yes to see where uninitialised values come from
==4176== ERROR SUMMARY: 2 errors from 2 contexts (suppressed: 0 from 0)
NikolajBjorner commented 5 years ago

the zip file looks like junk (corrupted). It does not exercise the code mentioned in the trace. Furthermore, looks like stack overflow.