SMTChecker and SMT Solvers: Exploring Formal Verification One Step at a Time
OverviewIn our previous blog – “Formal Verification Made Easy with SMTChecker”, we talked about formal verification, Solidity’s SMTChecker, and showed an example to detect arithmetic overflow in smart contracts. At the end of the blog post, we showed how to extract the SMTLIB2 representation of the smart contract. In case you didn’t understand what was happening, contact our experts today.
In this blog post we take over from where we left in our previous blog post and use the extracted SMTLIB2 representation with a different SMT solver. We will use “assert” verification target to showcase the whole process. But first, you might be thinking there are already 2 SMT solvers integrated with SMTChecker, Z3 and CVC4 (BTW, now there are 3 SMT solvers starting from solc 0.8.18!). Why do we even need a different SMT solver? Also, what are SMT solvers anyway?
What is an SMT Solver?
SMT (Satisfiability Modulo Theories) solvers are automated reasoning tools that can determine the satisfiability of logical formulas that are expressed in a language that combines Boolean logic and various theories (such as arithmetic, arrays, bit-vectors, etc.). In other words, SMT solvers determine whether a given logical formula can be true or false based on a set of logical and mathematical rules.
SMT solvers are used in various applications such as software verification, formal verification of hardware designs, optimization, and automated theorem proving. They are highly effective in solving complex logical problems, as they can make use of efficient algorithms, heuristics, and decision procedures to explore the space of possible solutions.
Why do we Need a Different SMT Solver?
There are several reasons why different SMT solvers are needed:
- Different problem domains: Different SMT solvers are designed to work best on different problem domains. For example, some solvers are specialized in handling arithmetic problems, while others are better at dealing with bit-vector problems.
- Performance: Different SMT solvers can have different performance characteristics, depending on the type of problems they are designed to solve, their algorithms, and the quality of their implementations.
- Input language: SMT solvers can support different input languages, which can make it easier or harder to express certain types of problems in a given solver. For example, some solvers may have a more expressive array theory, while others may have a more efficient bit-vector theory.
- Theories and Decision Procedures: SMT solvers can have different theories and decision procedures, which can affect their ability to solve different types of problems. For example, some solvers may have a more efficient theory for solving arithmetic problems, while others may have a more advanced decision procedure for dealing with arrays.
- Soundness and Completeness: Different SMT solvers can have different levels of soundness and completeness, which can affect their ability to solve problems correctly and efficiently.
Example of “Assert” Verification Target
For this blog article, we use a simple smart contract “Monotonic” (see Figure 1) written in Solidity to showcase how SMTChecker is used to check invariants – properties which should always be true, otherwise there’s a bug. We will define an invariant for the contract, afterwards we will extract the SMTLIB2 representation, and finally send it to 2 different SMT solvers, Z3 and Eldarica.
Smart Contract – Monotonic
The contract defines two functions, “f” and “inv”. The “f” function is an internal, pure function that takes an unsigned integer argument x and returns “x * 42”. The require statement checks that x is less than the maximum value of an uint128, which is a 128-bit unsigned integer. The “inv” function is a public, pure function that takes two unsigned integer arguments “a” and “b”. The require statement checks that “b” is greater than “a”. The assert statement checks that the result of “f(b)” is greater than the result of “f(a)”. The assert statement is the invariant. This contract implements a monotonic function, meaning that it preserves the order of the input values. The “inv” function asserts this property by checking that the result of “f” for “b” is greater than the result of “f” for “a” when “b” is greater than “a”. You can save the smart contract from Figure 1 (“Monotonic”) in “Monotonic.sol” file.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Monotonic {
function f(uint x) internal pure returns (uint) {
require(x < type(uint128).max);
return x * 42;
}
function inv(uint a, uint b) public pure {
require(b > a);
assert(f(b) > f(a));
}
}
Figure 1: Smart Contract “Monotonic” [source]Using SMTChecker with Hardhat
For this blog we use hardhat but in principle any other development framework can be used, e.g., Truffle, Foundry. A complete tutorial on how to setup a hardhat project can be found at hardhat website. Once the hardhat project is setup, copy the “Monotonic.sol” smart contract into the “contracts” directory of your project. At this point, head over to the previous blog – “Formal Verification Made Easy with SMTChecker” and if you followed it closely, your “hardhat.config.js” file should eventually look as shown in Figure 2. It already has modelchecker information inside it. If you haven’t already, please update the contract filename and contract name to “Monotonic.sol” and “Monotonic”, respectively (highlighted in yellow). The green highlighted text shows that we don’t want to use any SMT solver, instead we want to generate SMTLIB2 representation only. Please note, you cannot use “smtlib2” with “z3”, and “cvc4” at the same time. The blue highlighted text “assert” tells the SMTChecker to handle assertions.
require("@nomicfoundation/hardhat-toolbox");
/** @type import('hardhat/config').HardhatUserConfig */
module.exports = {
solidity: {
version: "0.8.17",
settings: {
modelChecker: {
contracts: {
"contracts/Monotonic.sol": ["Monotonic"]
},
divModNoSlacks: true,
engine: "chc",
invariants: ["contract", "reentrancy"],
showUnproved: false,
solvers: ["smtlib2"],
targets: ["underflow", "overflow", "assert"],
timeout: 20000
}
}
}
Figure 2: hardhat.config.js with SMTCheckerNow compile the hardhat project with the following command (see Figure 3):
npx hardhat compileFigure 3: Compilation Command
Getting the SMT Formula
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 compiled contract. At this point, you need to extract the object “auxiliaryInputRequested” from the JSON file. The SMT formula in smtlib2 format follows this keyword. One issue is that the SMTLIB2 representation has additional information and characters in it, e.g., “\n” characters. Manually removing these newline characters will take a lot of time and it is error prone. You can use the Python script from Figure 4 to extract the “auxiliaryInputRequested” object, process it (remove unwanted characters and save the SMTLIB2 representation to a file with name “Monotonic.smt2”). Please don’t forget to update the “json_filename” with your file’s name (highlighted in yellow). You can also use your own python/java script to do all the processing.
import json
import sys
def remove_before_char(string, char):
index = string.find(char)
if index == -1:
return string
else:
return string[index :]
# Open the JSON file
Json_filename = “fbb465323458c6abb2cc6f4d7c3a2ww3.json” # your filename will vary
with open(json_filename, "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
my_object = json_data["output"]["auxiliaryInputRequested"]
#print(my_object) as string
str_out = json.dumps(my_object)
str_out = str_out.replace(r'\n', '\n')
#removing the characters before (
str_out = remove_before_char (str_out, "(")
# spliting the string into 2 parts to remove "}} characters
new_str = str_out.split('"', 1)
str_out = new_str [0]
print (str_out)
with open(Monotonic.smt2', 'w') as f:
print(str_out, file=f)
Figure 4: Python code to extract “auxiliaryInputRequested” objectUsing a Different SMT Solver
After you have the “*.smt2” file, you can use any SMT solver which uses HORN logic (if you used chc engine) or which is compatible with “declare-datatypes” keyword (if you used bmc engine). In the context of this blog post, we will use Eldarica model checker. Please visit their GitHub page and follow the instructions to install it on your system. Once you have installed Eldarica, you can give the “Monotonic.smt2” file as input to Eldarica as shown below (Figure 5).
./eld Monotonic.smt2Figure 5: Command to run Eldarica model checker
Eldarica will return SAT. At this point, you can explore the invariants, in particular, try “assert(!(f(b) > f(a)))”. Here, we are telling the SMT solver to give us the result for the case when f(b) is less than or equal to f(a). In this case it should return UNSAT, meaning that the SMT solver could not find any combination of inputs where condition was satisfied.
One cool trick which you can do is run Eldarica and Z3 in parallel on the same “Monotonic.smt2” file. You should get same result output. Please explore SMTChecker and also different solvers for your use case. If you are unsure about how to define strong invariants or which SMT solver to use, please contact our experts.
Final Thoughts
SMT solvers and invariants play a critical role in ensuring the correctness, reliability, and security of smart contracts. The use of different SMT solvers and the definition of clear and precise invariants can help to catch bugs and ensure that smart contracts function as intended.
We at Truscova are experts in using formal verification to ensure correctness of your complex smart contracts. We specialize in creating invariants to detect bugs in smart contracts. Our experts can sit with your team to guide you in your verification process.
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.