search

PKU-ASAL / SeeWasm

A native symbolic execution engine for WebAssembly
40 stars 3 forks source link

AssertionError in test.py sample stack_bo_l1.wasm and stack_bo_l2.wasm #57

Closed 99hansling closed 2 years ago

99hansling commented 2 years ago

Describe the bug In implement engine on stack_bo_l1.wasm, an AssertionError occurred. Here is the whole output information:

Start to analyze: 04-09 12:03:25
WARNING:root:From: main, invoke: __original_main
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246416============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246417============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246418============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246419============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246420============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246421============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246422============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246423============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246424============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l1.c_27_9_[0]_5246425============
WARNING:root:From: __original_main, invoke: logic_bomb
WARNING:root:Invoked a C library function: strcpy
Traceback (most recent call last):
  File "eunomia_entry", line 182, in <module>
    main()
  File "eunomia_entry", line 169, in main
    graph.traverse()
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 360, in traverse
    self.final_states[entry_func] = self.traverse_one(entry_func)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 159, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 159, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 133, in deal_with_call
    func.emul(state, param_str, return_str, data_section, analyzer)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/internalFunctions.py", line 207, in emul
    src_string = C_extract_string_by_mem_pointer(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/internalFunctions.py", line 991, in C_extract_string_by_mem_pointer
    assert default_len is not None, f"extract {mem_pointer} from memory, however, the loaded part is a symbol, the default len should not be None"
AssertionError: extract 5246416 from memory, however, the loaded part is a symbol, the default len should not be None

To Reproduce Steps to reproduce the behavior: 1.Use the command /usr/bin/python3 test.py e, you'll get the AssertionError under test.py context 2.Also you can reproduce the behavior by directly execute the command /usr/bin/python3 eunomia_entry -f ./Wasm-samples/c_samples.nosync/emcc/stack_bo_l1.wasm -s --onlyfunc main --need_mapper

Expected behavior The AssertionError will be resolved for good.

Additional context Just under python environment of the requirements with Ubuntu 20.09 LTS.

99hansling commented 2 years ago

As for stack_bo_l2.wasm, here is the same problem. Maybe the root cause is also the same:

Start to analyze: 04-09 12:31:45
WARNING:root:From: main, invoke: __original_main
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246416============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246417============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246418============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246419============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246420============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246421============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246422============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246423============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246424============
WARNING:root:Invoked a C library function: scanf
WARNING:root:============Initiated an scanf integer: scanf_source/stack_bo_l2.c_29_9_[0]_5246425============
WARNING:root:From: __original_main, invoke: logic_bomb
WARNING:root:Invoked a C library function: strcpy
Traceback (most recent call last):
  File "eunomia_entry", line 182, in <module>
    main()
  File "eunomia_entry", line 169, in main
    graph.traverse()
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 360, in traverse
    self.final_states[entry_func] = self.traverse_one(entry_func)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 159, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/HANSLXH/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 159, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 133, in deal_with_call
    func.emul(state, param_str, return_str, data_section, analyzer)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/internalFunctions.py", line 207, in emul
    src_string = C_extract_string_by_mem_pointer(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/internalFunctions.py", line 991, in C_extract_string_by_mem_pointer
    assert default_len is not None, f"extract {mem_pointer} from memory, however, the loaded part is a symbol, the default len should not be None"
AssertionError: extract 5246416 from memory, however, the loaded part is a symbol, the default len should not be None
HNYuuu commented 2 years ago

As the pr #58 says, the error in sample stack_bo_l1.wasm has been fixed. Also, the stacknocrash_bo_l1.wasm can be analyzed correctly.

However, the stack_bo_l2.wasm and the heap_bo_l1.wasm (in #56) cannot be fixed. Neither KLEE nor Angr can pass these two samples. Please skip these two samples at the current stage, maybe fix these two samples in the future.