Smart Contract Invariants Protect Against Cybercriminals

This paper investigates whether smart contract invariants can protect against real-world cybercriminal attacks on blockchain systems, and whether automated tools can discover such attack-stopping invariants. The authors note that Blockchains are among the most adversarial environments in computing. Billions are stolen by cybercriminals who exploit vulnerabilities, and that no concept or technique has proven to really make a difference prior to this work.

The paper addresses four research questions:

• RQ1: To what extent do program invariants stop real world attacks on smart contracts?

• RQ2: To what extent do attack-stopping invariants break existing behavior according to historical replay verification?

• RQ3: What are the limitations of historical replay verification?

• RQ4: To what extent are the state-of-the-art invariant generation tools able to generate attack-stopping invariants for real world attacks?

The authors built INVARIANTEVAL, a benchmark of 28 real-world Ethereum exploits, each paired with a human-authored program invariant that blocks the attack. Each entry contains a triple of 1) a documented exploit transaction 2) a source code proof-of-concept that reproduces the attack path 3) a human-authored invariant. The dataset was constructed from the DeFiHackLabs repository, restricted to Ethereum exploits spanning July 2017 to June 2026. For each attacked contract, two authors independently write a program invariant, time-boxed to eight hours per case, with a third author resolving disagreements.

They also built PONDEREPLAY, a replay framework that re-executes transactions in order to prove the correctness and soundness of smart contract invariants. This framework replays transactions against three versions: the original on-chain trace (O), a recompiled unmodified contract (R), and a hardened contract with the invariant installed (H). The verification checks three fidelity criteria: transaction status fidelity, subcall fidelity, and storage fidelity.

All 28 ground-truth invariants blocked both the proof-of-concept exploits and the actual malicious on-chain transactions, achieving a perfect result 28/28 (100%). The authors note There are 25 attacks for which we did not succeed in writing the securing invariant. This is because of our limited expertise of the target protocol and the time-bound budget.

The invariants were classified into eight families: "Price oracle and slippage are the largest family, with 8/28 cases. Ledger, supply, and conservation checks follow with 6 cases. Access control and authorization account for 4 cases, tied with external call and interaction safety, three of which are reentrancy locks. Business logic guards and arithmetic safety cover 2 cases each; input validation and initialization checks cover 1 case each."

The authors replayed 108,637 historical transactions through the hardened contracts. Of these, 106,815 (98.3% of total replayed) transactions pass the preservation check, indicating equivalent behaviour between the recompiled and hardened contracts. However, 1,526 txs (1.4% of total replayed) showed divergence.

Manual analysis of the divergences identified five behavioral change reasons:

• Past Exploit: Transactions reproducing the same vulnerability pattern as documented attacks (e.g., APEMAGA)

• Misusage: Calls that the protocol design never envisioned or authorized, while not being malicious (e.g., Nimbus)

• Whitehat operation: Transactions technically equivalent to exploits but performed by whitehat hackers recovering funds (e.g., Anyswap)

• Over-restrictive invariant: The invariant expresses the right security property but its predicate is narrower than the protocol's actual intended interface (e.g., Yearn yDAI, where a keeper bot's legitimate earn calls were blocked)

• Tight numerical envelope: invariants whose guard is a numeric bound—a price band, a swap tax, a deviation threshold set too tightly for legitimate traffic (e.g., Inverse Finance)

296 transactions were inconclusive, with three mechanical causes identified:

• Original OOG (173 cases): a transaction that ran out of gas on-chain succeeds in the recompiled replay R because PONDEREPLAY does not cap the replay exactly at the original gas limit

• Subcall OOG (12 cases): an internal subcall exhausts gas and reverts differently in the two executions while the top-level outcome matches

• Accumulated drift (111 cases): state drift introduced by co-located transactions in the same block that behave differently under recompiled bytecode

Importantly, for 291 of the 296 inconclusive transactions (98%), the hardened trace H still matches the recompiled contract outcome R, confirming that inconclusiveness stems from the replay infrastructure, not from the invariant.

Three state-of-the-art tools were evaluated: InvCon, InvCon+, and FLAMES. The results show that only 2 of the 28 ground-truth invariants can be synthesized, both by FLAMES. These two cases correspond to APEMAGA and Inverse Finance. While All three tools produce candidates for many contracts (resp. 13, 24, and 28), but the candidates hardly capture the security-critical property that can block the exploit.

The paper details the BEC attack (April 2018, 900M loss) as a representative example. The batchTransfer function pays multiple recipients the same amount in one call by computing amount = cnt * value but the multiplication had no safety check. The attacker sent the transaction with 2 receivers and a value of 2 255. Multiplying those together (2×2 255) caused an overflow, so the balance check passed even though they had no tokens. The inserted invariant require(value <= uint256(-1) / cnt) catches this overflow scenario.

The authors conclude: "Every invariant blocked its target attack; 98.3% of replayed historical transactions were preserved, and every deviation was traced causally to the invariant rather than to replay noise. Against this ground truth, state-of-the-art generation tools fell short: FLAMES recovered the correct guard in only 2 of 28 cases. A single correctly placed invariant is sufficient to stop a real exploit; finding that invariant automatically remains an open problem."

Improvement 1: Attack-Stopping Invariant Synthesis via Causal Exploit Tracing

• What to improve: Current invariant generators (InvCon, FLAMES) produce generic candidates that miss security-critical properties.

• How: Train an AI system to analyze exploit transactions (as in INVARIANTEVAL) and trace the exact state-transition path that enables the attack (e.g., arithmetic overflow in BEC). The AI should generate invariants that directly negate the causal condition (e.g., require(value <= uint256(-1) / cnt)) rather than broad behavioral summaries.

• What the improved system can do: Automatically produce minimal, exploit-blocking invariants for new vulnerabilities by simulating attack paths and identifying the precise predicate that breaks the exploit’s precondition, reducing reliance on human experts.

Improvement 2: Behavioral Preservation-Aware Invariant Ranking

• What to improve: Invariants that block attacks may also break legitimate transactions (1.4% divergence in RQ2). Current tools don’t optimize for this trade-off.

• How: Integrate a replay-based preservation checker (like PONDEREPLAY) into the generation loop. The AI should score candidate invariants not only by attack-blocking capability but also by historical transaction preservation rate, penalizing over-restrictive predicates (e.g., tight numerical envelopes in Inverse Finance).

• What the improved system can do: Generate invariants that maximize security while minimizing false positives, automatically rejecting those that block whitehat operations or legitimate keeper calls, and suggesting relaxed bounds when needed.

Improvement 3: Automated Invariant Classification and Family-Aware Generation

• What to improve: The paper identifies 8 invariant families (e.g., price oracle, access control, reentrancy locks). Current tools treat all invariants uniformly.

• How: Train a classifier on the 28 ground-truth invariants to detect the vulnerability type from the exploit transaction (e.g., flash loan price manipulation vs. missing access control). Then use family-specific templates or search strategies (e.g., for oracle invariants, focus on price deviation checks; for reentrancy, focus on mutex flags).

• What the improved system can do: Rapidly narrow the invariant search space based on the attack’s family, improving synthesis success rates beyond the current 2/28, and enabling targeted generation for unseen but similar exploits.

Improvement 4: Replay Infrastructure-Aware Invariant Validation

• What to improve: PONDEREPLAY’s inconclusive results (296 txs) stem from gas limits, subcall reverts, and state drift—not invariants. AI systems should account for these artifacts.

• How: Build an AI validator that distinguishes invariant-induced divergences from replay noise by comparing hardened vs. recompiled traces at the subcall level and using statistical models to flag drift. The system should automatically discard inconclusive transactions or adjust replay parameters (e.g., exact gas capping) to reduce false negatives.

• What the improved system can do: Provide higher-confidence invariant validation, avoiding false alarms from replay infrastructure, and enabling reliable deployment decisions for hardened contracts.

Improvement 5: Historical Replay-Based Invariant Refinement

• What to improve: The paper shows 1,526 divergences with 5 distinct causes (e.g., misusage, whitehat ops). AI can learn from these to refine invariants post-generation.

• How: Implement a feedback loop where the AI replays historical transactions against a candidate invariant, clusters divergences by cause (using the paper’s taxonomy), and automatically adjusts the invariant—e.g., widening a numerical bound, adding an exception for whitehat addresses, or splitting the invariant into multiple conditional checks.

• What the improved system can do: Iteratively improve invariants over time, turning over-restrictive or under-restrictive predicates into precise, production-ready guards that preserve all legitimate historical behavior while still blocking the exploit.

Improvement 6: Cross-Protocol Invariant Transfer Learning

• What to improve: The 28 cases span diverse protocols (DeFi, tokens, exchanges). Current tools generate from scratch per contract.

• How: Pre-train an AI model on the INVARIANTEVAL dataset to learn invariant patterns that generalize across protocols (e.g., conservation checks for token transfers, slippage guards for DEXs). Use few-shot learning to adapt these patterns to new contracts with minimal examples.

• What the improved system can do: Quickly propose candidate invariants for new smart contracts by transferring knowledge from known attack families, drastically reducing the time from exploit discovery to hardened deployment.

Blockchains are among the most adversarial environments in computing. Billions are stolen by cybercriminals who exploit vulnerabilities. This is an open problem and no concept or technique has proven to really make a difference. In this paper, we claim that the classical notion of program invariant is perhaps the most powerful solution to the problem. We devise anoriginal experimental protocol to 1) study how invariants would have protected against past real-world attacks and 2) whether state-of-the-art automated tools can find them. The experimental toolchain is sophisticated. It is based on INVARIANTEVAL, a benchmark of 28 real Ethereum exploits, each paired with a human-authored invariant that blocks the attack. We validate every invariant with PONDEREPLAY, a replay framework that re-executes transactions in order to prove the correctness and soundness of smart contract invariants. We demonstrate that smart contract invariants block all the cybercriminal attacks in INVARIANTEVAL, fully validated by replaying 108,637 historical transactions. Our large-scale experiments clearly demonstrate that smart contract invariants protect against cybercriminals.