Using Symbolic Execution for Vulnerability Discovery

Detailed Instructions

Begin by isolating the specific smart contract function or protocol interaction to analyze. Define the symbolic variables that will represent unknown user inputs, such as msg.sender, msg.value, or array indices. Set initial constraints to bound the search space; for example, limit an ERC-20 amount to be less than type(uint256).max to avoid trivial overflow paths. Configure the symbolic engine's solver timeout and loop unrolling depth based on contract complexity. This step creates the formal model that the execution engine will explore.

• Sub-step 1: Identify the target function signature and its state dependencies.
• Sub-step 2: Declare symbolic variables for all external inputs and storage slots.
• Sub-step 3: Apply realistic constraints (e.g., balance >= amount) to prune impossible paths.

solidityCopy
// Symbolic variable declaration example for a transfer function
symbolic address sender;
constrain(sender != address(0));
symbolic uint256 amount;
constrain(amount > 0 && amount < totalSupply);

Tip: Model the contract's storage as a symbolic map to capture state changes across transactions.

Detailed Instructions

Initiate the symbolic execution, which treats the defined variables as unconstrained symbols rather than concrete values. The engine explores the control flow graph, forking a new symbolic state at every conditional branch (e.g., if, require). For each path, it records the path constraints—a set of logical formulas that must be true for execution to reach that point. For instance, a path requiring balanceOf[user] >= amount adds that constraint to its set. Monitor for path explosion; tools like Manticore or Mythril use strategies like state merging to manage this. The output is a set of symbolic states, each with its own constraints and a record of storage/world effects.

• Sub-step 1: Run the engine with the configured model and monitor for timeout.
• Sub-step 2: Log each unique path identifier and its terminal state (e.g., REVERT, STOP, SELFDESTRUCT).
• Sub-step 3: Extract the final path constraints and memory/state snapshots for analysis.

bashCopy
# Example command to run Manticore symbolically
manticore ./contract.sol --contract TargetContract --txlimit 1000

Tip: Prioritize analyzing paths that end in a SELFDESTRUCT opcode or an unconstrained external call first, as they often indicate critical flaws.

Detailed Instructions

For each collected symbolic state, formulate solver queries to check for property violations. This involves asking the Satisfiability Modulo Theories (SMT) solver (like Z3) if a set of constraints can be satisfied. To find a reentrancy bug, query for a state where an external call is made (e.g., call.value()) and the contract's storage is subsequently written without adhering to the checks-effects-interactions pattern. The solver either returns UNSAT (no violation possible) or SAT with a concrete counterexample—a set of exact input values that trigger the bug. For arithmetic issues, query for conditions like balanceAfter > balanceBefore without a corresponding mint.

• Sub-step 1: For a suspicious path, add the negation of a safety property (e.g., balance == oldBalance) to its constraints.
• Sub-step 2: Submit the combined constraint set to the solver.
• Sub-step 3: If SAT, decode the solver's model into a test case with specific calldata and block.number.

pythonCopy
# Pseudocode for a solver query to find an overflow
constraints = [symbolic_a + symbolic_b > MAX_UINT256]
if solver.satisfiable(constraints):
    model = solver.get_model()
    print(f"Overflow input: a={model[symbolic_a]}, b={model[symbolic_b]}")

Tip: Use the solver to generate minimal counterexamples, which are easier to understand and verify.

Detailed Instructions

Symbolic execution outputs require manual verification to eliminate false positives and assess impact. First, replay the generated concrete counterexample in a local fork (using Foundry or Hardhat) to confirm the vulnerability triggers. Check if the path is feasible under the real blockchain context—e.g., a path requiring block.timestamp == 12345 may be theoretically possible but impractical. Classify findings by severity (Critical, High, Medium) based on access controls, asset value at risk, and likelihood. Document the exact preconditions, attack sequence, and recommended fix. This step transforms a solver output into a actionable audit report item.

• Sub-step 1: Replicate the bug using the concrete inputs in a forked test environment.
• Sub-step 2: Evaluate the attack's preconditions (e.g., attacker token balance, governance role).
• Sub-step 3: Write a proof-of-concept exploit and a patched code snippet for the report.

solidityCopy
// Example of a verified finding: Insufficient access control
// Symbolic execution found a path where `msg.sender != owner` could call `selfdestruct`.
// Verified POC:
function test_UnauthorizedSelfdestruct() public {
    address attacker = makeAddr("attacker");
    vm.prank(attacker);
    vulnerableContract.emergencyShutdown(); // Should revert but doesn't
}

Tip: Correlate symbolic findings with static analysis warnings (e.g., Slither) to increase confidence in true positives.

Detailed Instructions

Translate the vulnerability into a formal security property that the fixed code must uphold. For a reentrancy fix, this property states that no external call can be made while the contract's state is inconsistent. In symbolic execution, this is expressed as a logical constraint or assertion. For a patched ERC-20 function, the property might be that the total supply is invariant during a token transfer. Define this property as a require or assert statement in a test harness or directly within the instrumented contract code. The symbolic execution engine will attempt to find any program path that violates this assertion, proving the mitigation is incomplete.

Tip: Start with the negation of the original exploit condition. If the bug allowed an overflow, assert that the relevant arithmetic operation never exceeds type(uint256).max.

Detailed Instructions

Integrate the security property from Step 1 into the contract's control flow. This often involves creating a dedicated test harness contract that calls the patched functions with symbolic arguments. For example, to verify a fixed access control modifier, the harness would call the protected function with a symbolic address for msg.sender. Use the Manticore or Mythril API to mark specific inputs (like address caller) as symbolic. Ensure the execution environment (e.g., symbolic block.number or msg.value) models relevant blockchain context. The goal is to create a program where the engine can explore all possible states resulting from the symbolic inputs, checking for property violations.

pythonCopy
# Example Manticore harness setup snippet
from manticore.ethereum import ManticoreEVM
m = ManticoreEVM()
contract_account = m.create_contract(open('PatchedToken.sol').read())
symbolic_sender = m.make_symbolic_value()
m.constrain(symbolic_sender != 0) # Constrain to valid address
# Call transfer with symbolic sender and value
tx = m.transaction(caller=symbolic_sender, address=contract_account, data=\"transfer(...)\")

Tip: Constrain symbolic values to realistic ranges (e.g., uint256 bounds) to avoid irrelevant exploration paths.

Detailed Instructions

Initiate the symbolic execution run. The engine will systematically explore the state space defined by the symbolic inputs and the contract's logic. Monitor the output for any test case or counterexample that satisfies the violation condition. A tool like Mythril will report "SATISFIABLE" if it finds a path that reaches an assertion failure or an unsafe operation. For the mitigation verification, a successful run should find zero violating paths. If a path is found, the engine will provide concrete values for the symbolic inputs (e.g., msg.sender = 0xbadc0de...) that trigger the violation. This concrete test case is crucial for debugging the incomplete fix.

• Sub-step 1: Run the analysis with a sufficient timeout or gas limit to ensure coverage.
• Sub-step 2: Parse the engine's logs for warnings or property violations.
• Sub-step 3: Extract the concrete variable assignments from any generated counterexample.

Tip: Use the --verbose flag or similar to get detailed path exploration logs, helping you understand which branches were taken.

Detailed Instructions

If the symbolic executor finds a violating path, analyze the provided counterexample. This is a set of concrete inputs and transaction sequences that bypass your mitigation. Map these inputs back to the source code to understand the new attack vector. The issue often lies in a missed edge case, such as a different state variable being manipulated or a nested call path. Update the mitigation—this may involve adding additional checks, modifying state update ordering, or employing a different defensive pattern like Checks-Effects-Interactions. After updating the code, return to Step 1 and repeat the verification process. Iteration continues until the symbolic analysis proves the property holds for all possible paths, resulting in a mathematically verified fix.

solidityCopy
// Example: Initial flawed mitigation missing an edge case
function withdraw() public {
    require(balances[msg.sender] > 0, "No balance"); // Check
    (bool success, ) = msg.sender.call{value: balances[msg.sender]}(""); // Interaction
    balances[msg.sender] = 0; // Effect - STILL VULNERABLE to reentrancy
}
// The symbolic engine would find a path where reentrancy resets balance before deduction.

Tip: Consider formal verification tools like Certora or SMTChecker for continuous property verification after each code change.