Model checking is a method of formally verifying whether a model of a system meets a specification. Modern model checkers can determine whether certain security properties hold true for a given program, and can automate the discovery of memory corruption bugs, unsafe arithmetic, assertion failures, and more. When a property is not found to hold, a model checker produces a counterexample that acts as a proof of its contradiction.
While working with our clients to test the security of high assurance software, such as smart contracts that transact valuable digital assets, we often find ourselves seeking a high level of confidence in a program’s correctness. A model checker is one type of tool with the potential of delivering this level of confidence when used effectively. Furthermore, the security properties we formulate can be later used by our clients to perform their own formal verification even after an engagement has ended. Many of these companies would not otherwise use formal methods due to their reputation of having steep learning curves and being highly academic.
This is why we are excited to see the development of a model checker within the Solidity compiler itself. Solidity is the predominant programming language for the Ethereum Virtual Machine (EVM), and is what many widely used smart contracts today are written in. While there are already several formal verification tools that support Solidity and/or the EVM, our hope is that having a model checker built directly into Solidity will make formal methods more accessible to developers. In addition, specifications are written inline using the Solidity language itself. This means that while there is some extra work involved in writing a specification, it does not come with the usual overhead of having to install a new tool and learn a new language.
At the time of writing this, Solidity’s model checker is still very much a work in progress, and we cannot yet recommend its sole use as a formal verification tool. However, a quick look at the Solidity GitHub repository shows promising and active development (http://github.com/ethereum/solidity/tree/develop/libsolidity/formal). In addition, one of its authors has demonstrated that it can find real bugs (https://medium.com/@leonardoalt/soliditys-smtchecker-can-automatically-find-real-bugs-beb566c24dea). This blog post aims to be an exploration of how Solidity’s model checker works, how it can be utilized to find certain types of bugs, and its current limitations.
SOLIDITY MODEL CHECKING 101
As stated, model checking is a method for formally verifying whether a model of a system meets a specification. In order to do this, Solidity’s model checker takes source code and encodes the parts it wants to reason about as SMT2, which is a language for SMT (satisfiability modulo theories) solvers. An SMT solver’s job is to take a system of constraints and determine whether a model exists. For example, a system containing the single constraint X > 3 has a model X = 7. However, a system containing the constraints X > 5 and X * 2 < 10 has no model. A popular SMT solver supported by Solidity is Microsoft’s Z3, which offers a good balance between performance and feature support.
The following graphic illustrates a simplified, high-level version of Solidity’s model checker process:
A sound model checker can do this type of encoding task without losing necessary information that could lead to false negatives (or if this is unavoidable, it emits warnings), while a complete model checker can do this encoding task without making generalizations that could lead to false positives. Solidity’s model checker is currently known to be sound but incomplete, while emitting warnings about unsupported language features (e.g., inline assembly). This means that the tool shouldn’t miss any bugs without warning you that it cannot reason about something, though it may also produce false positives which will need to be sorted through.
Bounded Model Checking
As it turns out, Solidity currently has two model checker engines that specialize in different uses of a backend SMT solver. The original one, a bounded model checker (BMC), is a relatively simple algorithm that analyzes Solidity functions in isolation. When encoding a Solidity source unit into SMT2, the checker navigates the unit’s abstract syntax tree (AST) and compiles a list of symbolic variables and constraints for each contract and function. Solidity’s built-in require function is used to declare assumptions made within the specification, while the built-in assert function is used to declare its verification targets (which may or may not have a possible model). Other AST nodes are used to determine the unit’s implementation.
The following example demonstrates that proving assertions that are local to a single basic function are straightforward. Note the use of the experimental SMTChecker pragma to enable the model checker.
pragma solidity >=0.5.0;
pragma experimental SMTChecker;
contract C {
function b(uint256 x) pure public {
require(x < 250 && x >= 10);
uint256 y = x * 2;
uint256 z = y - 15;
assert(z > 5);
}
}
Warning: Assertion violation happens here --> example1.sol:11:5: | 11 | assert(z > 5); | ^^^^^^^^^^^^^ Note: for: x = 10 y = 20 z = 5 Note: Callstack: Note:
Solidity’s BMC also contains several built-in checks for language-specific issues like integer underflows, integer overflows, division by zero, and insufficient funds on transfer. These types of built-in checks are exciting to see because they are provided “for free” and require virtually no effort to use.
The following example demonstrates this by having the BMC detect a more subtle and realistic bug, which can be exploited by an attacker to grant themselves unlimited tokens (hint: Consider the result of amount – fee(amount) when amount is zero):
pragma solidity >=0.5.0;
pragma experimental SMTChecker;
contract TransferWithFees {
address operator;
mapping (address => uint256) public balances;
constructor() public {
operator = msg.sender;
}
function transfer(address to, uint256 amount) public {
require(balances[msg.sender] >= amount, "Insufficient funds");
balances[msg.sender] -= amount;
balances[to] = safeAdd(balances[to], amount - fee(amount));
balances[operator] = safeAdd(balances[operator], fee(amount));
}
function fee(uint256 amount) internal pure returns(uint256) {
if(amount >= 1 ether) {
return 1 ether / 10000;
} if(amount >= 1 ether / 2) {
return 1 ether / 5000;
} else {
return 1 ether / 1000;
}
}
function safeAdd(uint256 a, uint256 b) internal pure returns(uint256) {
uint256 c = a + b;
require(c >= a, "Overflow on add");
return c;
}
}
Warning: Underflow (resulting value less than 0) happens here --> example2.sol:15:42: | 15 | balances[to] = safeAdd(balances[to], amount - fee(amount)); | ^^^^^^^^^^^^^^^^^^^^ Note: for: = 0x038d7eA4C68000 <result> = (- 1000000000000000) amount = 0 balances[msg.sender] = 0xFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFf8fb balances[to] = 0 msg.sender = 8366 operator = 8367 to = 8365 Note: Callstack: Note:
Unfortunately, this type of model checker is not without its limitations. As implied by its name, a bounded model checker can only analyze a finite number of program steps. This approach isn’t usually an issue for functions without loops. Consider that for if statements and Boolean operators, the model checker only needs to evaluate one extra path of execution. It asks the backend SMT solver to try finding a model for one version where the conditional returns true and another version where it returns false. However, with loops the model checker must also account for any number of loop iterations and the extra paths associated with them, which may become huge. This problem exists for virtually all Turing-complete languages and we call it state blowup.
To mitigate state blowup, Solidity’s model checker currently only considers one iteration of a loop. This approach alone would lead to unsoundness, so variables that were “touched” in the body of a loop have their knowledge of side effects erased and a warning is emitted. This leads to some obvious false positives such as the following:
pragma solidity >=0.5.0;
pragma experimental SMTChecker;
contract C {
function count() public pure returns(uint256) {
uint256 y = 0;
for(uint256 i = 0; i < 5; i++) {
y += y; // Effectively a NOP since y is always 0, but y is touched so the model checker erases knowledge.
}
return y;
}
}
Warning: Overflow (resulting value larger than 2**256 - 1) happens here --> example3.sol:9:7: | 9 | y += y; // Effectively a NOP since y is always 0, but y is touched so the model checker erases knowledge. | ^^^^^^ Note: for: = 0 <result> = 2**256 i = 0 y = 0x80 * 2**248 Note: Callstack: Note: Note that some information is erased after the execution of loops. You can re-introduce information using require().
Just as the warning explains, lost information can always be reintroduced using assumptions via require. While this can be helpful in some situations, it is often infeasible to work around this limitation without avoiding loops all together. How do other BMCs handle this issue?
Traditional BMCs take some integer k that acts as the upper bound of how many steps of executions to consider. When k is set to the minimal number of steps required to reach all program states (referred to as a program’s reachability diameter), soundness holds. The issue is that if k is set too high, the state blowup can quickly become intractable for complex programs. This is especially true when one considers contract interaction to be its own type of loop: While Solidity’s BMC only considers one function in isolation, an attacker is free to make zero or more calls to any of a contract’s public functions. A bug may not be found until a certain number of function calls are made in some particular order.
The inherit limitations of the bounded model checker have led to the recent introduction of a second type of model checker engine within Solidity that uses something called Constrained Horn Clauses.
Constrained Horn Clauses
When a SMT solver wants to efficiently reason about loops, it must have a way to efficiently reason about reachability. This becomes more apparent when we think of loops as recursive functions and ask if one program state may ever reach another. One way for an SMT solver to tackle this problem is by using Constrained Horn Clauses (CHCs) and Property Directed Reachability (PDR). CHCs are first-order logic formulas that are capable of encoding meaningful information about whether one program state is reachable from another. PDR is a relatively new type of incremental model checking algorithm that breaks the problem down into smaller subproblems called cubes, which can make it more tractable to analyze loops. Z3, as used by Solidity, incorporates both CHCs and PDR to more efficiently solve this otherwise intractable type of problem.
Just like the BMC, the CHC engine encodes a Solidity source unit into SMT2 by navigating the unit’s AST and compiling a list of symbolic variables and constraints. However, this time it navigates the unit and considers all possible paths of execution each contract can take. The CHC engine does this by attempting to synthesize the correct Horn clauses that accurately model these paths as logical relationships with constraints (which may or may not be recursive) between blocks of code. Z3 can then be asked to solve queries about these constrained logical relationships.
Consider the following button pressing puzzle as an example. Note that the CHC engine is able to quickly reason about the implications of calling each public function and evaluate if a model exists for not solving the puzzle. An assertion failure in is_not_solved would imply that the puzzle is solvable:
pragma solidity >=0.5.0;
pragma experimental SMTChecker;
contract C {
bool a;
bool b;
bool c;
bool d;
bool e;
bool f;
function pressA() public {
if(e) { a = true; } else { reset(); }
}
function pressB() public {
if(c) { b = true; } else { reset(); }
}
function pressC() public {
if(a) { c = true; } else { reset(); }
}
function pressD() public {
d = true;
}
function pressE() public {
if(d) { e = true; } else { reset(); }
}
function pressF() public {
if(b) { f = true; } else { reset(); }
}
function is_not_solved() view public {
assert(!f);
}
function reset() internal {
a = false;
b = false;
c = false;
d = false;
e = false;
f = false;
}
}
Warning: Assertion violation happens here --> example4.sol:37:5: | 37 | assert(!f); | ^^^^^^^^^^ Note: for: f = true Note: Callstack: Note:
While Solidity’s model checker doesn’t display the chain of independent function calls that led to a counterexample, it does guarantee that such a chain exists (as implied by f being set to true). It would be nice to see this type of information returned in future versions of the model checker.
Unfortunately, at the time of writing this it was too difficult to produce a more realistic example. This was largely due to an incompleteness of more complex types such as mappings when the CHC engine was used (e.g., see https://github.com/ethereum/solidity/issues/8688). A bug was also discovered that impacted the CHC engine’s ability to properly handle contract inheritance (https://github.com/ethereum/solidity/issues/8623). While the solver remains powerful, getting Solidity’s model checker closer to completeness is a challenging endeavor that will likely take some time.
Conclusion
Although Solidity’s model checker is very much a work in progress, we think that it is a tool with great potential. It is especially exciting to see built-in checks for language-specific issues like integer underflows, integer overflows, division by zero, and insufficient funds on transfer. This makes this tool already valuable, although incompleteness can lead to more false positives to sort through. We’d love to see this list extended to include other types of common bugs such as unsafe reentrancy, unsafe timestamp dependence, and denial of service. It is also exciting to see Solidity’s model checker make use of relatively new advances in model checking technology such as PDR. Although this feature is still in a very early phase of development, it could one day be used to detect more complex bugs.
We look forward to seeing this tool be developed further.
Author: Eric Rafaloff
