Offline Execution Mode

[montyly]

Summary of the problem

As an online symbolic execution, Manticore explores systematically all the paths of the program with respect to the symbolic inputs. While this is perfect to fully verify a target, it brings a significant overhead when Manticore is used as an exploit-generation tool. The idea is to add an "offline" mode where Manticore will explore a given trace, and reason symbolic on top of it, without exploring by the branches.

In many cases, we use Manticore to analyze a particular scenario/potential exploit. In those situations, we don't care about exploring the paths, as we want to validate/invalidate a PoC. So far, we were able to follow the process highlighted in test_exploit_generation_example, but it brings a significant amount of code to the script, and if far from being optimized.

We could add an offline mode directly to the API, to be set at the Manticore creation that will:

• Follow the concrete execution trace, without exploring the branches
• Build alongside the path predicate the same way it does in the online mode

In another term, it means to execute a concrete path while not concretizing the inputs leading to this path.

As the branches are not explored, we will also save all the solver queries on branches resolution. In term of API, in the offline mode, make_symbolic_value could take, for example, an additional argument (ex: concrete_value), so Manticore will have all the information to follow the concrete trace.

Example of usage:

m = ManticoreEVM(mode="offline")

user_account = m.create_account()
contract_account = m.solidity_create_contract("contract.sol")

input = m.make_symbolic_value(name="my_input", concrete_value=10)

contract_account.my_func(input)

# Some constraint on the return value
for state in m.ready_states:
    world = state.platform
    ret = world.human_transactions[-1]

    ret_val = ABI.deserialize("uint", ret.return_data)

    m.generate_testcase(state, name="Exploit", only_if=ret_val > 100)

m.finalize()

Here Manticore will explore only one path (my_func(10)) but will be able to reason symbolically on top of it.

In the long run, we could imagine mixing both modes, where concrete_value in make_symbolic_value is optional, and Manticore would be able to explore a subset of the paths validating the inputs.

[MatthewARinehart]

Identified as Manticore has an offline execution mode and Support sage mode (EVM) outcomes on the Q3 prioritization exercise.