Formal Verification Made Easy with SMTChecker
What is Formal Verification?Formal verification is the process of proving or disproving the correctness of a system with respect to a certain formal specification. It involves the use of mathematical techniques and tools to analyze the system and ensure that it meets the desired properties. Often used in critical systems where reliability and safety are of utmost importance. It identifies errors and defects in a system and ensures that the system meets the required specifications before it is deployed.
Formal verification can also be applied to smart contracts where it can help to ensure that the contracts function as intended. It also ensures that smart contracts do not contain any errors or vulnerabilities that could potentially lead to financial loss or other consequences. This is especially relevant since smart contracts are immutable and can't be altered once deployed on the blockchain. Hence, it is crucial to make sure they are correct before deployment.
There are a number of tools and techniques that can be used for formal verification of smart contracts, including model checking, theorem proving, and static analysis. These tools and techniques can help to check the correctness of the contract's code and logic, and ensure that it meets the desired properties and requirements.
Solidity’s SMTChecker and Formal Verification
SMTChecker is a formal verification tool for smart contracts written in the Solidity programming language. It uses Z3 theorem prover to check the contracts against a set of formal specifications. This allows developers to express the desired properties of a smart contract in a formal language and then use mathematical techniques to prove that the contract meets those properties.
SMTChecker can be used to check for various properties such as:
- Out-of-bound array accesses
- Integer overflow/underflow
- Division by zero
- Reentrancy vulnerabilities
- Unbounded storage variables
Example of Overflow Detection
For this blog article, we use a simple smart contract “Overflow” (see Figure 1) written in Solidity to showcase how SMTChecker can be used to detect overflows in smart contracts. We also show how one can get the SMT formula generated by the SMTChecker.
Smart Contract – Overflow
The contract defines an "add" function which takes in two unsigned integers as input (x_ and y_) and returns the sum of these two integers. This function is marked as "internal pure", which means it can only be called by other functions within the same contract and doesn't change the state of the contract. Additionally, the contract has a constructor function, which initializes two immutable state variables "x" and "y" with the values passed as input (x_ and y_), respectively. The last function is called "stateAdd" which is marked as "public view" and returns the sum of the state variables "x" and "y" by calling the "add" function. The "view" keyword means that the function only reads the state, but doesn't change it. You can save the above “Overflow” contract in “overflow.sol” file.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Overflow {
uint immutable x;
uint immutable y;
function add(uint x_, uint y_) internal pure returns (uint) {
return x_ + y_;
}
constructor(uint x_, uint y_) {
(x, y) = (x_, y_);
}
function stateAdd() public view returns (uint) {
return add(x, y);
}
}
Figure 1: Smart Contract “Overflow” [source]Using SMTChecker without Frameworks
SMTChecker can be used with and without development frameworks. If you want to explore SMTChecker with a development framework, skip this section and jump to the next one. Please note, it is convenient to use a development framework for bigger projects. If you want to explore SMTChecker for smaller smart contracts, this method can be used. Now follow the steps:
- Open a command line terminal
- Compile the “overflow.sol” contract as shown in Figure 2.
solc overflow.sol --model-checker-engine chc --model-checker-targets "overflow" --model-checker-show-unprovedFigure 2: Compilation of “overflow.sol”
In Figure 2, the compiler switch “model-checker-targets” allows SMTChecker to detect only that particular type of vulnerability, e.g., overflow detection can be enabled, division by zero can be enabled by writing “divByZero”. A more comprehensive list of supported targets is available here. The compiler switch “model-checker-engine” tells SMTChecker which reasoning engine to use. In Figure 2, we use Constrained Horn Clauses (CHC) because it is much more powerful than the other reasoning engine available, i.e., Bounded Model Checker (BMC). The last compiler switch “model-checker-show-unproved” tells SMTChecker that if any targets have not been proven, then generate a warning that specifies the number of unproven targets.
When the command from Figure 2 is executed, the following output is displayed on screen as depicted in Figure 3.
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
x = 115792089237316195423570985008687907853269984665640564039457584007913129639935, y = 1
= 0
Transaction trace:
Overflow.constructor(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)
State: x = 115792089237316195423570985008687907853269984665640564039457584007913129639935, y = 1
Overflow.stateAdd()
Overflow.add(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1) -- internal call
--> overflow.sol:9:16:
|
9 | return x_ + y_;
| ^^^^^^^
Figure 3: Compilation OutputSMTChecker detects that the an overflow can happen in the smart contract. The interpretation of the displayed output is in the section “Interpreting the Output”.
Using SMTChecker with Hardhat
For this blog we use hardhat but in principle any other development framework can be used. A complete tutorial on how to setup a hardhat project can be found at hardhat website. Once the hardhat project is setup, copy the “overflow.sol” smart contract into the “contracts” directory of your project. At this point, if you followed the hardhat tutorial closely, your “hardhat.config.js” file should look as depicted in Figure 4.
require("@nomicfoundation/hardhat-toolbox");
/** @type import('hardhat/config').HardhatUserConfig */
module.exports = {
solidity: “0.8.17”,
};
Figure 4: hardhat.config.jsIt does not have any information for SMTChecker. Let’s add that as follows (see Figure 5):
require("@nomicfoundation/hardhat-toolbox");
/** @type import('hardhat/config').HardhatUserConfig */
module.exports = {
solidity: {
version: "0.8.17",
settings: {
modelChecker: {
contracts: {
"contracts/overflow.sol": ["Overflow"]
},
divModNoSlacks: true,
engine: "chc",
invariants: ["contract", "reentrancy"],
showUnproved: false,
solvers: ["z3"],
targets: ["underflow", "overflow", "assert"],
timeout: 20000
}
}
}
Figure 5: hardhat.config.js with SMTCheckerIn Figure 5, we add additional settings to enable model checker. We specify that the SMTChecker should only analyze “overflow.sol” to reduce complexity. One can add more contracts by listing them under “contracts” keyword. For more details on each keyword, please check here.
Now compile the hardhat project with the following command (see Figure 6):
npx hardhat compileFigure 6: Compilation Command
The output displayed on screen will be the same as shown in Figure 3.
Interpreting the Output
Compiling the smart contract “overflow.sol” with or without development frameworks results in the output as shown in Figure 3. The SMTChecker issues a warning that it has detected a case of arithmetic overflow in our smart contract in function “stateAdd()” which in turn calls ”add(…)” function. It shows a concrete counterexample (x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935) to make the resultant of “add” function overflow. It means if one gives these values as input to add function, it will result in an overflow. It shows the strength of SMTChecker which can accurately detect if an arithmetic operation will result in an overflow.
How to Get the SMT Formula
In some cases, one needs to know what was the SMT formula created from their Solidity code. The SMT formula is a representation of the properties of the smart contract in a formal language that can be understood by the theorem prover, i.e., Z3 or CVC4 in case of SMTChecker. There are multiple use cases which come to mind for the need to extract the SMT formula, e.g., using a different theorem prover, debugging, equivalence checking etc.
The good thing is that the SMTChecker can output the SMT formular in SMTLIB2 format, but there’s a catch. One has to disable the theorem provers. In the Figure 5, we need to replace the “solvers” from “z3” to “smtlib2”. Afterwards, we recompile the smart contract. Now, in the hardhat project you can go to directory “artifacts” followed by “build-info”. You can find a JSON file in the directory for your compiler contract. You can
import json
# Open the JSON file
with open("overflow_out.json", "r") as json_file:
# Load the JSON data from the file
json_data = json.load(json_file)
# Extract the object you want from the JSON data
smt_object = json_data["output"]["auxiliaryInputRequested"]
print(smt_object)
Figure 7: Python code to extract “auxiliaryInputRequested” objectopen the file in any text editor/browser of your choice. Look for the object “auxiliaryInputRequested”. The SMT formula in smtlib2 format follows this keyword. You can extract this info from the JSON file using python script or java script or any way you like. Figure 7 shows a sample python code to extract “auxiliaryInputRequested” object.
When the Python code from Figure 7 is executed, the SMT formula is displayed on screen as follows:
….. (x_3_1 Int) (x_3_2 Int) (x__21_1 Int) (x__7_0 Int) (x__7_1 Int) (y_5_0 Int) (y_5_1 Int) (y_5_2 Int) (y__23_1 Int) (y__9_0 Int) (y__9_1 Int)) (=> (and (and (block_8_add_18_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 y_5_0 x__7_0 y__9_0 state_1 x_3_1 y_5_1 x__7_1 y__9_1 _12_1) (and (=> true (and (>= expr_15_0 0) (<= expr_15_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_15_0 y__9_1) (and (=> true (and (>= expr_14_0 0) (<= expr_14_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_0 x__7_1) (and (= _12_1 0) (and (and (>= y__9_1 0) (<= y__9_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x__7_1 0) (<= x__7_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))) (and (> (+ expr_14_0 expr_15_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935) (= error_1 1))) (block_10_function_add__19_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 y_5_0 x__7_0 y__9_0 state_1 x_3_1 y_5_1 x__7_1 y__9_1 _12_1)))) (assert(forall ( (_12_0 Int) (_12_1 Int) (_38_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_14_0 Int) (expr_15_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int) (x__21_1 Int) (x__7_0 Int) (x__7_1 Int) (y_5_0 Int) (y_5_1 Int) (y_5_2 Int) (y__23_1 Int) (y__9_0 Int) (y__9_1 Int)) (=> (block_10_function_add__19_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 y_5_0 x__7_0 y__9_0 state_1 x_3_1 y_5_1 x__7_1 y__9_1 _12_1) (summary_3_function_add__19_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 y_5_0 x__7_0 y__9_0 state_1 x_3_1 y_5_1 x__7_1 y__9_1 _12_1)))) (assert(forall ( (_12_0 Int) (_12_1 Int) (_12_2 Int) (_38_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_14_0 Int) (expr_15_0 Int) (expr_16_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int) (x__21_1 Int) (x__7_0 Int) (x__7_1 Int) (y_5_0 Int) (y_5_1 Int) (y_5_2 Int) (y__23_1 Int) (y__9_0 Int) (y__9_1 Int)) (=> (and (and (block_8_add_18_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 y_5_0 x__7_0 y__9_0 state_1 x_3_1 y_5_1 x__7_1 y__9_1 _12_1) (and (= _12_2 expr_16_1) (and (=> true (and (>= expr_16_1 0) (<= expr_16_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_16_1 (+ expr_14_0 expr_15_0)) (and (= error_1 error_0) (and (=> true (and (>= expr_15_0 0) (<= expr_15_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_15_0 y__9_1) (and (=> true (and (>= expr_14_0 0) (<= expr_14_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_0 x__7_1) (and (= _12_1 0) (and (and (>= y__9_1 0) (<= y__9_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) …..Figure 8: Excerpt of the SMT formular in SMTLIB2 format
Figure 8 shows an excerpt of the SMT formula generated by SMTChecker. You might be confused and wondering, what am I looking at! Afterwards, the first thing you might notice is that your variables as defined in Figure 1 are nowhere to be seen. Now you must be having many questions!
Final Thoughts
SMTChecker is a powerful tool if used correctly. It can detect many vulnerabilities if the model checker is enabled. It can also give you the SMT formulas, if you want to explore different use-cases. However, it comes with its own set of limitations. To quote from SMTChecker’s website
“If a bug is reported, it might be a false positive introduced by abstractions (due to erasing knowledge or using a non-precise type). If it determines that a verification target is safe, it is indeed safe, that is, there are no false negatives (unless there is a bug in the SMTChecker)”We at Truscova are experts in using formal verification to ensure correctness of your complex smart contracts. We can fine-tune the solver to report accurate results.
About Truscova:
Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.