Analysis Tips
We recommend following the guidelines below to ensure Manticore tests achieve the highest degree of coverage, performance, and efficacy.
- Always use an UNSAT check to verify properties, not SAT. Testing that the constraints of a path are satisfiable (SAT) does not mean that the constraints are always true, but only that these constraints are satisfiable for at least one valuation of the inputs. A property should be tested by checking the unsatisfiability (UNSAT) of the negation of the property. Applicable APIs include state.must_be_true and state.can_be_true.
- Certain CLI flags can help improve performance a lot:
-
--txlimit: put hard limit on symbolic transactions if you know you don't need more than a certain amount -
--avoid-constants: ignore functions marked as constant as they claim they wont effect the contract state -
--limit-loops: extremely useful if the contract reassigns an array length -
--txnoether: ignore gas calculations during contract execution - Only enable detectors when you need them. Each detector adds some performance overhead.
-
- Use m.all_states or m.busy_states to check for properties on running states. Some tests use m.terminated_states, which will not iterate over the running states. As a result, the tests will not cover all the paths.
- Verify the existence of running states before checking any of their properties. Tests may incorrectly assume that there are running states available and pass if they find none.
- Use FilterFunction to restrict the functions to explore during the symbolic execution of transactions. FilterFunction will constrain input based on function metadata, and can include or avoid functions selected by the specified criteria.
- Keep track of solver timeouts, since they could indicate missing paths to be explored. If the solver times out during a property check, it is not possible to verify that the property is never violated. Manticore defaults to consider solver timeouts UNSAT, and this is configurable via config.py.
- Verify properties using different callers in the required transactions. In Manticore, the caller of an Ethereum transaction is always concrete, so it is essential to verify that properties hold regardless of the caller used.
- Check the length of state.input_symbols. Checking state.input_symbols length will help catch incorrect assumptions on its elements.
The following are all performance optimization tips:
See here: http://manticore.readthedocs.io/en/latest/models.html
For example, printf could be a pretty expensive function to symbolically execute, but doesn't actually affect the program. You can use a manticore hook to effectively patch it out.
@m.hook(first_instruction_of_printf)
def patch_printf(state):
state.cpu.PC = address_of_printf_ret
# state.cpu.RAX = some_return_value (if you also care about the function's return value (maybe strlen?), just set the appropriate register to it!)The state.abandon() API is really useful for making an analysis run faster. If you know that you aren't interested in certain code paths, hook on them, and simply just call state.abandon().
If you want to analyse just one function, it is possible to do so by jumping to it whenever all things are initialised and setting the state values corresponding to the function arguments (e.g. registers).
Manticore supports adding temporary constraints that would otherwise overconstrain the state to aid in solving. For example (from state.solve_buffer)
buffer = self.cpu.read_bytes(addr, nbytes)
result = []
with self.constraints as temp_cs:
for c in buffer:
result.append(self._solver.get_value(temp_cs, c))
temp_cs.add(c == result[-1])
return result
# No constraints are actually added to state.constraints!Similarly, you can use with state as temp_state: ..., but only changes to state.constraints will be local to the with block.
state.mem.write(addr, 'a')
with state as temp_state:
temp_state.mem.write(addr, 'b')
state.mem.read(addr, 1) # ['b']!