Source-linked AI summary
solc-verify: A Modular Verifier for Solidity Smart Contracts
Ákos Hajdu, Dejan Jovanović
TL;DR
Smart-contract bugs can have devastating financial effects, while verification approaches face limits in scalability, precision, expressiveness, and ease of use. solc-verify uses annotations and modular SMT-based analysis to verify Solidity contracts, and the authors report finding bugs and proving non-trivial properties on real-world examples.
Problem
Smart-contract bugs can cause devastating financial losses, while existing verification approaches have limits in scalability, precision, expressiveness, or ease of use.
Source: §1 · p. 2Method
solc-verify translates annotated Solidity contracts into Boogie and discharges verification conditions with SMT solvers using modular program analysis.
Source: §1 · p. 2Results
solc-verify finds bugs and proves correctness of non-trivial properties on real-world contracts with minimal user effort.
Source: §7 · p. 16Takeaways & Limitations
Developers can specify high-level contract properties, including invariants and function pre- and postconditions, as in-code annotations.
Source: §1 · p. 2solc-verify does not support low-level callcode and delegatecall, which would require encoding EVM details.
Source: §4 · p. 9
Abstract
from arXiv · showhide
We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.
1 Introduction
Smart contracts let mutually distrusting parties execute coded terms on public blockchains, but bugs can cause severe financial losses. solc-verify applies modular verification to Solidity contracts using developer-written specifications and SMT solvers.
1 Introduction
- Smart contracts extend blockchains from digital money to programs that execute contractual terms among mutually distrusting parties.Public blockchains let parties transact without a central authority.Source: §1 · p. 1
- Contract bugs can cause devastating financial losses, and deployed code is immutable without complex upgrade solutions involving a central authority.The DAO bug enabled an attacker to steal $60M despite scrutiny of a relatively small contract.Source: §1 · p. 2
- solc-verify translates annotated Solidity contracts into Boogie and uses SMT solvers to verify properties such as invariants and function pre- and postconditions.The tool addresses Solidity-specific modeling challenges, including 256-bit arithmetic and properties such as equality between summed balances and total supply.Source: §1 · p. 2
2 Background
Ethereum contracts are written in Solidity, compiled to EVM bytecode, and run through transactions that update ledger state. The SimpleBank example illustrates contract state and functions, as well as a reentrancy vulnerability.
2 Background
- Ethereum stores accounts and associated data in a ledger, and deployed contracts are publicly accessible at an address but cannot be modified.Transactions invoke public functions and execute contract code on the network, subject to gas limits and runtime errors.Source: §2 · p. 3
- SimpleBank stores user balances in a mapping and exposes deposit and withdrawal functions that operate on Ether and the caller’s balance.Its top-level annotation states that the sum of individual balances equals the bank’s total balance.Source: §2 · p. 3, Figure 1 · p. 4
- SimpleBank’s withdrawal transfers Ether before deducting the caller’s balance, enabling reentrant calls to spend the same balance repeatedly.The passage connects this flaw to the DAO bug.Source: §2 · p. 4
3 Overview and Features
solc-verify extends the Solidity compiler with annotated, modular verification that translates contracts into Boogie, checks verification conditions with SMT solvers, and maps reported errors back to Solidity code.
3 Overview and Features
- In-code annotations specify contract invariants, function pre- and postconditions, and loop invariants as side-effect-free Solidity expressions.Contract invariants must hold before and after public functions and after construction; non-public functions are inlined to depth one by default.Source: §3 · pp. 4–5
- The Solidity compiler extension translates annotated contracts into Boogie for verification by the Boogie verifier and SMT solvers, then presents results at the Solidity code level.Reported errors are mapped back to the original contract with locations such as line numbers and function names.Source: §3 · pp. 4, 6, Figure 3 · p. 5
- A specification-language sum function tracks collections through an associated ghost variable that is updated alongside collection changes.The paper describes this encoding as a sufficient abstraction for its needs.Source: §3 · p. 5
- Correctness requires public calls without expected failures to avoid unexpected failures and satisfy their specifications.Expected failures include deliberate guards such as require or revert; unexpected failures include assertions and overflows.Source: §3 · p. 5
- Boogie generates verification conditions for SMT solvers, with the encoding enabling quantifier-free conditions and support for solvers without quantifiers.The implementation supports z3, cvc4, and an extension for yices2.Source: §3 · p. 5
- Gas is not modeled, so the current approach does not verify liveness properties or gas upper bounds.The paper notes that gas modeling could be added for those purposes.Source: §3 · p. 5
4 Translation Details and Properties
solc-verify translates Solidity contracts into Boogie and models contract, type, and Ethereum-specific behavior for verification. Its translation handles common Solidity constructs while retaining boundaries around unsupported features and arithmetic choices.
Contracts
- One Boogie program can represent one or multiple contracts, using available annotations across them; reasoning across contracts requires care because EVM addresses are untyped.Inheritance is supported through compiler flattening and virtual-call disambiguation.Source: §4 · p. 6
Types
- Arithmetic can use unbounded integers, bitvectors, or modular arithmetic with range assertions; structures, enums, and tuples are not currently supported.Bitvectors provide precise arithmetic but may scale poorly at Solidity’s default 256-bit size.Source: §4 · p. 6
State variables and functions
- State variables become address-indexed global mappings, and each function becomes a Boogie procedure with a receiver parameter identifying its contract instance.Calls pass the target contract’s address as the receiver; this models contract storage as a heap.Source: §4 · pp. 6–7, Figure 4 · p. 7
Functions and statements
- Modifiers are inlined, most Solidity statements map directly to Boogie, and deliberate exceptions become assumptions while assertions remain checks.Low-level call is treated as arbitrary external computation; callcode and delegatecall are unsupported because they require EVM-level modeling.Source: §4 · pp. 7, 9
Transactions
- Balances are modeled as a global address-to-integer map; payable calls pass transaction value, while send and transfer directly update that map.The caller’s balance is reduced before a payable call; an insufficient balance for send or transfer is modeled as an expected failure.Source: §4 · p. 8
Overflow detection
- Overflow conditions are accumulated and asserted at each basic-block end, allowing intervening manual checks to prevent false alarms from guarded arithmetic.The approach accommodates the common practice of checking arithmetic results after computation.Source: §4 · p. 9
5 Examples and Experiments on Real World Contracts
The experiments assess language coverage and scalability, inspect unannotated contracts for errors, and use annotations to find bugs and verify corrected contracts. They demonstrate both the scope and limits of solc-verify on real-world examples.
5.1 Language Coverage
- Roughly 50% of 7,836 selected contracts translated to Boogie across arithmetic modes, and average processing took around one second per contract.The authors caution that scalability depends on property complexity; bitvector encoding can become infeasible for more complex invariants.Source: §5.1 · p. 10, Table 1 · p. 10
5.2 Unannotated Contracts
- Of 88 contracts containing assertions, 80 triggered errors; 78 were false alarms from using assert where require was intended.The examples included assertions used to enforce input validity, time locks, call success, permissions, and arithmetic results.Source: §5.2 · p. 11
- Among 68 manually checked high-transaction contracts, solc-verify reported 33 overflow alarms: 29 false alarms and four potentially real issues.The false alarms largely reflected unstated magnitude assumptions, including array-length bounds and limits on Ether balances or timestamps.Source: §5.2 · p. 12
- A food-store overflow can bypass the msg.value >= cost check, while a batch-transfer counter overflow might be benign because the counter is otherwise unused.The food-store cost uses caller-provided bundles multiplied by price; the bypass could open the door to a potential exploit.Source: §5.2 · p. 12
5.3 Annotated Contracts
- The invariant sum(balances) == this.balance exposes the SimpleBank reentrancy bug, and solc-verify proves the reordered fix instantly.The invariant is violated when the contract deducts the balance after making the external call; reducing it first preserves the invariant before that call.Source: §5.3 · p. 13
- Modular arithmetic detects the BEC batchTransfer overflow and verifies the fixed version; annotated 256-bit VCs discharge in seconds, while bitvector mode does not terminate.The overflow invalidates the total transfer amount and can let attackers create tokens while keeping their own balance constant.Source: §5.3 · p. 14
- The annotated checks complement pattern-focused tools: Slither handles both bank versions but misses BEC overflow, while Mythril also flags the corrected bank version.The authors position solc-verify as complementary to tools that target well-known vulnerability patterns.Source: §5.3 · pp. 14–15
6 Related Work
Related work spans vulnerability-pattern, theorem-prover, automata-based, and SMT-based approaches. The paper distinguishes solc-verify through Solidity-level specifications and modular, automated verification.
Vulnerability pattern-based approaches
- Pattern-based approaches can check specific properties but are limited to built-in patterns, while reasoning about general properties is difficult in EVM-based approaches.The paper contrasts these approaches with checking high-level, user-defined properties directly in Solidity.Source: §6 · p. 15
Theorem prover-based approaches
- Theorem-prover approaches offer precise formal semantics but can require user interaction and formalizing properties in a separate prover language.The paper contrasts this with Solidity annotations and fully automated modular verification; loop invariants may still be needed, though complex contract loops are described as rare.Source: §6 · p. 15
Automata-based approaches
- Model-based approaches are orthogonal to source-code verification, which avoids requiring developers to learn a modeling language or transform models into source.The passage discusses FSolidM and manual modeling in BIP.Source: §6 · p. 16
SMT-based approaches
- Existing SMT-based tools have limits including unavailable comparisons, restricted scope or feature support, false overflow alarms, and no developer-supplied specifications beyond require and assert.The paper identifies contract-level invariants and fewer false overflow alarms among challenges its approach addresses.Source: §6 · p. 16
7 Conclusion
solc-verify uses modular program reasoning and SMT solvers to verify Solidity contracts at source level. It supports high-level properties through annotations and has been used to find bugs and prove correctness of non-trivial properties with minimal user effort.
7 Conclusion
- solc-verify automates verification of Solidity smart contracts using modular program reasoning and SMT solvers.It discharges verification conditions in a modular and scalable way.Source: §7 · p. 16
- At source level, developers can annotate contracts with invariants, loop invariants, pre- and post-conditions, and assertions.The tool reasons about high-level properties while working with Solidity source code.Source: §7 · p. 16
- On real-world contracts, solc-verify can find bugs and prove correctness of non-trivial properties with minimal user effort.The paper characterizes the approach as automated and user-friendly formal verification.Source: §7 · p. 16