Chuyển đến nội dung chính

Cách sử dụng Manticore để tìm lỗi trong hợp đồng thông minh

Solidity
hợp đồng thông minh
bảo mật
kiểm thử
xác minh chính thức
Nâng cao
Trailofbits
13 tháng 1, 2020
15 phút đọc
Chỉnh sửa trang (opens in a new tab)

Mục đích của hướng dẫn này là chỉ cho bạn cách sử dụng Manticore để tự động tìm lỗi trong hợp đồng thông minh.

Cài đặt

Manticore yêu cầu >= Python 3.6. Nó có thể được cài đặt thông qua pip hoặc sử dụng Docker.

Manticore thông qua Docker

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

Lệnh cuối cùng chạy eth-security-toolbox trong một Docker có quyền truy cập vào thư mục hiện tại của bạn. Bạn có thể thay đổi các tệp từ máy chủ của mình và chạy các công cụ trên các tệp từ Docker

Bên trong Docker, chạy:

solc-select 0.5.11
cd /home/trufflecon/

Manticore thông qua pip

pip3 install --user manticore

Khuyến nghị sử dụng solc 0.5.11.

Chạy một tập lệnh

Để chạy một tập lệnh Python với Python 3:

python3 script.py

Giới thiệu về thực thi tượng trưng động

Tóm tắt về Thực thi tượng trưng động

Thực thi tượng trưng động (DSE) là một kỹ thuật phân tích chương trình khám phá không gian trạng thái với mức độ nhận thức ngữ nghĩa cao. Kỹ thuật này dựa trên việc khám phá các "đường dẫn chương trình", được biểu diễn dưới dạng các công thức toán học gọi là path predicates. Về mặt khái niệm, kỹ thuật này hoạt động trên các vị từ đường dẫn theo hai bước:

  1. Chúng được xây dựng bằng cách sử dụng các ràng buộc trên đầu vào của chương trình.
  2. Chúng được sử dụng để tạo ra các đầu vào chương trình sẽ khiến các đường dẫn liên quan thực thi.

Cách tiếp cận này không tạo ra kết quả dương tính giả theo nghĩa là tất cả các trạng thái chương trình được xác định đều có thể được kích hoạt trong quá trình thực thi cụ thể. Ví dụ: nếu phân tích tìm thấy một lỗi tràn số nguyên, nó được đảm bảo là có thể tái tạo.

Ví dụ về Vị từ đường dẫn

Để hiểu rõ hơn về cách DSE hoạt động, hãy xem xét ví dụ sau:

function f(uint a){

  if (a == 65) {
      // Có một lỗi hiện diện
  }

}

Vì f() chứa hai đường dẫn, một DSE sẽ xây dựng hai vị từ đường dẫn khác nhau:

  • Đường dẫn 1: a == 65
  • Đường dẫn 2: Not (a == 65)

Mỗi vị từ đường dẫn là một công thức toán học có thể được đưa cho một cái gọi là trình giải quyết SMT (opens in a new tab), nó sẽ cố gắng giải phương trình. Đối với Path 1, trình giải quyết sẽ nói rằng đường dẫn có thể được khám phá với a = 65. Đối với Path 2, trình giải quyết có thể cung cấp cho a bất kỳ giá trị nào khác 65, ví dụ a = 0.

Xác minh các thuộc tính

Manticore cho phép kiểm soát hoàn toàn mọi quá trình thực thi của từng đường dẫn. Do đó, nó cho phép bạn thêm các ràng buộc tùy ý vào hầu hết mọi thứ. Sự kiểm soát này cho phép tạo ra các thuộc tính trên hợp đồng.

Xem xét ví dụ sau:

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // không có bảo vệ tràn số
  return c;
}

Ở đây chỉ có một đường dẫn để khám phá trong hàm:

  • Đường dẫn 1: c = a + b

Sử dụng Manticore, bạn có thể kiểm tra lỗi tràn số và thêm các ràng buộc vào vị từ đường dẫn:

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

Nếu có thể tìm thấy một định giá của a và b mà vị từ đường dẫn ở trên là khả thi, điều đó có nghĩa là bạn đã tìm thấy một lỗi tràn số. Ví dụ: trình giải quyết có thể tạo ra đầu vào a = 10 , b = MAXUINT256.

Nếu bạn xem xét một phiên bản đã được sửa:

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

Công thức liên quan với kiểm tra tràn số sẽ là:

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

Công thức này không thể giải được; nói cách khác, đây là một bằng chứng cho thấy trong safe_add, c sẽ luôn tăng.

Do đó, DSE là một công cụ mạnh mẽ, có thể xác minh các ràng buộc tùy ý trên mã của bạn.

Chạy dưới Manticore

Chúng ta sẽ xem cách khám phá một hợp đồng thông minh với API Manticore. Mục tiêu là hợp đồng thông minh sau example.sol (opens in a new tab):

Chạy một khám phá độc lập

Bạn có thể chạy Manticore trực tiếp trên hợp đồng thông minh bằng lệnh sau (project có thể là một Tệp Solidity hoặc một thư mục dự án):

$ manticore project

Bạn sẽ nhận được đầu ra của các trường hợp kiểm thử giống như thế này (thứ tự có thể thay đổi):

Nếu không có thông tin bổ sung, Manticore sẽ khám phá hợp đồng bằng các giao dịch tượng trưng mới cho đến khi nó không khám phá thêm các đường dẫn mới trên hợp đồng. Manticore không chạy các giao dịch mới sau một giao dịch thất bại (ví dụ: sau một hoàn nguyên).

Manticore sẽ xuất thông tin trong một thư mục mcore_*. Trong số những thứ khác, bạn sẽ tìm thấy trong thư mục này:

  • global.summary: độ bao phủ và cảnh báo của trình biên dịch
  • test_XXXXX.summary: độ bao phủ, lệnh cuối cùng, số dư tài khoản cho mỗi trường hợp kiểm thử
  • test_XXXXX.tx: danh sách chi tiết các giao dịch cho mỗi trường hợp kiểm thử

Ở đây Manticore tìm thấy 7 trường hợp kiểm thử, tương ứng với (thứ tự tên tệp có thể thay đổi):

Giao dịch 0Giao dịch 1Giao dịch 2Kết quả
test_00000000.txTạo hợp đồngf(!=65)f(!=65)STOP
test_00000001.txTạo hợp đồnghàm dự phòngREVERT
test_00000002.txTạo hợp đồngRETURN
test_00000003.txTạo hợp đồngf(65)REVERT
test_00000004.txTạo hợp đồngf(!=65)STOP
test_00000005.txTạo hợp đồngf(!=65)f(65)REVERT
test_00000006.txTạo hợp đồngf(!=65)hàm dự phòngREVERT

Tóm tắt khám phá f(!=65) biểu thị f được gọi với bất kỳ giá trị nào khác 65.

Như bạn có thể nhận thấy, Manticore tạo ra một trường hợp kiểm thử duy nhất cho mỗi giao dịch thành công hoặc bị hoàn nguyên.

Sử dụng cờ --quick-mode nếu bạn muốn khám phá mã nhanh (nó vô hiệu hóa các trình phát hiện lỗi, tính toán Gas, ...)

Thao tác với một hợp đồng thông minh thông qua API

Phần này mô tả chi tiết cách thao tác với một hợp đồng thông minh thông qua API Python của Manticore. Bạn có thể tạo tệp mới với phần mở rộng Python *.py và viết mã cần thiết bằng cách thêm các lệnh API (những lệnh cơ bản sẽ được mô tả bên dưới) vào tệp này và sau đó chạy nó bằng lệnh $ python3 *.py. Bạn cũng có thể thực thi các lệnh bên dưới trực tiếp vào bảng điều khiển Python, để chạy bảng điều khiển, hãy sử dụng lệnh $ python3.

Tạo Tài khoản

Điều đầu tiên bạn nên làm là khởi tạo một chuỗi khối mới bằng các lệnh sau:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

Một tài khoản không phải hợp đồng được tạo bằng cách sử dụng m.create_account (opens in a new tab):

user_account = m.create_account(balance=1000)

Một hợp đồng Solidity có thể được triển khai bằng cách sử dụng m.solidity_create_contract (opens in a new tab):

Tóm tắt

Thực thi các giao dịch

Manticore hỗ trợ hai loại giao dịch:

  • Giao dịch thô: tất cả các hàm đều được khám phá
  • Giao dịch có tên: chỉ một hàm được khám phá

Giao dịch thô

Một giao dịch thô được thực thi bằng cách sử dụng m.transaction (opens in a new tab):

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

Người gọi, địa chỉ, dữ liệu hoặc giá trị của giao dịch có thể là cụ thể hoặc tượng trưng:

Ví dụ:

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)

Nếu dữ liệu là tượng trưng, Manticore sẽ khám phá tất cả các hàm của hợp đồng trong quá trình thực thi giao dịch. Sẽ rất hữu ích khi xem giải thích về Hàm dự phòng trong bài viết Thực hành với Ethernaut CTF (opens in a new tab) để hiểu cách hoạt động của việc chọn hàm.

Giao dịch có tên

Các hàm có thể được thực thi thông qua tên của chúng. Để thực thi f(uint var) với một giá trị tượng trưng, từ user_account và với 0 ether, hãy sử dụng:

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

Nếu value của giao dịch không được chỉ định, nó mặc định là 0.

Tóm tắt

  • Các đối số của một giao dịch có thể là cụ thể hoặc tượng trưng
  • Một giao dịch thô sẽ khám phá tất cả các hàm
  • Hàm có thể được gọi bằng tên của chúng

Không gian làm việc

m.workspace là thư mục được sử dụng làm thư mục đầu ra cho tất cả các tệp được tạo:

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

Chấm dứt Khám phá

Để dừng khám phá, hãy sử dụng m.finalize() (opens in a new tab). Không có giao dịch nào khác được gửi sau khi phương thức này được gọi và Manticore tạo ra các trường hợp kiểm thử cho mỗi đường dẫn được khám phá.

Tóm tắt: Chạy dưới Manticore

Kết hợp tất cả các bước trước đó lại với nhau, chúng ta có được:

Tất cả mã ở trên bạn có thể tìm thấy trong example_run.py (opens in a new tab)

Lấy các đường dẫn ném lỗi

Bây giờ chúng ta sẽ tạo các đầu vào cụ thể cho các đường dẫn gây ra ngoại lệ trong f(). Mục tiêu vẫn là hợp đồng thông minh sau 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();
        }
    }
}

Sử dụng thông tin trạng thái

Mỗi đường dẫn được thực thi đều có trạng thái của chuỗi khối. Một trạng thái có thể là sẵn sàng hoặc bị hủy, nghĩa là nó đạt đến lệnh THROW hoặc REVERT:

for state in m.all_states:
    # làm gì đó với trạng thái

Bạn có thể truy cập thông tin trạng thái. Ví dụ:

  • state.platform.get_balance(account.address): số dư của tài khoản
  • state.platform.transactions: danh sách các giao dịch
  • state.platform.transactions[-1].return_data: dữ liệu được trả về bởi giao dịch cuối cùng

Dữ liệu được trả về bởi giao dịch cuối cùng là một mảng, có thể được chuyển đổi thành một giá trị bằng ABI.deserialize, ví dụ:

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

Cách tạo trường hợp kiểm thử

Sử dụng m.generate_testcase(state, name) (opens in a new tab) để tạo trường hợp kiểm thử:

m.generate_testcase(state, 'BugFound')

Tóm tắt

  • Bạn có thể lặp qua trạng thái bằng m.all_states
  • state.platform.get_balance(account.address) trả về số dư của tài khoản
  • state.platform.transactions trả về danh sách các giao dịch
  • transaction.return_data là dữ liệu được trả về
  • m.generate_testcase(state, name) tạo đầu vào cho trạng thái

Tóm tắt: Lấy Đường dẫn ném lỗi

Tất cả mã ở trên bạn có thể tìm thấy trong example_run.py (opens in a new tab)

Lưu ý rằng chúng ta có thể đã tạo một tập lệnh đơn giản hơn nhiều, vì tất cả các trạng thái được trả về bởi terminated_state đều có REVERT hoặc INVALID trong kết quả của chúng: ví dụ này chỉ nhằm mục đích chứng minh cách thao tác với API.

Thêm các ràng buộc

Chúng ta sẽ xem cách ràng buộc việc khám phá. Chúng ta sẽ giả định rằng tài liệu của f() tuyên bố rằng hàm không bao giờ được gọi với a == 65, vì vậy bất kỳ lỗi nào với a == 65 đều không phải là lỗi thực sự. Mục tiêu vẫn là hợp đồng thông minh sau 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();
        }
    }
}

Toán tử

Mô-đun Toán tử (opens in a new tab) tạo điều kiện thuận lợi cho việc thao tác với các ràng buộc, trong số những thứ khác, nó cung cấp:

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT (lớn hơn không dấu),
  • Operators.UGE (lớn hơn hoặc bằng không dấu),
  • Operators.ULT (nhỏ hơn không dấu),
  • Operators.ULE (nhỏ hơn hoặc bằng không dấu).

Để nhập mô-đun, hãy sử dụng lệnh sau:

from manticore.core.smtlib import Operators

Operators.CONCAT được sử dụng để nối một mảng với một giá trị. Ví dụ: return_data của một giao dịch cần được thay đổi thành một giá trị để kiểm tra với một giá trị khác:

last_return = Operators.CONCAT(256, *last_return)

Các ràng buộc

Bạn có thể sử dụng các ràng buộc trên toàn cục hoặc cho một trạng thái cụ thể.

Ràng buộc toàn cục

Sử dụng m.constrain(constraint) để thêm một ràng buộc toàn cục. Ví dụ: bạn có thể gọi một hợp đồng từ một địa chỉ tượng trưng và giới hạn địa chỉ này thành các giá trị cụ thể:

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)

Ràng buộc trạng thái

Sử dụng state.constrain(constraint) (opens in a new tab) để thêm một ràng buộc vào một trạng thái cụ thể. Nó có thể được sử dụng để ràng buộc trạng thái sau khi khám phá để kiểm tra một số thuộc tính trên đó.

Kiểm tra Ràng buộc

Sử dụng solver.check(state.constraints) để biết liệu một ràng buộc có còn khả thi hay không. Ví dụ: đoạn mã sau sẽ ràng buộc symbolic_value khác 65 và kiểm tra xem trạng thái có còn khả thi hay không:

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # trạng thái là khả thi

Tóm tắt: Thêm các Ràng buộc

Thêm ràng buộc vào mã trước đó, chúng ta có được:

Tất cả mã ở trên bạn có thể tìm thấy trong example_run.py (opens in a new tab)

Cập nhật trang lần cuối: 3 tháng 4, 2026

lukassiml (opens in a new tab)
nhszn (opens in a new tab)
rex4539r (opens in a new tab)
+6