Symbolic Execution Under Cryptographic Constraints

Abstract

Symbolic execution is the backbone of automated smart contract vulnerability detection. It encodes program paths as logical formulas and queries SMT solvers for satisfying assignments that trigger bugs. This approach fails when the program under analysis uses cryptographic hash functions. Keccak256, the hash primitive of the Ethereum Virtual Machine, produces 256-bit outputs that resist preimage computation and fall outside the decidable fragments of first-order theories supported by modern SMT solvers. The result is a class of opaque predicates---branch conditions that symbolic execution cannot resolve without concrete information. This paper formalizes the problem, characterizes the decidability boundary, and surveys practical strategies: concolic execution, under-approximation, lazy constraint resolution, and abstract memory models for hash-indexed storage. We give particular attention to the EVM storage mapping problem, where Solidity compiles mapping(K => V) into keccak256-indexed storage slots, creating a pervasive hash dependency throughout contract state.

1. Introduction

Symbolic execution treats program inputs as symbolic variables and computes constraints along each execution path. When a branch condition depends on symbolic input, the engine queries an SMT solver to determine feasibility of both branches. Infeasible paths are pruned; feasible ones yield concrete test inputs. Tools like KLEE [1], Mythril [2], and Manticore [3] have applied this technique to find real vulnerabilities in systems code and smart contracts.

The technique has an Achilles heel. When a program computes y = keccak256(x) and later branches on y, the symbolic executor must reason about the relationship between x and y. But keccak256 is a cryptographic hash function. Its security rests on preimage resistance: given y, finding any x such that keccak256(x) = y is computationally infeasible. An SMT solver asked to find such an x will either time out or return unknown. The branch becomes opaque.

This is not a tooling limitation. It is a consequence of the mathematical properties of cryptographic hash functions interacting with the expressiveness limits of decidable logical theories. Understanding exactly where and why the breakdown occurs is necessary for designing sound workarounds.

2. Background

2.1 Symbolic Execution

A symbolic executor maintains a symbolic state (pc, sigma, Pi) consisting of a program counter pc, a symbolic store sigma mapping variables to symbolic expressions, and a path constraint Pi---a conjunction of boolean formulas accumulated from branch conditions. At each conditional branch if (e), the executor forks:

• True branch: add e to Pi, continue if Pi /\ e is satisfiable
• False branch: add not e to Pi, continue if Pi /\ (not e) is satisfiable

Satisfiability is checked by an SMT solver operating over a background theory---typically quantifier-free bitvectors (QF_BV) for fixed-width machine integers, extended with arrays (QF_ABV) for memory modeling.

2.2 SMT Solving and Decidable Theories

SMT solvers decide satisfiability modulo theories. The key theories for program analysis are:

Theory	Fragment	Decidable	Complexity
QF_BV	Quantifier-free bitvectors	Yes	NEXPTIME-complete [4]
QF_ABV	QF_BV + arrays	Yes	NEXPTIME-complete
QF_NIA	Quantifier-free nonlinear integer arithmetic	Undecidable in general	---
QF_BV + uninterpreted functions	Bitvectors with UFs	Yes	NEXPTIME-complete

Decidability means there exists a procedure that terminates with SAT or UNSAT for every formula in the theory. All standard EVM operations---ADD, MUL, DIV, AND, OR, SHL, comparisons, memory loads and stores---fall within QF_ABV and are decidable.

2.3 EVM Storage Model

The EVM provides a persistent key-value store mapping 256-bit keys to 256-bit values. Solidity compiles high-level storage variables to this flat address space using deterministic slot assignment. Simple variables occupy sequential slots. Mappings use a hash-based scheme:

storage_address(mapping[key]) = keccak256(key . slot)

where . denotes concatenation and slot is the mapping’s base storage slot [5]. Nested mappings compose:

storage_address(m[k1][k2]) = keccak256(k2 . keccak256(k1 . slot))

Dynamic arrays use keccak256(slot) as the base address, with element i at keccak256(slot) + i.

This design means that every read or write to a Solidity mapping passes through keccak256. Symbolic analysis of contract state is inseparable from the hash function problem.

3. The Opaque Predicate Problem

3.1 Formal Definition

An opaque predicate is a branch condition whose outcome is determined by the program’s semantics but cannot be resolved by the analysis [6]. In the context of symbolic execution with hash functions, we define:

Definition 1. A hash-induced opaque predicate is a path constraint of the form keccak256(E) = C where E is a symbolic expression and C is a concrete 256-bit constant, or equivalently, any constraint requiring reasoning about the preimage or image of a cryptographic hash.

Consider a contract that checks:

function withdraw(bytes32 secret) external {
    require(keccak256(abi.encodePacked(secret)) == storedHash);
    // transfer funds
}

The path constraint for the transfer branch is:

Pi /\ (keccak256(secret) = storedHash)

Resolving this constraint requires finding a preimage of storedHash under keccak256---precisely what preimage resistance guarantees is hard.

3.2 Why Backward Reasoning Fails

Symbolic execution reasons backward through constraints: given a target condition, find inputs that satisfy it. For arithmetic operations, SMT solvers invert efficiently. Given x + 5 = 10, the solver yields x = 5. Given x * 3 = 12, the solver yields x = 4.

Keccak256 is a one-way function by design. Its internal structure---24 rounds of permutation over a 1600-bit state using the Keccak-f[1600] sponge construction [7]---is expressible as a boolean circuit, but encoding it in QF_BV produces a formula with tens of thousands of variables and clauses. The solver can technically attempt to find a satisfying assignment, but the search space is 2^256 and the propagation structure of the hash provides no useful unit propagation or conflict-driven learning opportunities. In practice, every major SMT solver (Z3, CVC5, Boolector) either times out or returns unknown.

flowchart LR
    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0
    classDef success fill:#1a331a,stroke:#a8c686,stroke-width:2px,color:#c8e8b0

    A["Symbolic input x"]:::process
    B["keccak256(x)"]:::attack
    C["Branch condition: hash = C"]:::attack
    D["SMT query: find x such that keccak256(x) = C"]:::attack
    E["Solver: TIMEOUT / UNKNOWN"]:::attack

    F["Arithmetic: x + 5 = 10"]:::process
    G["SMT query: find x"]:::process
    H["Solver: x = 5"]:::success

    A --> B --> C --> D --> E
    F --> G --> H

3.3 Forward Reasoning Also Fails (at Scale)

One might ask: can the solver reason forward---given a symbolic x, compute keccak256(x) symbolically and check whether the result matches C? The answer is theoretically yes but practically no. Encoding keccak256 as a QF_BV circuit yields a formula with approximately 150,000 boolean variables [8]. The solver must find an assignment to all of them that is consistent with both the hash circuit and the path constraint. The hash’s diffusion property ensures that small changes in input produce uncorrelated changes in output, destroying the locality that SAT/SMT solvers exploit.

4. Decidability Analysis

4.1 Hash Functions and Theory Boundaries

The decidable theories used by SMT solvers---QF_BV, QF_ABV, QF_LIA---have known expressiveness boundaries. We can characterize where keccak256 falls.

Proposition 1. Keccak256, fully encoded as a bitvector circuit, lies within QF_BV. However, satisfiability queries involving keccak256 constraints, while decidable in theory, have worst-case complexity that renders them practically intractable.

The proof is straightforward: keccak256 is a deterministic function on fixed-width bitvectors, so its input-output relation can be expressed as a QF_BV formula. Decidability follows from QF_BV decidability. But the formula size (O(10^5) variables per hash invocation) and the absence of exploitable structure in the hash’s boolean circuit place these instances among the hardest in the QF_BV decision problem.

Proposition 2. Treating keccak256 as an uninterpreted function restores tractability at the cost of soundness for collision-sensitive properties.

If keccak256 is modeled as an uninterpreted function f, the solver enforces functional consistency (x = y => f(x) = f(y)) but nothing else. This is decidable and fast. The approximation is sound for many analyses: if two storage reads use different keys, the solver correctly infers they access different slots. But it cannot reason about specific hash values, and it incorrectly permits f(x) != f(y) when x != y---it cannot enforce injectivity (collision resistance).

4.2 The Undecidability of Hash Preimage Constraints in Practice

While QF_BV with encoded keccak256 is decidable, the practical situation is closer to undecidability from the perspective of bounded-time analysis. We can make this precise:

Theorem 1. For any fixed timeout T, there exist keccak256 preimage constraints that no SMT solver can resolve within time T, assuming keccak256 is preimage resistant.

This follows directly from the preimage resistance assumption. If a solver could efficiently find preimages within a fixed time bound for arbitrary targets, it would constitute a break of the hash function’s security. Since no such break is known for Keccak, we treat preimage constraints as practically undecidable.

5. Concolic Execution

Concolic (concrete-symbolic) execution is the primary practical response to the hash function problem [9]. The idea: execute the program with concrete inputs while simultaneously maintaining symbolic state. When a hash function is encountered, compute the hash concretely and record the mapping.

5.1 Algorithm

Algorithm: CONCOLIC_WITH_HASH_RESOLUTION
Input: Program P, initial concrete input I_0
Output: Set of explored paths with vulnerability reports

1.  worklist <- {I_0}
2.  explored <- {}
3.  hash_map <- {}          // concrete hash cache: input -> output
4.  while worklist is not empty:
5.      I <- worklist.pop()
6.      (path, sigma, Pi) <- execute_concretely_and_symbolically(P, I)
7.      for each hash invocation keccak256(e) encountered during execution:
8.          v_concrete <- evaluate(e, I)       // concrete input value
9.          h_concrete <- keccak256(v_concrete) // concrete hash output
10.         hash_map[v_concrete] <- h_concrete
11.         add constraint (e = v_concrete => keccak256(e) = h_concrete) to Pi
12.     explored <- explored + {path}
13.     check_vulnerabilities(sigma, Pi)
14.     for each branch b in path:
15.         Pi_neg <- negate_branch(Pi, b)
16.         // Replace hash constraints with known concrete mappings
17.         Pi_resolved <- substitute_known_hashes(Pi_neg, hash_map)
18.         if SMT_solve(Pi_resolved) = SAT with model M:
19.             I_new <- extract_input(M)
20.             if path_of(I_new) not in explored:
21.                 worklist.add(I_new)
22.     return explored

5.2 Soundness and Completeness

Concolic execution with concrete hash resolution is sound: every reported vulnerability corresponds to a real execution. But it is incomplete: it can only explore paths reachable from concrete hash values it has observed. If a vulnerability is guarded by require(keccak256(x) == C) and no concrete input in the worklist produces a hash matching C, that path is never explored.

flowchart TD
    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef data fill:#332a1a,stroke:#d4b870,stroke-width:2px,color:#f0e0c0
    classDef highlight fill:#332519,stroke:#e8a87c,stroke-width:2px,color:#f0d8c0
    classDef success fill:#1a331a,stroke:#a8c686,stroke-width:2px,color:#c8e8b0

    A["Concrete input I"]:::data
    B["Execute P with I"]:::process
    C["Record hash pairs: input -> output"]:::data
    D["Collect path constraint Pi"]:::process
    E["Negate branch, substitute known hashes"]:::process
    F["SMT solve simplified constraint"]:::process
    G{"SAT?"}:::highlight
    H["New concrete input"]:::success
    I["Add to worklist"]:::process
    J["Path unexplorable"]:::highlight

    A --> B --> C --> D --> E --> F --> G
    G -->|"Yes"| H --> I
    G -->|"No / Unknown"| J

The coverage depends on the quality of seed inputs. Fuzzing-generated seeds, transaction histories from mainnet, and manually crafted inputs for known entry points all improve the concolic engine’s reach.

6. The Storage Mapping Problem

6.1 The Pervasiveness of Hash-Indexed Storage

Consider a token contract with a balance mapping:

mapping(address => uint256) public balances;

function transfer(address to, uint256 amount) external {
    require(balances[msg.sender] >= amount);
    balances[msg.sender] -= amount;
    balances[to] += amount;
}

The compiled EVM bytecode accesses storage at:

slot_sender = keccak256(msg.sender . 0)
slot_to     = keccak256(to . 0)

A symbolic executor analyzing transfer with symbolic msg.sender and to must reason about SLOAD(keccak256(msg.sender . 0)) and SSTORE(keccak256(to . 0), ...). The hash converts a simple arithmetic problem (can amount exceed the balance?) into one entangled with keccak256.

6.2 Symbolic Memory Models

Three approaches handle hash-indexed storage in symbolic analysis:

Flat uninterpreted function model. Treat keccak256 as an uninterpreted function H. Storage becomes an array indexed by H(key . slot). The solver enforces key1 = key2 => H(key1 . slot) = H(key2 . slot) but cannot compute concrete slot addresses. This model is fast and sufficient for detecting arithmetic bugs within a single mapping, but it cannot reason about cross-mapping interactions or specific slot values.

Concrete-backed model. Maintain a concrete key-value store populated from on-chain state. When symbolic execution encounters SLOAD(keccak256(E)), check if E can be concretized. If so, look up the concrete slot. If not, fork: one branch assumes the slot contains a known value, the other treats it as unconstrained. This is the approach used by tools like Mythril [2] when connected to an archive node.

Layered model. Combine an uninterpreted function layer (for symbolic reasoning) with a concrete cache (for known values). The symbolic layer handles relational queries (“are these two storage accesses to the same slot?”) while the concrete layer resolves specific values.

flowchart TD
    classDef system fill:#1a3333,stroke:#5ba8a8,stroke-width:2px,color:#c0e8e8
    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef data fill:#332a1a,stroke:#d4b870,stroke-width:2px,color:#f0e0c0

    subgraph layered ["Layered Memory Model"]
        A["SLOAD(keccak256(E))"]:::process
        B{"E concretizable?"}:::process
        C["Concrete cache lookup"]:::data
        D["Uninterpreted function H(E)"]:::system
        E["Return concrete value"]:::data
        F["Return symbolic H(E) with UF constraints"]:::system

        A --> B
        B -->|"Yes"| C --> E
        B -->|"No"| D --> F
    end

6.3 Hash Collision as a Vulnerability

Two distinct mapping keys can theoretically hash to the same storage slot. For keccak256, no collision is known, and the probability is approximately 2^{-256} per pair, making it negligible under standard assumptions. But the structure of Solidity’s slot computation introduces a subtlety.

For a mapping at slot s, the storage address is keccak256(key . s). For a mapping at slot s', it is keccak256(key' . s'). A collision occurs when:

keccak256(key . s) = keccak256(key' . s')

where key . s != key' . s'. While cryptographically negligible, some analyses need to prove non-collision for soundness. The uninterpreted function model does not guarantee this---it allows H(a) = H(b) when a != b. A sound analysis must either assume collision resistance as an axiom or add explicit non-collision constraints for each pair of accessed slots.

In practice, the risk comes not from keccak256 collisions but from implementation bugs in slot calculation---incorrect slot numbers, missing padding, or hash composition errors that produce overlapping storage. These are detectable by static analysis of the slot computation logic without needing to reason about the hash itself.

7. Practical Strategies

7.1 Lazy Constraint Resolution

Rather than attempting to solve hash constraints immediately, defer them. When encountering keccak256(E), introduce a fresh symbolic variable h with the constraint h = keccak256(E) held in a deferred set. Continue execution using h in place of the hash output. If a branch later requires a specific value of h, check:

1. Can E be concretized from the current path constraint? If so, compute keccak256(E) concretely and substitute.
2. Does the constraint system already determine h through other means (e.g., h was loaded from storage and its concrete value is known)? If so, substitute.
3. Otherwise, the branch is hash-opaque. Report it as a coverage gap and continue along the concretely observed branch.

This strategy avoids solver timeouts on hash constraints while preserving soundness for the paths it does explore.

7.2 Under-Approximation

Accept that full path coverage is impossible and instead check whether vulnerabilities exist under specific assumptions about hash values. For each mapping access pattern, assume:

• msg.sender is a fixed address A (e.g., the attacker)
• to is a fixed address B (e.g., the victim)
• Compute concrete storage slots from these assumptions
• Run fully symbolic analysis on the arithmetic within those slots

This reduces the problem to standard QF_BV reasoning. The trade-off: vulnerabilities that depend on specific address relationships (e.g., msg.sender = address(this)) may be missed unless those specific values are in the assumption set.

7.3 Summary Functions for Known Patterns

Many contracts follow recognizable patterns: ERC-20 balance mappings, ERC-721 ownership mappings, access control role mappings. For these, the slot computation is structurally predictable. A symbolic executor can recognize the pattern and substitute a summary function that captures the mapping’s semantics without reasoning through the hash:

Summary: ERC20_BALANCE(addr, slot) -> symbolic_value
Semantics: independent symbolic value per (addr, slot) pair
Constraint: ERC20_BALANCE(a, s) >= 0 (uint256 range)

This bypasses keccak256 entirely for recognized patterns, treating the mapping as an abstract data type rather than a concrete storage computation.

7.4 Constraint Partitioning

When a path constraint contains both hash-dependent and hash-independent sub-formulas, partition them:

Pi = Pi_arith /\ Pi_hash

Solve Pi_arith independently. If it is unsatisfiable, the path is infeasible regardless of hash values. If it is satisfiable, the remaining question is whether Pi_hash can also be satisfied---which may require concolic resolution or under-approximation.

This partitioning avoids contaminating tractable arithmetic queries with intractable hash constraints, improving solver performance on the portions of the path constraint that are decidable.

8. Related Work

KLEE [1] pioneered practical symbolic execution for systems code, demonstrating the power and limits of SMT-based path exploration. It handles library calls through concrete execution fallbacks---a precursor to the concolic hash resolution strategy.

Mythril [2] applies symbolic execution specifically to EVM bytecode, using Z3 as its backend solver. Its handling of keccak256 relies on a combination of concrete execution and uninterpreted function modeling, with known limitations on hash-dependent paths.

Manticore [3] from Trail of Bits supports both EVM and native binary symbolic execution. It treats keccak256 as an uninterpreted function with functional consistency constraints, accepting the under-approximation this implies.

The KLEE-based approach to handling external functions through concretization was formalized by Cadar et al. [1] and extended to cryptographic operations by subsequent work on concolic testing.

Luu et al. [10] identified symbolic execution limitations in their work on Oyente, one of the earliest EVM analysis tools, noting that “the symbolic execution engine cannot reason about cryptographic operations” and proposing path-specific concretization.

The EVM storage layout specification is defined in the Solidity documentation [5], and the keccak256 sponge construction is standardized in FIPS 202 [7].

References

[1] C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,” OSDI 2008. https://www.usenix.org/conference/osdi-08/klee-unassisted-and-automatic-generation-high-coverage-tests-complex-systems

[2] B. Mueller, “Mythril: Security Analysis Tool for EVM Bytecode,” https://github.com/Consensys/mythril

[3] Trail of Bits, “Manticore: Symbolic Execution Tool,” https://github.com/trailofbits/manticore

[4] R. Brummayer and A. Biere, “Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays,” TACAS 2009. https://doi.org/10.1007/978-3-642-00768-2_16

[5] Solidity Documentation, “Layout of State Variables in Storage,” https://docs.soliditylang.org/en/latest/internals/layout_in_storage.html

[6] C. Collberg, C. Thomborson, and D. Low, “A Taxonomy of Obfuscating Transformations,” Technical Report 148, Department of Computer Science, University of Auckland, 1997. https://researchspace.auckland.ac.nz/handle/2292/3491

[7] NIST, “SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions,” FIPS PUB 202, 2015. https://doi.org/10.6028/NIST.FIPS.202

[8] L. De Moura and N. Bjorner, “Z3: An Efficient SMT Solver,” TACAS 2008. https://doi.org/10.1007/978-3-540-78800-3_24

[9] K. Sen, D. Marinov, and G. Agha, “CUTE: A Concolic Unit Testing Engine for C,” ESEC/FSE 2005. https://doi.org/10.1145/1081706.1081750

[10] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making Smart Contracts Smarter,” CCS 2016. https://doi.org/10.1145/2976749.2978309