solidity中的SMT（1）

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

例如对于如下代码

// 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类型相加，可能导致的溢出。

使用方法：

solc --model-checker-engine "all" --model-checker-targets "underflow,overflow" overflow.sol

其中

model-checker-engine指定了分析所使用的引擎，model-checker-targets指定使用的checker。执行的输出如下：

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：

       270.61 msec task-clock:u              #    0.997 CPUs utilized          
            0      context-switches:u        #    0.000 /sec                   
            0      cpu-migrations:u          #    0.000 /sec                   
       18,773      page-faults:u             #   69.374 K/sec                  
  855,936,173      cycles:u                  #    3.163 GHz                    
   55,947,528      stalled-cycles-frontend:u #    6.54% frontend cycles idle   
  133,702,666      stalled-cycles-backend:u  #   15.62% backend cycles idle    
1,102,148,341      instructions:u            #    1.29  insn per cycle         
                                             #    0.12  stalled cycles per insn
  225,395,044      branches:u                #  832.924 M/sec                  
    6,859,913      branch-misses:u           #    3.04% of all branches        

  0.271336637 seconds time elapsed

  0.243750000 seconds user
  0.026701000 seconds sys

BMC stat：

      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

当前已有的形式化规则：

enum class VerificationTargetType { 
    ConstantCondition,
    Underflow,
    Overflow,
    UnderOverflow,
    DivByZero,
    Balance,
    Assert,
    PopEmptyArray,
    OutOfBounds 
};

Custom Annotation

Solidity可以通过特定格式的注释标记函数的semantics，来提高SMT的分析效率（当然也可以用来降低准确性）。举例来说：

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就会给出警告。

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_);
   |         ^^^^^^^^^^^^^^^^