SMTChecker와 형식 검증

SMTChecker와 형식 검증 (SMTChecker and Formal Verification)

형식 검증(formal verification)을 사용하면 소스 코드가 특정 형식 명세를 충족한다는 자동화된 수학적 증명을 수행할 수 있어요. 명세는 여전히 형식적(소스 코드처럼)이지만, 보통 훨씬 더 단순해요. Solidity는 SMT(Satisfiability Modulo Theories)와 Horn 해석에 기반한 형식 검증 접근을 구현해요.

출처: 문서

본문

형식 검증(formal verification)을 사용하면 소스 코드가 특정 형식 명세를 충족한다는 자동화된 수학적 증명을 수행할 수 있어요. 명세는 여전히 형식적(소스 코드처럼)이지만, 보통 훨씬 더 단순해요. 형식 검증 자체는 여러분이 한 것(명세)과 어떻게 했는지(실제 구현) 사이의 차이를 이해하는 데만 도움이 될 수 있다는 점에 주의해요. 명세가 원하는 것인지, 의도하지 않은 효과를 놓치지 않았는지는 여전히 확인해야 해요.

Solidity는 SMT(Satisfiability Modulo Theories)와 Horn 해석에 기반한 형식 검증 접근을 구현해요. SMTChecker 모듈은 코드가 require와 assert 문으로 주어진 명세를 충족한다는 것을 자동으로 증명하려고 해요. 즉 require 문을 가정으로 간주하고 assert 문 안의 조건이 항상 참임을 증명하려고 해요. 어서션 실패가 발견되면, 어서션이 어떻게 위반될 수 있는지 보여 주는 반례(counterexample)가 사용자에게 주어질 수 있어요. SMTChecker가 어떤 속성에 대해 경고를 주지 않으면, 그 속성은 안전하다는 뜻이에요.

SMTChecker가 컴파일 시점에 확인하는 다른 검증 대상은:

산술 언더플로우와 오버플로우.
0으로 나누기.
사소한 조건과 도달할 수 없는 코드.
빈 배열 팝(pop).
범위를 벗어난 인덱스 접근.
전송에 대한 자금 부족.

위 모든 대상은 모든 엔진이 활성화되면 기본으로 자동 확인되지만, Solidity >=0.8.7의 경우 언더플로우와 오버플로우는 예외예요.

SMTChecker가 보고하는 잠재적 경고는 다음과 같아요:

<failing property> happens here. 이것은 SMTChecker가 특정 속성이 실패함을 증명했다는 뜻이에요. 반례가 주어질 수 있지만, 복잡한 상황에서는 반례를 보여 주지 않을 수도 있어요. 이 결과는 SMT 인코딩이 표현하기 어렵거나 불가능한 Solidity 코드에 추상화를 추가할 때 특정 경우에 거짓 양성(false positive)일 수도 있어요.
<failing property> might happen here. 이것은 솔버가 주어진 시간 초과 안에 어느 경우도 증명하지 못했다는 뜻이에요. 결과가 알려지지 않았으므로 SMTChecker는 건전성을 위해 잠재적 실패를 보고해요. 이것은 쿼리 타임아웃을 늘리면 해결될 수 있지만, 문제가 엔진이 풀기에 단순히 너무 어려울 수도 있어요.

SMTChecker를 활성화하려면 어떤 엔진을 실행할지 선택해야 하며, 기본은 엔진 없음이에요. 엔진을 선택하면 모든 파일에서 SMTChecker가 활성화돼요.

참고 (Note)

Solidity 0.8.4 이전에는 SMTChecker를 활성화하는 기본 방법은 pragma experimental SMTChecker;이었고 pragma를 포함하는 컨트랙트만 분석됐어요. 그 pragma는 비권장됐으며, 하위 호환을 위해 여전히 SMTChecker를 활성화하지만 0.9.0에서 제거될 거예요. 이제 단일 파일에서 pragma를 사용해도 모든 파일에 대해 SMTChecker가 활성화된다는 점도 주의해요.

참고 (Note)

검증 대상에 대한 경고의 부재는 SMTChecker와 기반 솔버에 버그가 없다고 가정할 때 논쟁의 여지가 없는 수학적 정확성 증명을 나타내요. 이런 문제는 매우 어렵고 일반적인 경우 자동으로 해결하기 불가능할 때가 많다는 점을 명심하세요. 따라서 여러 속성은 해결되지 않거나 큰 컨트랙트의 경우 거짓 양성으로 이어질 수 있어요. 모든 증명된 속성은 중요한 성과로 봐야 해요. 고급 사용자는 SMTChecker Tuning을 참고해 더 복잡한 속성을 증명하는 데 도움이 되는 몇 가지 옵션을 배울 수 있어요.

튜토리얼 (Tutorial)

오버플로우 (Overflow)

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

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);
    }
}

위 컨트랙트는 오버플로우 확인 예시를 보여 줘요. SMTChecker는 Solidity >=0.8.7의 경우 언더플로우와 오버플로우를 기본으로 확인하지 않으므로, 명령줄 옵션 --model-checker-targets "underflow,overflow" 또는 JSON 옵션 settings.modelChecker.targets = ["underflow", "overflow"]을 사용해야 해요. 대상 구성에 대한 이 절을 참고해요.

여기서 다음을 보고해요:

Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
 = 0

Transaction trace:
Overflow.constructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
State: x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
Overflow.stateAdd()
    Overflow.add(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call
 --> o.sol:9:20:
  |
9 |             return x_ + y_;
  |                    ^^^^^^^

오버플로우 경우를 걸러내는 require 문을 추가하면, SMTChecker는(경고를 보고하지 않음으로써) 오버플로우에 도달할 수 없다는 것을 증명해요:

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

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) {
        require(x < type(uint128).max);
        require(y < type(uint128).max);
        return add(x, y);
    }
}

Assert

어서션은 코드의 불변식(invariant)을 나타내요. 모든 트랜잭션, 모든 입력과 스토리지 값에 대해 참이어야 하는 속성이에요. 그렇지 않으면 버그가 있어요. 아래 코드는 오버플로우를 보장하는 함수 f를 정의해요. 함수 inv는 f가 단조 증가한다는 명세를 정의해요: 모든 가능한 쌍 (a, b)에 대해 b > a라면 f(b) > f(a). f가 실제로 단조 증가하므로 SMTChecker는 우리의 속성이 옳다고 증명해요. 속성과 함수 정의를 가지고 놀아보며 어떤 결과가 나오는지 보는 것을 권장해요!

open in Remix

// 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));
    }
}

더 복잡한 속성을 검증하기 위해 루프 안에 어서션을 추가할 수도 있어요. 다음 코드는 제한 없는 숫자 배열의 최대 요소를 찾고, 찾은 요소가 배열의 모든 요소보다 크거나 같아야 한다는 속성을 단언해요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Max {
    function max(uint[] memory a) public pure returns (uint) {
        uint m = 0;
        for (uint i = 0; i < a.length; ++i)
            if (a[i] > m)
                m = a[i];

        for (uint i = 0; i < a.length; ++i)
            assert(m >= a[i]);

        return m;
    }
}

이 예시에서 SMTChecker는 세 가지 속성을 자동으로 증명하려고 할 거예요:

첫 번째 루프의 ++i가 오버플로우하지 않음.
두 번째 루프의 ++i가 오버플로우하지 않음.
어서션이 항상 참.

참고 (Note)

이 속성들은 루프를 포함해 이전 예시보다 훨씬 훨씬 어려우니 루프에 주의하세요!

모든 속성이 올바르게 안전하다고 증명돼요. 속성이나 배열 제한을 바꿔 다른 결과를 보세요. 예를 들어 코드를 다음으로 바꾸면:

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Max {
    function max(uint[] memory a) public pure returns (uint) {
        require(a.length >= 5);
        uint m = 0;
        for (uint i = 0; i < a.length; ++i)
            if (a[i] > m)
                m = a[i];

        for (uint i = 0; i < a.length; ++i)
            assert(m > a[i]);

        return m;
    }
}

다음을 얻어요:

Warning: CHC: Assertion violation happens here.
Counterexample:

a = [0, 0, 0, 0, 0]
 = 0

Transaction trace:
Test.constructor()
Test.max([0, 0, 0, 0, 0])
  --> max.sol:14:4:
   |
14 |            assert(m > a[i]);

상태 속성 (State Properties)

지금까지 예시는 pure 코드에 대한 SMTChecker 사용만 보여 줬어요. 특정 연산이나 알고리즘에 대한 속성을 증명했죠. 스마트 컨트랙트에서 흔한 속성 유형은 컨트랙트의 상태를 포함하는 속성이에요. 그런 속성에 대해 어서션이 실패하게 하려면 여러 트랜잭션이 필요할 수 있어요.

예를 들어 두 축 모두 좌표가 범위(-2^127, 2^127 - 1)에 있는 2D 그리드를 고려해 보세요. 로봇을 위치 (0, 0)에 놓아요. 로봇은 대각선으로만, 한 번에 한 걸음씩 움직일 수 있고, 그리드 밖으로 움직일 수 없어요. 로봇의 상태 머신은 아래 스마트 컨트랙트로 나타낼 수 있어요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Robot {
    int x = 0;
    int y = 0;

    modifier wall {
        require(x > type(int128).min && x < type(int128).max);
        require(y > type(int128).min && y < type(int128).max);
        _;
    }

    function moveLeftUp() wall public {
        --x;
        ++y;
    }

    function moveLeftDown() wall public {
        --x;
        --y;
    }

    function moveRightUp() wall public {
        ++x;
        ++y;
    }

    function moveRightDown() wall public {
        ++x;
        --y;
    }

    function inv() public view {
        assert((x + y) % 2 == 0);
    }
}

함수 inv는 x + y가 짝수여야 한다는 상태 머신의 불변식을 나타내요. SMTChecker는 로봇에게 얼마나 많은 명령을 주든, 무한히 많이 주더라도 불변식이 결코 실패할 수 없다는 것을 증명해요. 관심 있는 독자는 그 사실을 수동으로도 증명하고 싶을 수 있어요. 힌트: 이 불변식은 귀납적(inductive)이에요.

SMTChecker를 속여 우리가 도달 가능하다고 생각하는 특정 위치로의 경로를 알게 할 수도 있어요. 다음 함수를 추가해 (2, 4)가 도달 불가능하다는 속성을 추가할 수 있어요.

open in Remix

function reach_2_4() public view {
    assert(!(x == 2 && y == 4));
}

이 속성은 거짓이고, 속성이 거짓임을 증명하는 동안 SMTChecker는 (2, 4)에 정확히 어떻게 도달하는지 알려 줘요:

Warning: CHC: Assertion violation happens here.
Counterexample:
x = 2, y = 4

Transaction trace:
Robot.constructor()
State: x = 0, y = 0
Robot.moveLeftUp()
State: x = (- 1), y = 1
Robot.moveRightUp()
State: x = 0, y = 2
Robot.moveRightUp()
State: x = 1, y = 3
Robot.moveRightUp()
State: x = 2, y = 4
Robot.reach_2_4()
  --> r.sol:35:4:
   |
35 |            assert(!(x == 2 && y == 4));
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^

위 경로가 반드시 결정적이지는 않다는 점에 주의해요. (2, 4)에 도달할 수 있는 다른 경로가 있기 때문이에요. 어떤 경로가 표시되는지 선택은 사용된 솔버, 그 버전, 또는 그냥 무작위로 바뀔 수 있어요.

외부 호출과 재진입 (External Calls and Reentrancy)

모든 외부 호출은 SMTChecker에 의해 알 수 없는 코드에 대한 호출로 취급돼요. 그 이유는 호출된 컨트랙트의 코드가 컴파일 시점에 사용 가능하더라도, 배포된 컨트랙트가 실제로 컴파일 시점에 인터페이스가 온 컨트랙트와 같을 것이라는 보장이 없기 때문이에요.

어떤 경우에는 외부로 호출된 코드가 무엇이든 할 수 있어도(호출자 컨트랙트에 재진입하는 것을 포함) 여전히 참인 상태 변수에 대한 속성을 자동으로 추론하는 것이 가능해요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

interface Unknown {
    function run() external;
}

contract Mutex {
    uint x;
    bool lock;

    Unknown immutable unknown;

    constructor(Unknown u) {
        require(address(u) != address(0));
        unknown = u;
    }

    modifier mutex {
        require(!lock);
        lock = true;
        _;
        lock = false;
    }

    function set(uint x_) mutex public {
        x = x_;
    }

    function run() mutex public {
        uint xPre = x;
        unknown.run();
        assert(xPre == x);
    }
}

위 예시는 재진입을 금지하기 위해 mutex 플래그를 사용하는 컨트랙트를 보여 줘요. 솔버는 unknown.run()이 호출될 때 컨트랙트가 이미 "잠금"되어 있음을 추론할 수 있고, 알 수 없는 호출된 코드가 무엇을 하든 x의 값을 바꾸는 것이 불가능해요.

함수 set에서 mutex 수정자를 "잊어버리면", SMTChecker는 외부로 호출된 코드의 동작을 합성해 어서션이 실패하게 할 수 있어요:

Warning: CHC: Assertion violation happens here.
Counterexample:
x = 1, lock = true, unknown = 1

Transaction trace:
Mutex.constructor(1)
State: x = 0, lock = false, unknown = 1
Mutex.run()
    unknown.run() -- untrusted external call, synthesized as:
        Mutex.set(1) -- reentrant call
  --> m.sol:32:3:
   |
32 |                assert(xPre == x);
   |                ^^^^^^^^^^^^^^^^^

SMTChecker 옵션과 튜닝 (SMTChecker Options and Tuning)

시간 초과 (Timeout)

SMTChecker는 솔버별로 선택된 하드코딩된 리소스 한도(rlimit)를 사용하며, 이는 시간과 정확히 관련되지 않아요. 우리는 시간보다 솔버 안에서 더 많은 결정성 보장을 주기 때문에 rlimit 옵션을 기본으로 선택했어요. 이 옵션은 대략 "쿼리당 수 초 시간 초과"로 해석돼요. 물론 많은 속성이 매우 복잡하고 많은 시간이 필요해 결정성이 중요하지 않아요.

SMTChecker가 기본 rlimit으로 컨트랙트 속성을 해결하지 못하면, CLI 옵션 --model-checker-timeout <time> 또는 JSON 옵션 settings.modelChecker.timeout=<time>으로 밀리초 단위의 시간 초과를 줄 수 있어요. 여기서 0은 시간 초과 없음을 뜻해요.

검증 대상 (Verification Targets)

SMTChecker가 만드는 검증 대상의 유형은 CLI 옵션 --model-checker-target <targets> 또는 JSON 옵션 settings.modelChecker.targets=<targets>으로도 커스터마이즈할 수 있어요. CLI 경우 <targets>는 공백 없는 쉼표로 구분된 하나 이상의 검증 대상 목록이고, JSON 입력에서는 문자열로 된 하나 이상의 대상 배열이에요.

대상을 나타내는 키워드는:

어서션: assert.
산술 언더플로우: underflow.
산술 오버플로우: overflow.
0으로 나누기: divByZero.
사소한 조건과 도달할 수 없는 코드: constantCondition.
빈 배열 팝: popEmptyArray.
범위를 벗어난 배열/고정 바이트 인덱스 접근: outOfBounds.
전송에 대한 자금 부족: balance.
위 모두: default(CLI 전용).

흔한 대상 부분집합은 예를 들어 --model-checker-targets assert,overflow 같은 것이에요. 모든 대상이 기본으로 확인되지만, Solidity >=0.8.7의 경우 언더플로우와 오버플로우는 예외예요. 검증 대상을 언제 어떻게 나눌지에 대한 정확한 휴리스틱은 없지만, 특히 큰 컨트랙트를 다룰 때 유용할 수 있어요.

증명된 대상 (Proved Targets)

증명된 대상이 있으면 SMTChecker는 각 엔진에 대해 증명된 대상의 수를 알리는 경고를 하나씩 내요. 모든 특정 증명된 대상을 보고 싶으면 CLI 옵션 --model-checker-show-proved-safe와 JSON 옵션 settings.modelChecker.showProvedSafe = true를 사용할 수 있어요.

증명되지 않은 대상 (Unproved Targets)

증명되지 않은 대상이 있으면 SMTChecker는 증명되지 않은 대상이 몇 개인지 알리는 경고를 하나 내요. 모든 특정 증명되지 않은 대상을 보고 싶으면 CLI 옵션 --model-checker-show-unproved와 JSON 옵션 settings.modelChecker.showUnproved = true을 사용할 수 있어요.

지원되지 않는 언어 기능 (Unsupported Language Features)

어셈블리 블록 같은 특정 Solidity 언어 기능은 SMTChecker가 적용하는 SMT 인코딩에서 완전히 지원되지 않아요. 지원되지 않는 구조는 건전성을 보존하기 위해 과잉 근사(overapproximation)로 추상화돼, 이 기능이 지원되지 않아도 안전하다고 보고된 어떤 속성도 안전하다는 뜻이에요. 그러나 대상 속성이 지원되지 않는 기능의 정밀한 동작에 의존할 때 그런 추상화는 거짓 양성을 일으킬 수 있어요.

인코더가 그런 경우를 만나면 기본으로 본 것이 지원되지 않는 기능이 몇 개인지 알리는 일반 경고를 보고해요. 모든 특정 지원되지 않는 기능을 보고 싶으면 CLI 옵션 --model-checker-show-unsupported와 JSON 옵션 settings.modelChecker.showUnsupported = true을 사용할 수 있고, 그 기본 값은 false예요.

검증된 컨트랙트 (Verified Contracts)

기본으로 주어진 소스의 모든 배포 가능한 컨트랙트가 배포될 것으로서 개별 분석돼요. 이는 컨트랙트에 많은 직접·간접 상속 부모가 있으면, 비록 블록체인에서 가장 파생된 것만 직접 접근되더라도 그들 모두가 자체로 분석된다는 뜻이에요. 이는 SMTChecker와 솔버에 불필요한 부담을 줘요. 이런 경우를 돕기 위해, 사용자는 어떤 컨트랙트를 배포된 것으로 분석할지 지정할 수 있어요. 부모 컨트랙트는 물론 여전히 분석되지만, 가장 파생된 컨트랙트의 맥락에서만 분석되어 인코딩과 생성된 쿼리의 복잡성을 줄여요. 추상 컨트랙트는 기본으로 SMTChecker가 가장 파생된 것으로 분석하지 않는다는 점에 주의해요.

선택된 컨트랙트는 CLI에서 <source>:<contract> 쌍의 쉼표로 구분된 목록(공백 허용되지 않음)으로 줄 수 있어요: --model-checker-contracts "<source1.sol:contract1>,<source2.sol:contract2>,<source2.sol:contract3>", 그리고 JSON 입력의 settings.modelChecker.contracts 객체로도 줄 수 있는데, 그 형태는 다음과 같아요:

"contracts": {
    "source1.sol": ["contract1"],
    "source2.sol": ["contract2", "contract3"]
}

신뢰할 수 있는 외부 호출 (Trusted External Calls)

기본적으로 SMTChecker는 컴파일 시점에 사용 가능한 코드가 외부 호출에 대한 런타임 코드와 같다고 가정하지 않아요. 다음 컨트랙트를 예로 들어요:

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Ext {
    uint public x;
    function setX(uint _x) public { x = _x; }
}
contract MyContract {
    function callExt(Ext _e) public {
        _e.setX(42);
        assert(_e.x() == 42);
    }
}

MyContract.callExt가 호출될 때 인자로 주소가 주어져요. 배포 시점에 주소 _e가 실제로 컨트랙트 Ext의 배포를 포함한다는 것을 확실히 알 수 없어요. 따라서 SMTChecker는 위 어서션이 위반될 수 있다고 경고할 거예요. _e가 Ext가 아닌 다른 컨트랙트를 포함한다면 사실이에요.

그러나 이런 외부 호출을 신뢰할 수 있는 것으로 취급하는 것이 유용할 수 있어요. 예를 들어 인터페이스의 다른 구현들이 같은 속성을 준수하는지 테스트하기 위해서요. 이는 주소 _e가 정말 컨트랙트 Ext로 배포됐다고 가정한다는 뜻이에요. 이 모드는 CLI 옵션 --model-checker-ext-calls=trusted 또는 JSON 필드 settings.modelChecker.extCalls: "trusted"로 활성화할 수 있어요.

이 모드를 활성화하면 SMTChecker 분석이 훨씬 더 계산 비용적으로 비쌀 수 있다는 점을 알아두세요.

이 모드의 중요한 부분은 컨트랙트 타입과 컨트랙트에 대한 고수준 외부 호출에 적용되고, call과 delegatecall 같은 저수준 호출에는 적용되지 않는다는 것이에요. 주소의 스토리지는 컨트랙트 타입별로 저장되고, SMTChecker는 외부로 호출된 컨트랙트가 호출자 표현식의 타입을 가진다고 가정해요. 따라서 주소나 컨트랙트를 다른 컨트랙트 타입으로 캐스팅하면 다른 스토리지 값을 만들어, 아래 예시처럼 가정이 일관되지 않으면 건전하지 않은 결과를 줄 수 있어요:

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract D {
    constructor(uint _x) { x = _x; }
    uint public x;
    function setX(uint _x) public { x = _x; }
}

contract E {
    constructor() { x = 2; }
    uint public x;
    function setX(uint _x) public { x = _x; }
}

contract C {
    function f() public {
        address d = address(new D(42));

        // `d` was deployed as `D`, so its `x` should be 42 now.
        assert(D(d).x() == 42); // should hold
        assert(D(d).x() == 43); // should fail

        // E and D have the same interface, so the following
        // call would also work at runtime.
        // However, the change to `E(d)` is not reflected in `D(d)`.
        E(d).setX(1024);

        // Reading from `D(d)` now will show old values.
        // The assertion below should fail at runtime,
        // but succeeds in this mode's analysis (unsound).
        assert(D(d).x() == 42);
        // The assertion below should succeed at runtime,
        // but fails in this mode's analysis (false positive).
        assert(D(d).x() == 1024);
    }
}

위 때문에, address 또는 contract 타입의 특정 변수에 대한 신뢰할 수 있는 외부 호출이 항상 같은 호출자 표현식 타입을 가지도록 확인하세요. 또한 상속의 경우 호출된 컨트랙트의 변수를 가장 파생된 타입의 타입으로 캐스팅하는 것이 도움이 돼요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

interface Token {
    function balanceOf(address _a) external view returns (uint);
    function transfer(address _to, uint _amt) external;
}

contract TokenCorrect is Token {
    mapping (address => uint) balance;
    constructor(address _a, uint _b) {
        balance[_a] = _b;
    }
    function balanceOf(address _a) public view override returns (uint) {
        return balance[_a];
    }
    function transfer(address _to, uint _amt) public override {
        require(balance[msg.sender] >= _amt);
        balance[msg.sender] -= _amt;
        balance[_to] += _amt;
    }
}

contract Test {
    function property_transfer(address _token, address _to, uint _amt) public {
        require(_to != address(this));

        TokenCorrect t = TokenCorrect(_token);

        uint xPre = t.balanceOf(address(this));
        require(xPre >= _amt);
        uint yPre = t.balanceOf(_to);

        t.transfer(_to, _amt);
        uint xPost = t.balanceOf(address(this));
        uint yPost = t.balanceOf(_to);

        assert(xPost == xPre - _amt);
        assert(yPost == yPre + _amt);
    }
}

함수 property_transfer에서 외부 호출이 변수 t에 대해 수행된다는 점에 주의해요.

이 모드의 또 다른 주의점은 분석된 컨트랙트 밖의 컨트랙트 타입 상태 변수에 대한 호출이에요. 아래 코드에서 B가 A를 배포해도, B 자체에 대한 트랜잭션 사이에 저장된 B.a의 주소가 B 밖의 누구에게든 호출될 가능성이 있어요. B.a에 대한 가능한 변경을 반영하기 위해, 인코딩은 B.a에 대한 무한한 수의 호출이 외부로 이루어질 수 있게 허용해요. 인코딩은 B.a의 스토리지를 추적하므로 어서션 (2)는 유지되어야 해요. 그러나 현재 인코딩은 그런 호출이 개념적으로 B에서 이루어질 수 있게 허용하므로 어서션 (3)은 실패해요. 인코딩을 논리적으로 더 강하게 만드는 것은 신뢰 모드의 확장이며 개발 중이에요. 인코딩은 address 변수의 스토리지를 추적하지 않으므로, B.a가 address 타입이었다면 인코딩은 그 스토리지가 B에 대한 트랜잭션 사이에 바뀌지 않는다고 가정할 거예요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract A {
    uint public x;
    address immutable public owner;
    constructor() {
        owner = msg.sender;
    }
    function setX(uint _x) public {
        require(msg.sender == owner);
        x = _x;
    }
}

contract B {
    A a;
    constructor() {
        a = new A();
        assert(a.x() == 0); // (1) should hold
    }
    function g() public view {
        assert(a.owner() == address(this)); // (2) should hold
        assert(a.x() == 0); // (3) should hold, but fails due to a false positive
    }
}

보고된 추론 귀납적 불변식 (Reported Inferred Inductive Invariants)

CHC 엔진으로 안전하게 증명된 속성에 대해, SMTChecker는 Horn 솔버가 증명의 일부로 추론한 귀납적 불변식을 검색할 수 있어요. 현재 사용자에게 보고할 수 있는 불변식 유형은 두 가지뿐이에요:

컨트랙트 불변식(Contract Invariants): 컨트랙트가 실행할 수 있는 모든 가능한 트랜잭션 전후에 참인 컨트랙트 상태 변수에 대한 속성. 예: x >= y(여기서 x와 y는 컨트랙트의 상태 변수).
재진입 속성(Reentrancy Properties): 알 수 없는 코드에 대한 외부 호출이 있을 때의 컨트랙트 동작을 나타냄. 이 속성들은 외부 호출 전후의 상태 변수 값 사이의 관계를 표현할 수 있으며, 외부 호출은 재진입 호출을 포함해 무엇이든 자유롭게 할 수 있어요. 프라임 처리된 변수는 그 외부 호출 후의 상태 변수 값을 나타내요. 예: lock -> x = x'.

사용자는 CLI 옵션 --model-checker-invariants "contract,reentrancy" 또는 JSON 입력의 settings.modelChecker.invariants 필드에서 배열로 보고할 불변식 유형을 선택할 수 있어요. 기본으로 SMTChecker는 불변식을 보고하지 않아요.

슬랙 변수를 가진 나눗셈과 모듈로 (Division and Modulo With Slack Variables)

SMTChecker가 사용하는 기본 Horn 솔버인 Spacer는 Horn 규칙 안의 나눗셈과 모듈로 연산을 자주 싫어해요. 그 때문에 기본으로 Solidity 나눗셈과 모듈로 연산은 d = a / b이고 m = a % b일 때 제약 a = b * d + m을 사용해 인코딩돼요. 그러나 Eldarica 같은 다른 솔버는 구문적으로 정밀한 연산을 선호해요. 명령줄 플래그 --model-checker-div-mod-no-slacks와 JSON 옵션 settings.modelChecker.divModNoSlacks를 사용해 사용된 솔버 선호도에 따라 인코딩을 토글할 수 있어요.

Natspec 함수 추상화 (Natspec Function Abstraction)

pow와 sqrt 같은 공통 수학 메서드를 포함한 특정 함수는 완전 자동 방식으로 분석하기에 너무 복잡할 수 있어요. 이 함수들은 SMTChecker가 그 함수들을 추상화해야 함을 나타내는 Natspec 태그로 주석 처리될 수 있어요. 이는 함수의 본문이 사용되지 않고, 호출될 때 함수가:

비결정적 값을 반환하고, 추상화된 함수가 view/pure이면 상태 변수를 그대로 유지하거나, 그렇지 않으면 상태 변수도 비결정적 값으로 설정한다는 뜻이에요. 이는 주석 /// @custom:smtchecker abstract-function-nondet으로 사용할 수 있어요.
해석되지 않은 함수로 동작한다는 뜻. 이는 함수의 의미(본문이 주는)가 무시되고, 이 함수가 가진 유일한 속성은 같은 입력이 주어지면 같은 출력을 보장한다는 것이에요. 현재 개발 중이며 주석 /// @custom:smtchecker abstract-function-uf으로 사용할 수 있을 거예요.

모델 검사 엔진 (Model Checking Engines)

SMTChecker 모듈은 두 가지 다른 추론 엔진, Bounded Model Checker(BMC)와 Constrained Horn Clauses(CHC) 시스템을 구현해요. 두 엔진 모두 현재 개발 중이며 다른 특성이 있어요. 엔진은 독립적이고, 모든 속성 경고는 어느 엔진에서 왔는지 알려 줘요. 위의 모든 반례가 있는 예시는 더 강력한 엔진인 CHC가 보고했어요.

기본으로 두 엔진이 모두 사용되며, CHC가 먼저 실행되고 증명되지 않은 모든 속성이 BMC로 전달돼요. CLI 옵션 --model-checker-engine {all,bmc,chc,none} 또는 JSON 옵션 settings.modelChecker.engine={all,bmc,chc,none}으로 특정 엔진을 선택할 수 있어요.

Bounded Model Checker (BMC)

경고 (Warning)

BMC 엔진은 비권장됐고 미래 릴리스에서 제거될 거예요. bmc로 명시적으로 선택하거나 all로 암시적으로 선택하면 비권장 경고가 발생해요. 대신 CHC 엔진을 사용하세요.

BMC 엔진은 함수를 독립적으로 분석해요. 즉 각 함수를 분석할 때 여러 트랜잭션에 걸친 컨트랙트의 전체 동작을 고려하지 않아요. 이 엔진에서 루프도 현재 무시돼요. 내부 함수 호출은 직접 재귀든 간접 재귀든 재귀적이지 않은 한 인라인돼요. 외부 함수 호출은 가능하면 인라인돼요. 재진입에 의해 잠재적으로 영향을 받는 지식은 지워져요.

위 특성들 때문에 BMC는 거짓 양성을 보고하기 쉬우지만, 가볍고 작은 로컬 버그를 빠르게 찾을 수 있어야 해요.

Constrained Horn Clauses (CHC)

컨트랙트의 Control Flow Graph(CFG)는 Horn 절의 시스템으로 모델링돼요. 여기서 컨트랙트의 수명 주기는 모든 public/external 함수를 비결정적으로 방문할 수 있는 루프로 표현돼요. 이렇게 하면 어떤 함수를 분석할 때도 무한한 수의 트랜잭션에 걸친 전체 컨트랙트의 동작이 고려돼요. 이 엔진은 루프를 완전히 지원해요. 내부 함수 호출은 지원되고, 외부 함수 호출은 호출된 코드가 알 수 없고 무엇이든 할 수 있다고 가정해요.

CHC 엔진은 증명할 수 있는 것의 측면에서 BMC보다 훨씬 강력하고, 더 많은 컴퓨팅 리소스가 필요할 수 있어요.

SMT와 Horn 솔버 (SMT and Horn solvers)

위에서 자세히 설명한 두 엔진은 논리 백엔드로 자동 정리 증명기(automated theorem provers)를 사용해요. BMC는 SMT 솔버를 사용하는 반면 CHC는 Horn 솔버를 사용해요. 종종 같은 도구가 둘 다로 동작할 수 있는데, z3처럼요. z3는 주로 SMT 솔버이고 Spacer를 Horn 솔버로 사용할 수 있게 하며, Eldarica는 둘 다 해요.

사용자는 CLI 옵션 --model-checker-solvers {all,cvc5,eld,smtlib2,z3} 또는 JSON 옵션 settings.modelChecker.solvers=[smtlib2,z3]으로 사용할 솔버를(가능하면) 선택할 수 있는데, 여기서:

cvc5는 시스템에 설치되어야 하는 바이너리를 통해 사용돼요. BMC만 cvc5를 사용해요.
eld는 시스템에 설치되어야 하는 바이너리를 통해 사용돼요. CHC만 eld를 사용하고, z3가 활성화되지 않았을 때만 그래요.
smtlib2는 smtlib2 형식으로 SMT/Horn 쿼리를 출력해요. 이것들은 컴파일러의 콜백 메커니즘과 함께 사용될 수 있어서, 시스템의 어떤 솔버 바이너리든 쿼리의 결과를 컴파일러에 동기적으로 반환하는 데 사용될 수 있어요. 이것은 호출된 솔버에 따라 BMC와 CHC 둘 다가 사용할 수 있어요.
z3는 soljson.js에 정적으로 사용 가능해요(Solidity 0.6.9부터). 즉 컴파일러의 JavaScript 바이너리. 그 외에는 시스템에 설치되어야 하는 바이너리를 통해 사용돼요.

참고 (Note)

z3 버전 4.8.16은 이전 버전과 ABI 호환성이 깨졌고 solc <=0.8.13과 함께 사용될 수 없어요. z3 >=4.8.16을 사용한다면 solc >=0.8.14를 사용하고, 반대로 옛 solc 릴리스에는 옛 z3만 사용하세요. 또한 SMTChecker가 하는 것처럼 최신 z3 릴리스를 사용할 것을 권장해요.

BMC와 CHC 둘 다 z3를 사용하고, z3는 브라우저를 포함한 더 다양한 환경에서 사용 가능하므로, 대부분의 사용자는 이 옵션에 대해 거의 걱정할 필요가 없을 거예요. 더 고급 사용자는 더 복잡한 문제에 대체 솔버를 시도하기 위해 이 옵션을 적용할 수 있어요.

선택된 엔진과 솔버의 특정 조합은 SMTChecker가 아무것도 하지 않게 할 수 있다는 점에 주의해요. 예를 들어 CHC와 cvc5를 선택하는 경우.

추상화와 거짓 양성 (Abstraction and False Positives)

SMTChecker는 추상화를 불완전하고 건전한 방식으로 구현해요. 버그가 보고되면, 추상화(지식 지우기 또는 비정밀 타입 사용)로 도입된 거짓 양성일 수 있어요. 검증 대상이 안전하다고 결정하면 실제로 안전해요. 즉 거짓 음성은 없어요(SMTChecker에 버그가 없는 한). 대상이 증명될 수 없으면 이전 절의 튜닝 옵션을 사용해 솔버를 도울 수 있어요. 거짓 양성이 확실하면, 더 많은 정보를 가진 require 문을 코드에 추가하는 것도 솔버에 더 많은 힘을 줄 수 있어요.

SMT 인코딩과 타입 (SMT Encoding and Types)

SMTChecker 인코딩은 가능한 한 정밀해지려고 노력하며, Solidity 타입과 표현식을 아래 표처럼 가장 가까운 SMT-LIB 표현에 매핑해요.

Solidity 타입	SMT sort	Theories
Boolean	Bool	Bool
intN, uintN, address, bytesN, enum, contract	Integer	LIA, NIA
array, mapping, bytes, string	Tuple (Array elements, Integer length)	Datatypes, Arrays, LIA
struct	Tuple	Datatypes
기타 타입	Integer	LIA

아직 지원되지 않는 타입은 단일 256비트 부호 없는 정수로 추상화되며, 지원되지 않는 연산은 무시된다.

SMT 인코딩이 내부적으로 어떻게 동작하는지에 대한 자세한 내용은 논문 SMT-based Verification of Solidity Smart Contracts를 참고해요.

함수 호출 (Function Calls)

BMC 엔진에서 같은 컨트랙트(또는 기본 컨트랙트)에 대한 함수 호출은 가능할 때, 즉 그 구현이 사용 가능할 때 인라인돼요. 다른 컨트랙트의 함수에 대한 호출은 실제 배포된 코드가 같다는 것을 보장할 수 없으므로 코드가 사용 가능해도 인라인되지 않아요.

CHC 엔진은 호출된 함수의 요약(summary)을 사용해 내부 함수 호출을 지원하는 비선형 Horn 절을 만들어요. 외부 함수 호출은 잠재적 재진입 호출을 포함해 알 수 없는 코드에 대한 호출로 취급돼요.

복잡한 pure 함수는 인자에 대해 해석되지 않은 함수(UF)로 추상화돼요.

함수	BMC/CHC 동작
`assert`	검증 대상.
`require`	가정.
내부 호출	BMC: 함수 호출 인라인. CHC: 함수 요약.
알려진 코드에 대한 외부 호출	BMC: 함수 호출 인라인 또는 상태 변수와 로컬 스토리지 참조에 대한 지식 지우기. CHC: 호출된 코드가 알 수 없다고 가정. 호출 반환 후 유지되는 불변식 추론 시도.
스토리지 배열 push/pop	정밀하게 지원. 빈 배열을 pop하는지 확인.
ABI 함수	UF로 추상화.
`addmod`, `mulmod`	정밀하게 지원.
`gasleft`, `blobhash`, `blockhash`, `keccak256`, `ecrecover`, `ripemd160`	UF로 추상화.
구현 없는 pure 함수(외부 또는 복잡)	UF로 추상화
구현 없는 외부 함수	BMC: 상태 지식 지우기 및 결과가 비결정적이라고 가정. CHC: 비결정적 요약. 호출 반환 후 유지되는 불변식 추론 시도.
`transfer`	BMC: 컨트랙트 잔액이 충분한지 확인. CHC: 아직 확인을 수행하지 않음.
기타	현재 지원되지 않음

추상화를 사용하면 정밀한 지식이 손실되지만, 많은 경우 증명 능력의 손실을 의미하지는 않아요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Recover
{
    function f(
        bytes32 hash,
        uint8 v1, uint8 v2,
        bytes32 r1, bytes32 r2,
        bytes32 s1, bytes32 s2
    ) public pure returns (address) {
        address a1 = ecrecover(hash, v1, r1, s1);
        require(v1 == v2);
        require(r1 == r2);
        require(s1 == s2);
        address a2 = ecrecover(hash, v2, r2, s2);
        assert(a1 == a2);
        return a1;
    }
}

위 예시에서 SMTChecker는 ecrecover을 실제로 계산할 만큼 표현력이 충분하지 않지만, 함수 호출을 해석되지 않은 함수로 모델링함으로써 동등한 매개변수로 호출될 때 반환 값이 같다는 것을 알 수 있어요. 이것은 위 어서션이 항상 참임을 증명하기에 충분해요.

함수 호출을 UF로 추상화하는 것은 결정적이라고 알려진 함수에 대해 할 수 있고, pure 함수에 대해 쉽게 할 수 있어요. 그러나 일반 외부 함수에는 이것을 하기 어려운데, 그것들이 상태 변수에 의존할 수 있기 때문이에요.

참조 타입과 앨리어싱 (Reference Types and Aliasing)

Solidity는 같은 데이터 위치를 가진 참조 타입에 대해 앨리어싱을 구현해요. 이는 한 변수가 같은 데이터 영역에 대한 참조를 통해 수정될 수 있다는 뜻이에요.

SMTChecker는 어느 참조가 같은 데이터를 가리키는지 추적하지 않아요. 이는 로컬 참조나 참조 타입의 상태 변수가 할당될 때마다, 같은 타입과 데이터 위치의 변수에 대한 모든 지식이 지워진다는 뜻이에요. 타입이 중첩되면 지식 제거는 모든 접두사 기본 타입도 포함해요.

open in Remix

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Aliasing
{
    uint[] array1;
    uint[][] array2;
    function f(
        uint[] memory a,
        uint[] memory b,
        uint[][] memory c,
        uint[] storage d
    ) internal {
        array1[0] = 42;
        a[0] = 2;
        c[0][0] = 2;
        b[0] = 1;
        // Erasing knowledge about memory references should not
        // erase knowledge about state variables.
        assert(array1[0] == 42);
        // However, an assignment to a storage reference will erase
        // storage knowledge accordingly.
        d[0] = 2;
        // Fails as false positive because of the assignment above.
        assert(array1[0] == 42);
        // Fails because `a == b` is possible.
        assert(a[0] == 2);
        // Fails because `c[i] == b` is possible.
        assert(c[0][0] == 2);
        assert(d[0] == 2);
        assert(b[0] == 1);
    }
    function g(
        uint[] memory a,
        uint[] memory b,
        uint[][] memory c,
        uint x
    ) public {
        f(a, b, c, array2[x]);
    }
}

b[0]에 대한 할당 후, a에 대한 지식을 지워야 해요. 그것이 같은 타입(uint[])과 데이터 위치(메모리)를 갖기 때문이에요. 또한 c에 대한 지식도 지워야 해요. 그 기본 타입도 메모리에 있는 uint[]이기 때문이에요. 이는 어떤 c[i]가 b나 a와 같은 데이터를 가리킬 수 있다는 것을 암시해요.

array와 d에 대한 지식은 지우지 않는다는 점에 주의해요. 그것들이 스토리지에 있기 때문이에요. 타입이 uint[]인데도요. 그러나 d가 할당되면 array에 대한 지식을 지워야 하고 그 반대도 마찬가지예요.

컨트랙트 잔액 (Contract Balance)

컨트랙트는 배포 트랜잭션에서 msg.value > 0이라면 그와 함께 보내진 자금으로 배포될 수 있어요. 그러나 컨트랙트의 주소는 배포 전에 이미 자금을 가질 수 있고, 그것을 컨트랙트가 유지해요. 따라서 SMTChecker는 EVM 규칙과 일치하도록 생성자에서 address(this).balance >= msg.value라고 가정해요.

컨트랙트의 잔액은 컨트랙트에 대한 어떤 호출도 트리거하지 않고 증가할 수도 있는데, 다음 경우에 그래요:

다른 컨트랙트가 selfdestruct를 실행하며 남은 자금의 대상이 분석된 컨트랙트인 경우,
컨트랙트가 어떤 블록의 coinbase(즉 block.coinbase)인 경우.

이것을 제대로 모델링하기 위해, SMTChecker는 매 새 트랜잭션에서 컨트랙트의 잔액이 최소한 msg.value만큼 성장할 수 있다고 가정해요.

실세계 가정 (Real World Assumptions)

Solidity와 EVM에서 표현할 수 있지만 실제로는 발생할 것으로 기대되지 않는 시나리오가 있어요. 그런 경우 중 하나는 push 중에 동적 스토리지 배열의 길이가 오버플로우하는 것이에요. push 연산이 길이 2^256 - 1의 배열에 적용되면 그 길이가 조용히 오버플로우해요. 그러나 배열을 그 지점까지 키우는 데 필요한 연산은 실행하는 데 수십억 년이 걸리므로 실제로는 발생할 가능성이 낮아요.

SMTChecker가 취하는 또 다른 비슷한 가정은 주소의 잔액이 결코 오버플로우할 수 없다는 것이에요. 비슷한 아이디어가 EIP-1985에 제시됐어요.

SMTChecker와 형식 검증