본문으로 건너뛰기

스마트 컨트랙트에서 버그를 찾기 위해 맨티코어(Manticore)를 사용하는 방법

Solidity
스마트 컨트랙트
보안
테스트
정형 검증
고급
트레일오브비츠
2020년 1월 13일
21 분 소요

이 튜토리얼의 목적은 맨티코어를 사용하여 스마트 컨트랙트에서 자동으로 버그를 찾는 방법을 보여주는 것입니다.

설치

맨티코어는 Python 3.6 이상이 필요합니다. pip를 통해 설치하거나 Docker를 사용하여 설치할 수 있습니다.

Docker를 통한 맨티코어 설치

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

마지막 명령어는 현재 디렉터리에 접근할 수 있는 Docker 내에서 eth-security-toolbox를 실행합니다. 호스트에서 파일을 변경하고 Docker에서 해당 파일에 대해 도구를 실행할 수 있습니다.

Docker 내부에서 다음을 실행하세요.

solc-select 0.5.11
cd /home/trufflecon/

pip를 통한 맨티코어 설치

pip3 install --user manticore

solc 0.5.11 버전을 권장합니다.

스크립트 실행

Python 3으로 Python 스크립트를 실행하려면:

python3 script.py

동적 심볼릭 실행 소개

동적 심볼릭 실행 요약

동적 심볼릭 실행(Dynamic symbolic execution, DSE)은 높은 수준의 의미론적 인식을 바탕으로 상태 공간을 탐색하는 프로그램 분석 기법입니다. 이 기법은 path predicates라고 불리는 수학적 공식으로 표현되는 "프로그램 경로"의 디스커버리를 기반으로 합니다. 개념적으로 이 기법은 두 단계로 경로 조건식(path predicates)에 대해 작동합니다.

  1. 프로그램의 입력에 대한 제약 조건을 사용하여 구성됩니다.
  2. 연관된 경로가 실행되도록 하는 프로그램 입력을 생성하는 데 사용됩니다.

이 접근 방식은 식별된 모든 프로그램 상태가 구체적인 실행 중에 트리거될 수 있다는 점에서 오탐(false positive)을 생성하지 않습니다. 예를 들어, 분석에서 정수 오버플로를 발견하면 이는 반드시 재현 가능함이 보장됩니다.

경로 조건식 예시

DSE가 어떻게 작동하는지 이해하기 위해 다음 예시를 살펴보겠습니다.

function f(uint a){

  if (a == 65) {
      // 버그가 존재합니다
  }

}

f()에는 두 개의 경로가 포함되어 있으므로, DSE는 두 개의 서로 다른 경로 조건식을 구성합니다.

  • 경로 1: a == 65
  • 경로 2: Not (a == 65)

각 경로 조건식은 이른바 SMT 솔버 (opens in a new tab)에 전달될 수 있는 수학적 공식이며, 솔버는 이 방정식을 풀려고 시도합니다. Path 1의 경우, 솔버는 a = 65를 사용하여 경로를 탐색할 수 있다고 알려줍니다. Path 2의 경우, 솔버는 a에 65가 아닌 임의의 값(예: a = 0)을 부여할 수 있습니다.

속성 검증

맨티코어는 각 경로의 모든 실행에 대한 완전한 제어를 허용합니다. 결과적으로 거의 모든 것에 임의의 제약 조건을 추가할 수 있습니다. 이러한 제어를 통해 컨트랙트에 대한 속성을 생성할 수 있습니다.

다음 예시를 살펴보겠습니다.

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // 오버플로 보호 없음
  return c;
}

여기 함수에서 탐색할 경로는 단 하나뿐입니다.

  • 경로 1: c = a + b

맨티코어를 사용하면 오버플로를 확인하고 경로 조건식에 제약 조건을 추가할 수 있습니다.

  • c = a + b AND (c < a OR c < b)

위의 경로 조건식이 실현 가능한 a 및 b의 값을 찾을 수 있다면, 이는 오버플로를 발견했음을 의미합니다. 예를 들어 솔버는 a = 10 , b = MAXUINT256라는 입력을 생성할 수 있습니다.

수정된 버전을 고려해 보겠습니다.

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

오버플로 검사가 포함된 연관 공식은 다음과 같습니다.

  • c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

이 공식은 풀 수 없습니다. 다시 말해 이는 safe_add에서 c가 항상 증가한다는 증명입니다.

따라서 DSE는 코드에 대한 임의의 제약 조건을 검증할 수 있는 강력한 도구입니다.

맨티코어에서 실행하기

맨티코어 API를 사용하여 스마트 컨트랙트를 탐색하는 방법을 알아보겠습니다. 대상은 다음 스마트 컨트랙트인 example.sol (opens in a new tab)입니다.

독립 실행형 탐색 실행

다음 명령어를 사용하여 스마트 컨트랙트에서 직접 맨티코어를 실행할 수 있습니다(project는 Solidity 파일이거나 프로젝트 디렉터리일 수 있습니다).

$ manticore project

다음과 같은 테스트 케이스 출력을 얻게 됩니다(순서는 변경될 수 있음).

추가 정보가 없으면 맨티코어는 컨트랙트에서 새로운 경로를 탐색하지 않을 때까지 새로운 심볼릭 트랜잭션으로 컨트랙트를 탐색합니다. 맨티코어는 실패한 트랜잭션(예: 되돌리기 이후) 이후에는 새로운 트랜잭션을 실행하지 않습니다.

맨티코어는 mcore_* 디렉터리에 정보를 출력합니다. 이 디렉터리에서 다음을 찾을 수 있습니다.

  • global.summary: 커버리지 및 컴파일러 경고
  • test_XXXXX.summary: 테스트 케이스별 커버리지, 마지막 명령어, 계정 잔액
  • test_XXXXX.tx: 테스트 케이스별 상세 트랜잭션 목록

여기서 맨티코어는 7개의 테스트 케이스를 찾았으며, 이는 다음과 같습니다(파일 이름 순서는 변경될 수 있음).

트랜잭션 0트랜잭션 1트랜잭션 2결과
test_00000000.tx컨트랙트 생성f(!=65)f(!=65)STOP
test_00000001.tx컨트랙트 생성폴백 함수REVERT
test_00000002.tx컨트랙트 생성RETURN
test_00000003.tx컨트랙트 생성f(65)REVERT
test_00000004.tx컨트랙트 생성f(!=65)STOP
test_00000005.tx컨트랙트 생성f(!=65)f(65)REVERT
test_00000006.tx컨트랙트 생성f(!=65)폴백 함수REVERT

탐색 요약에서 f(!=65)는 65가 아닌 임의의 값으로 호출된 f를 나타냅니다.

보시다시피 맨티코어는 성공하거나 되돌리기된 모든 트랜잭션에 대해 고유한 테스트 케이스를 생성합니다.

빠른 코드 탐색을 원한다면 --quick-mode 플래그를 사용하세요(버그 탐지기, 가스 계산 등을 비활성화합니다).

API를 통해 스마트 컨트랙트 조작하기

이 섹션에서는 맨티코어 Python API를 통해 스마트 컨트랙트를 조작하는 방법에 대해 자세히 설명합니다. Python 확장자인 *.py로 새 파일을 생성하고 이 파일에 API 명령어(기본 사항은 아래에 설명됨)를 추가하여 필요한 코드를 작성한 다음, $ python3 *.py 명령어로 실행할 수 있습니다. 또한 아래 명령어들을 Python 콘솔에서 직접 실행할 수도 있으며, 콘솔을 실행하려면 $ python3 명령어를 사용합니다.

계정 생성

가장 먼저 해야 할 일은 다음 명령어를 사용하여 새로운 블록체인을 초기화하는 것입니다.

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

컨트랙트 계정이 아닌 일반 계정은 m.create_account (opens in a new tab)를 사용하여 생성됩니다.

user_account = m.create_account(balance=1000)

Solidity 컨트랙트는 m.solidity_create_contract (opens in a new tab)를 사용하여 배포할 수 있습니다.

요약

트랜잭션 실행

맨티코어는 두 가지 유형의 트랜잭션을 지원합니다.

  • 원시(Raw) 트랜잭션: 모든 함수가 탐색됩니다.
  • 명명된(Named) 트랜잭션: 하나의 함수만 탐색됩니다.

원시 트랜잭션

원시 트랜잭션은 m.transaction (opens in a new tab)을 사용하여 실행됩니다.

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

트랜잭션의 호출자, 주소, 데이터 또는 값은 구체적이거나 심볼릭일 수 있습니다.

예를 들어:

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              value=symbolic_value)

데이터가 심볼릭인 경우, 맨티코어는 트랜잭션 실행 중에 컨트랙트의 모든 함수를 탐색합니다. 함수 선택이 어떻게 작동하는지 이해하려면 Ethernaut CTF 실습 (opens in a new tab) 문서의 폴백 함수 설명을 참조하는 것이 도움이 될 것입니다.

명명된 트랜잭션

함수는 이름을 통해 실행될 수 있습니다. user_account에서 0 이더(ether)와 심볼릭 값으로 f(uint var)를 실행하려면 다음을 사용하세요.

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)

트랜잭션의 value가 지정되지 않은 경우 기본값은 0입니다.

요약

  • 트랜잭션의 인수는 구체적이거나 심볼릭일 수 있습니다.
  • 원시 트랜잭션은 모든 함수를 탐색합니다.
  • 함수는 이름으로 호출될 수 있습니다.

작업 공간(Workspace)

m.workspace는 생성된 모든 파일의 출력 디렉터리로 사용되는 디렉터리입니다.

print("Results are in {}".format(m.workspace))

탐색 종료

탐색을 중지하려면 m.finalize() (opens in a new tab)를 사용하세요. 이 메서드가 호출되면 더 이상 트랜잭션이 전송되지 않으며, 맨티코어는 탐색된 각 경로에 대한 테스트 케이스를 생성합니다.

요약: 맨티코어에서 실행하기

이전의 모든 단계를 종합하면 다음과 같습니다.

위의 모든 코드는 example_run.py (opens in a new tab)에서 찾을 수 있습니다.

예외 발생 경로 가져오기

이제 f()에서 예외를 발생시키는 경로에 대한 특정 입력을 생성해 보겠습니다. 대상은 여전히 다음 스마트 컨트랙트인 example.sol (opens in a new tab)입니다.

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

상태 정보 사용

실행된 각 경로는 블록체인의 상태를 가집니다. 상태는 준비(ready) 상태이거나 종료(killed) 상태이며, 종료 상태는 THROW 또는 REVERT 명령어에 도달했음을 의미합니다.

for state in m.all_states:
    # 상태로 무언가를 수행합니다

상태 정보에 접근할 수 있습니다. 예를 들어:

  • state.platform.get_balance(account.address): 계정의 잔액
  • state.platform.transactions: 트랜잭션 목록
  • state.platform.transactions[-1].return_data: 마지막 트랜잭션에서 반환된 데이터

마지막 트랜잭션에서 반환된 데이터는 배열이며, 예를 들어 ABI.deserialize를 사용하여 값으로 변환할 수 있습니다.

data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint", data)

테스트 케이스 생성 방법

테스트 케이스를 생성하려면 m.generate_testcase(state, name) (opens in a new tab)를 사용하세요.

m.generate_testcase(state, 'BugFound')

요약

  • m.all_states를 사용하여 상태를 반복할 수 있습니다.
  • state.platform.get_balance(account.address)는 계정의 잔액을 반환합니다.
  • state.platform.transactions는 트랜잭션 목록을 반환합니다.
  • transaction.return_data는 반환된 데이터입니다.
  • m.generate_testcase(state, name)는 상태에 대한 입력을 생성합니다.

요약: 예외 발생 경로 가져오기

위의 모든 코드는 example_run.py (opens in a new tab)에서 찾을 수 있습니다.

참고로 terminated_state가 반환하는 모든 상태는 결과에 REVERT 또는 INVALID를 가지므로 훨씬 더 간단한 스크립트를 생성할 수도 있었습니다. 이 예시는 API를 조작하는 방법을 보여주기 위한 목적으로만 작성되었습니다.

제약 조건 추가

탐색을 제한하는 방법을 알아보겠습니다. f()의 문서에 이 함수가 a == 65로 호출되지 않는다고 명시되어 있다고 가정해 보겠습니다. 따라서 a == 65와 관련된 버그는 실제 버그가 아닙니다. 대상은 여전히 다음 스마트 컨트랙트인 example.sol (opens in a new tab)입니다.

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

연산자(Operators)

Operators (opens in a new tab) 모듈은 제약 조건의 조작을 용이하게 하며, 특히 다음을 제공합니다.

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT (부호 없는 큼),
  • Operators.UGE (부호 없는 크거나 같음),
  • Operators.ULT (부호 없는 작음),
  • Operators.ULE (부호 없는 작거나 같음).

모듈을 가져오려면 다음을 사용하세요.

from manticore.core.smtlib import Operators

Operators.CONCAT는 배열을 값에 연결하는 데 사용됩니다. 예를 들어, 트랜잭션의 return_data를 다른 값과 비교하여 확인하려면 값으로 변경해야 합니다.

last_return = Operators.CONCAT(256, *last_return)

제약 조건

제약 조건은 전역적으로 사용하거나 특정 상태에 대해 사용할 수 있습니다.

전역 제약 조건

전역 제약 조건을 추가하려면 m.constrain(constraint)를 사용하세요. 예를 들어, 심볼릭 주소에서 컨트랙트를 호출하고 이 주소가 특정 값이 되도록 제한할 수 있습니다.

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

상태 제약 조건

특정 상태에 제약 조건을 추가하려면 state.constrain(constraint) (opens in a new tab)를 사용하세요. 탐색 후 상태를 제한하여 해당 상태의 일부 속성을 확인하는 데 사용할 수 있습니다.

제약 조건 확인

제약 조건이 여전히 실현 가능한지 확인하려면 solver.check(state.constraints)를 사용하세요. 예를 들어, 다음은 symbolic_value가 65와 다르도록 제한하고 상태가 여전히 실현 가능한지 확인합니다.

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # 상태가 실현 가능합니다

요약: 제약 조건 추가

이전 코드에 제약 조건을 추가하면 다음과 같습니다.

위의 모든 코드는 example_run.py (opens in a new tab)에서 찾을 수 있습니다.