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