search

Z3Prover / z3

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

use after free in ../src/math/lp/emonics.cpp:90 nla::emonics::insert_cell(nla::emonics::head_tail&, unsigned int) #3371

Closed 5hadowblad3 closed 4 years ago

5hadowblad3 commented 4 years ago

Hi, there.

There is a use after free issue that causes segmentation fault using z3. It might also become exploitable since it can modify the memory space.

To reproduce this issue, simply run z3 poc.smt2

z3-uaf_emonics90.smt2.zip

OS: Ubuntu 16.06 commit 6ad261e

Here is the trace reported by ASAN.

=================================================================
==35268==ERROR: AddressSanitizer: heap-use-after-free on address 0x60300003c288 at pc 0x000001e37735 bp 0x7ffdb0124400 sp 0x7ffdb01243f0
WRITE of size 8 at 0x60300003c288 thread T0
    #0 0x1e37734 in nla::emonics::insert_cell(nla::emonics::head_tail&, unsigned int) ../src/math/lp/emonics.cpp:90
    #1 0x1e39916 in nla::emonics::add(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/emonics.cpp:294
    #2 0x1e1dede in nla::emonics::add(unsigned int, old_svector<unsigned int, unsigned int> const&) ../src/math/lp/emonics.h:156
    #3 0x1e071e9 in nla::core::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/nla_core.cpp:142
    #4 0x1d4db12 in nla::solver::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/nla_solver.cpp:30
    #5 0xdae649 in smt::theory_lra::imp::switcher::add_monic(unsigned int, unsigned int, unsigned int const*) (/home/heqing/dependence/z3/build/z3+0xdae649)
    #6 0xdb29eb in smt::theory_lra::imp::internalize_mul(app*, int&, rational&) ../src/smt/theory_lra.cpp:698
    #7 0xdb15a5 in smt::theory_lra::imp::linearize(smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb15a5)
    #8 0xdb0e88 in smt::theory_lra::imp::linearize_term(expr*, smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb0e88)
    #9 0xdb4507 in smt::theory_lra::imp::internalize_def(app*) (/home/heqing/dependence/z3/build/z3+0xdb4507)
    #10 0xdb6da4 in smt::theory_lra::imp::internalize_term(app*) (/home/heqing/dependence/z3/build/z3+0xdb6da4)
    #11 0xda7fe3 in smt::theory_lra::internalize_term(app*) ../src/smt/theory_lra.cpp:3935
    #12 0x1105181 in smt::context::internalize_theory_term(app*) ../src/smt/smt_internalizer.cpp:834
    #13 0x1104357 in smt::context::internalize_term(app*) ../src/smt/smt_internalizer.cpp:773
    #14 0x1100331 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:358
    #15 0x10ffd7a in smt::context::internalize(expr*, bool) ../src/smt/smt_internalizer.cpp:339
    #16 0xdb21db in smt::theory_lra::imp::internalize_args(app*) (/home/heqing/dependence/z3/build/z3+0xdb21db)
    #17 0xdb2385 in smt::theory_lra::imp::internalize_mul(app*, int&, rational&) ../src/smt/theory_lra.cpp:665
    #18 0xdb15a5 in smt::theory_lra::imp::linearize(smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb15a5)
    #19 0xdb0e88 in smt::theory_lra::imp::linearize_term(expr*, smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb0e88)
    #20 0xdb4507 in smt::theory_lra::imp::internalize_def(app*) (/home/heqing/dependence/z3/build/z3+0xdb4507)
    #21 0xdb6634 in smt::theory_lra::imp::internalize_atom(app*, bool) (/home/heqing/dependence/z3/build/z3+0xdb6634)
    #22 0xda7f94 in smt::theory_lra::internalize_atom(app*, bool) ../src/smt/theory_lra.cpp:3932
    #23 0x1101a51 in smt::context::internalize_theory_atom(app*, bool) ../src/smt/smt_internalizer.cpp:468
    #24 0x1100d39 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:411
    #25 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #26 0x1103623 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:587
    #27 0x1100da7 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:416
    #28 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #29 0x1103623 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:587
    #30 0x1100da7 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:416
    #31 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #32 0x1100739 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:374
    #33 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #34 0x1103623 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:587
    #35 0x1100da7 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:416
    #36 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #37 0x1100739 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:374
    #38 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #39 0x1103623 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:587
    #40 0x1100da7 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:416
    #41 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #42 0x10fe8b3 in smt::context::internalize_assertion(expr*, app*, unsigned int) ../src/smt/smt_internalizer.cpp:245
    #43 0x11b150c in smt::context::internalize_assertions() ../src/smt/smt_context.cpp:3135
    #44 0x11b572b in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3526
    #45 0x11225c2 in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #46 0x11212a3 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #47 0xc4d0fb in ctx_solver_simplify_tactic::reduce(goal&) (/home/heqing/dependence/z3/build/z3+0xc4d0fb)
    #48 0xc4c82d in ctx_solver_simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/heqing/dependence/z3/build/z3+0xc4c82d)
    #49 0x19deb87 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:909
    #50 0x19d7954 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #51 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #52 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #53 0x19dd595 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763
    #54 0x1a0cc80 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #55 0x1a0d11b in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:168
    #56 0x191b73e in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
    #57 0x18c072d in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
    #58 0x18c0f3e in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
    #59 0x18c2319 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #60 0x18a12fe in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #61 0x41efab in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #62 0x415a9e in main ../src/shell/main.cpp:352
    #63 0x7fe5421f382f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #64 0x414808 in _start (/home/heqing/dependence/z3/build/z3+0x414808)

0x60300003c288 is located 8 bytes inside of 24-byte region [0x60300003c280,0x60300003c298)
freed by thread T0 here:
    #0 0x7fe5430f32ca in __interceptor_free (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x982ca)
    #1 0x253bd89 in memory::deallocate(void*) ../src/util/memory_manager.cpp:260
    #2 0x4754de in void dealloc_svect<char>(char*) ../src/util/memory_manager.h:128
    #3 0xa41c77 in region::pop_scope() ../src/util/region.h:63
    #4 0xa41cbd in region::pop_scope(unsigned int) ../src/util/region.h:70
    #5 0x1e3744c in nla::emonics::pop(unsigned int) ../src/math/lp/emonics.cpp:64
    #6 0x1e073f4 in nla::core::pop(unsigned int) ../src/math/lp/nla_core.cpp:153
    #7 0x1d4dc4c in nla::solver::pop(unsigned int) ../src/math/lp/nla_solver.cpp:48
    #8 0xdae526 in smt::theory_lra::imp::switcher::pop(unsigned int) (/home/heqing/dependence/z3/build/z3+0xdae526)
    #9 0xdb8277 in smt::theory_lra::imp::pop_scope_eh(unsigned int) (/home/heqing/dependence/z3/build/z3+0xdb8277)
    #10 0xda82b6 in smt::theory_lra::pop_scope_eh(unsigned int) ../src/smt/theory_lra.cpp:3963
    #11 0x11a9892 in smt::context::pop_scope_core(unsigned int) ../src/smt/smt_context.cpp:2436
    #12 0x11a9d73 in smt::context::pop_scope(unsigned int) ../src/smt/smt_context.cpp:2477
    #13 0x11ae691 in smt::context::pop(unsigned int) ../src/smt/smt_context.cpp:2918
    #14 0x1122540 in smt::kernel::imp::pop(unsigned int) ../src/smt/smt_kernel.cpp:100
    #15 0x1120eed in smt::kernel::pop(unsigned int) ../src/smt/smt_kernel.cpp:272
    #16 0xc4cc0c in ctx_solver_simplify_tactic::reduce(goal&) (/home/heqing/dependence/z3/build/z3+0xc4cc0c)
    #17 0xc4c82d in ctx_solver_simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/heqing/dependence/z3/build/z3+0xc4c82d)
    #18 0x19deb87 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:909
    #19 0x19d7954 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #20 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #21 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #22 0x19dd595 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763
    #23 0x1a0cc80 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #24 0x1a0d11b in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:168
    #25 0x191b73e in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
    #26 0x18c072d in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
    #27 0x18c0f3e in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
    #28 0x18c2319 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #29 0x18a12fe in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179

previously allocated by thread T0 here:
    #0 0x7fe5430f3602 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98602)
    #1 0x253bdd5 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x6327ba in region::allocate(unsigned long) ../src/util/region.h:37
    #3 0x6328ec in operator new(unsigned long, region&) ../src/util/region.h:113
    #4 0x1e3764c in nla::emonics::insert_cell(nla::emonics::head_tail&, unsigned int) ../src/math/lp/emonics.cpp:87
    #5 0x1e39916 in nla::emonics::add(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/emonics.cpp:294
    #6 0x1e1dede in nla::emonics::add(unsigned int, old_svector<unsigned int, unsigned int> const&) ../src/math/lp/emonics.h:156
    #7 0x1e071e9 in nla::core::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/nla_core.cpp:142
    #8 0x1d4db12 in nla::solver::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/nla_solver.cpp:30
    #9 0xdae649 in smt::theory_lra::imp::switcher::add_monic(unsigned int, unsigned int, unsigned int const*) (/home/heqing/dependence/z3/build/z3+0xdae649)
    #10 0xdb29eb in smt::theory_lra::imp::internalize_mul(app*, int&, rational&) ../src/smt/theory_lra.cpp:698
    #11 0xdb15a5 in smt::theory_lra::imp::linearize(smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb15a5)
    #12 0xdb0e88 in smt::theory_lra::imp::linearize_term(expr*, smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb0e88)
    #13 0xdb4507 in smt::theory_lra::imp::internalize_def(app*) (/home/heqing/dependence/z3/build/z3+0xdb4507)
    #14 0xdb6da4 in smt::theory_lra::imp::internalize_term(app*) (/home/heqing/dependence/z3/build/z3+0xdb6da4)
    #15 0xda7fe3 in smt::theory_lra::internalize_term(app*) ../src/smt/theory_lra.cpp:3935
    #16 0x1105181 in smt::context::internalize_theory_term(app*) ../src/smt/smt_internalizer.cpp:834
    #17 0x1104357 in smt::context::internalize_term(app*) ../src/smt/smt_internalizer.cpp:773
    #18 0x1100331 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:358
    #19 0x10ffd7a in smt::context::internalize(expr*, bool) ../src/smt/smt_internalizer.cpp:339
    #20 0xdb21db in smt::theory_lra::imp::internalize_args(app*) (/home/heqing/dependence/z3/build/z3+0xdb21db)
    #21 0xdb2385 in smt::theory_lra::imp::internalize_mul(app*, int&, rational&) ../src/smt/theory_lra.cpp:665
    #22 0xdb15a5 in smt::theory_lra::imp::linearize(smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb15a5)
    #23 0xdb0e88 in smt::theory_lra::imp::linearize_term(expr*, smt::theory_lra::imp::scoped_internalize_state&) (/home/heqing/dependence/z3/build/z3+0xdb0e88)
    #24 0xdb4507 in smt::theory_lra::imp::internalize_def(app*) (/home/heqing/dependence/z3/build/z3+0xdb4507)
    #25 0xdb6634 in smt::theory_lra::imp::internalize_atom(app*, bool) (/home/heqing/dependence/z3/build/z3+0xdb6634)
    #26 0xda7f94 in smt::theory_lra::internalize_atom(app*, bool) ../src/smt/theory_lra.cpp:3932
    #27 0x1101a51 in smt::context::internalize_theory_atom(app*, bool) ../src/smt/smt_internalizer.cpp:468
    #28 0x1100d39 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:411
    #29 0x1100241 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350

SUMMARY: AddressSanitizer: heap-use-after-free ../src/math/lp/emonics.cpp:90 nla::emonics::insert_cell(nla::emonics::head_tail&, unsigned int)
Shadow bytes around the buggy address:
  0x0c067ffff800: fa fa fd fd fd fd fa fa 00 00 00 00 fa fa fd fd
  0x0c067ffff810: fd fa fa fa fd fd fd fd fa fa fd fd fd fd fa fa
  0x0c067ffff820: fd fd fd fd fa fa fd fd fd fd fa fa 00 00 00 fa
  0x0c067ffff830: fa fa fd fd fd fd fa fa fd fd fd fd fa fa fd fd
  0x0c067ffff840: fd fd fa fa fd fd fd fd fa fa fd fd fd fa fa fa
=>0x0c067ffff850: fd[fd]fd fa fa fa fd fd fd fa fa fa fd fd fd fa
  0x0c067ffff860: fa fa fd fd fd fa fa fa fd fd fd fd fa fa fd fd
  0x0c067ffff870: fd fd fa fa fd fd fd fd fa fa fd fd fd fd fa fa
  0x0c067ffff880: fd fd fd fd fa fa fd fd fd fd fa fa fd fd fd fa
  0x0c067ffff890: fa fa fd fd fd fd fa fa 00 00 00 fa fa fa fd fd
  0x0c067ffff8a0: fd fd fa fa 00 00 00 00 fa fa fd fd fd fa 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
==35268==ABORTING
NikolajBjorner commented 4 years ago

given that this is likely related to the other "use-after-free" occurrences in emonics, it is better to just list them in the same issue. No need to file different issues

NikolajBjorner commented 4 years ago

they seem addressed in the debug branch, but reproduce in the master. The debug branch has addressed bugs in emonics so the master is behind on this functionality.

As noted before: bugs that are triggered by smt.arith.solver = 6 are only relevant to test against the debug branch at this point. Therefore closing as it seems fixed in Debug.