Introduction
Solidity实现了一种基于SMT（Satisfiability Modulo Theories）和Horn逻辑的形式化验证方法。SMTChecker模块自动尝试证明代码满足require和assert语句所给出的规范。也就是说，它将require语句视为某种假设，并试图证明assert语句中的条件始终为真。如果发现断言失败，可能会给用户一个反例，说明断言是如何被违反的。如果SMTChecker对一个属性没有给出警告，这意味着该属性是可满足的。
如此，solidity便可以在compile time进行下列属性的检查：
- Arithmetic underflow and overflow.
- Division by zero.
- Trivial conditions and unreachable code.
- Popping an empty array.
- Out of bounds index access.
- Insufficient funds for a transfer.
Example
例如对于如下代码
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
| // SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.4;
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);
}
}
|
我们希望在编译阶段可以发现潜在的overflow问题，就是add函数中的两个uint类型相加，可能导致的溢出。
使用方法：
1
| solc --model-checker-engine "all" --model-checker-targets "underflow,overflow" overflow.sol
|
其中
model-checker-engine指定了分析所使用的引擎，model-checker-targets指定使用的checker。执行的输出如下：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
| Warning: This is a pre-release compiler version, please do not use it in production.
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:10:16:
|
10 | return x_ + y_;
| ^^^^^^^
|
Model Checking Engines
Solidity目前实现有两种check engine。
- Bounded Model Checker (BMC)
- Constrained Horn Clauses (CHC)
BMC
BMC位于libsolidity/formal/BMC.h，是一种针对过程内的分析，也就是忽略函数调用带来的影响。循环也同样会被忽略。对于internal function如果没有递归那么则会做inline的分析。extern call在可能的情况下也会实现inline。总是，它是一种以轻量、快速为目标的引擎。
CHC
CHC位于libsolidity/formal/CHC.h。通过将合约的CFG建模为一个Horn clauses，实现分析。这样每个函数在被分析的时候都会考虑到在非限制情况下的side-effect（包括循环）。
CHC的分析能力比BMC强大许多，代价是更多的资源消耗。
一个直观的例子，对于上文的例子分别使用两种引擎并通过perf进行采样。
CHC stat：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
| 270.61 msec task-clock:u
0 context-switches:u
0 cpu-migrations:u
18,773 page-faults:u
855,936,173 cycles:u
55,947,528 stalled-cycles-frontend:u
133,702,666 stalled-cycles-backend:u
1,102,148,341 instructions:u
225,395,044 branches:u
6,859,913 branch-misses:u
0.271336637 seconds time elapsed
0.243750000 seconds user
0.026701000 seconds sys
|
BMC stat：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
| 36.98 msec task-clock:u # 0.984 CPUs utilized
0 context-switches:u # 0.000 /sec
0 cpu-migrations:u # 0.000 /sec
5,585 page-faults:u # 151.010 K/sec
95,168,344 cycles:u # 2.573 GHz
5,230,800 stalled-cycles-frontend:u # 5.50% frontend cycles idle
16,163,554 stalled-cycles-backend:u # 16.98% backend cycles idle
129,053,280 instructions:u # 1.36 insn per cycle
# 0.13 stalled cycles per insn
22,862,839 branches:u # 618.177 M/sec
583,533 branch-misses:u # 2.55% of all branches
0.037567873 seconds time elapsed
0.027219000 seconds user
0.010202000 seconds sys
|
前者几乎高出一个数量级，而如果代码越复杂，可以遇见性能差距就会越大。
Verfication Targets
当前已有的形式化规则：
1
2
3
4
5
6
7
8
9
10
11
| enum class VerificationTargetType {
ConstantCondition,
Underflow,
Overflow,
UnderOverflow,
DivByZero,
Balance,
Assert,
PopEmptyArray,
OutOfBounds
};
|
Custom Annotation
Solidity可以通过特定格式的注释标记函数的semantics，来提高SMT的分析效率（当然也可以用来降低准确性）。举例来说：
1
2
3
4
5
6
7
8
9
10
11
12
| contract SMTAnnotation {
/// @custom:smtchecker abstract-function-nondet
function no_effect(uint y_) internal pure returns (uint) {
return y_;
}
function test_abstract(uint x_) public pure {
uint y_ = no_effect(x_);
assert(y_ == x_);
}
}
|
正常情况下CHC是完全可以分析出no_effect的作用，对于表达式assert(y_ == x_);的结果为SAT。但是如果我们添加上一个abstract-function-nondet的annotation，那么no_effect就不会被SMT所使用，并且该annotation表代表的语义是返回一个nondeterministic value并且保持状态不变（即view或者pure语义），那么此时CHC就会给出警告。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
| Warning: CHC: Assertion violation happens here.
Counterexample:
x_ = 0
y_ = 1
Transaction trace:
SMTAnnotation.constructor()
SMTAnnotation.test_abstract(0)
SMTAnnotation.plus_one(0) -- internal call
--> overflow.sol:36:9:
|
36 | assert(y_ == x_);
| ^^^^^^^^^^^^^^^^
|