Cách sử dụng Manticore để phát hiện lỗi trong hợp đồng thông minh

Mục đích của hướng dẫn này là chỉ ra 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 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 tệp từ máy chủ lưu trữ của mình và chạy các công cụ trên tệp từ docker

Bên trong docker, chạy:

solc-select 0.5.11
cd /home/trufflecon/

Manticore qua pip

pip3 install --user manticore

Nên dùng solc 0.5.11.

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

Để chạy một tập lệnh python bằng python 3:

python3 script.py

Giới thiệu về thực thi ký hiệu động

Thực thi ký hiệu động một cách ngắn gọn

Thực thi ký hiệu độ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à vị từ đường dẫn. 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 của chương trình sẽ khiến các đường dẫn liên quan thực thi.

Phương pháp 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 có thể tái tạo được.

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:

1function f(uint a){
2
3  if (a == 65) {
4      // Có một lỗi
5  }
6
7}
Sao chép

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à bộ giải SMT (opens in a new tab), nó sẽ cố gắng giải phương trình. Đối với Đường dẫn 1, bộ giải sẽ cho biết rằng đường dẫn có thể được khám phá với a = 65. Đối với Đường dẫn 2, bộ giải có thể gán cho a bất kỳ giá trị nào khác ngoài 65, ví dụ a = 0.

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

Manticore cho phép toàn quyền kiểm soát tất cả việc thực thi của mỗi đườ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ứ. Kiểm soát này cho phép tạo ra các thuộc tính trên hợp đồng.

Hãy xem xét ví dụ sau:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // không có bảo vệ chống tràn
3  return c;
4}
Sao chép

Ở đâ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ụ: bộ giải 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 đã sửa lỗi:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
Sao chép

Công thức liên quan với kiểm tra lỗi 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 Giao diện Lập trình Ứng dụng Manticore. Mục tiêu là hợp đồng thông minh sau đây example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Hiện tất cả
Sao chép

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à 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ử như sau (thứ tự có thể thay đổi):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Hiện tất cả

Nếu không có thông tin bổ sung, Manticore sẽ khám phá hợp đồng với các giao dịch ký hiệu mới cho đến khi nó không khám phá được 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 không thành công (ví dụ: sau một lệnh revert).

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):

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 lại.

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 bộ phát hiện lỗi, tính toán gas, ...)

Thao tác một hợp đồng thông minh thông qua Giao diện Lập trình Ứng dụng

Phần này mô tả chi tiết cách thao tác một hợp đồng thông minh thông qua Giao diện Lập trình Ứng dụng 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 Giao diện Lập trình Ứng dụng (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. Ngoài ra, bạn 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

Việc đầ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:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Sao chép

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

1user_account = m.create_account(balance=1000)
Sao chép

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):

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Khởi tạo hợp đồng
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Hiện tất cả
Sao chép

Tóm tắt

• Bạn có thể tạo tài khoản người dùng và tài khoản hợp đồng với m.create_account (opens in a new tab) và m.solidity_create_contract (opens in a new tab).

Thực thi giao dịch

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

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

Giao dịch thô

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

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Sao chép

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 ký hiệu:

• m.make_symbolic_value (opens in a new tab) tạo ra một giá trị ký hiệu.
• m.make_symbolic_buffer(size) (opens in a new tab) tạo một mảng byte ký hiệu.

Ví dụ:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
Sao chép

Nếu dữ liệu là ký hiệu, 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ẽ hữu ích khi xem giải thích về Hàm dự phòng trong bài viết Thực hành Ethernaut CTF (opens in a new tab) để hiểu cách hoạt động của việc lựa chọn hàm.

Giao dịch được đặt 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ị ký hiệu, từ user_account và với 0 ether, hãy sử dụng:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
Sao chép

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

Tóm tắt

• Các đối số của một giao dịch có thể là cụ thể hoặc ký hiệu
• 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:

1print("Results are in {}".format(m.workspace))
Sao chép

Chấm dứt việc khám phá

Để dừng việc khám phá, hãy sử dụng m.finalize() (opens in a new tab). Không nên gửi thêm giao dịch nào sau khi phương thức này được gọi và Manticore tạo 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

Tổng hợp tất cả các bước trước đó, chúng ta có:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # dừng việc khám phá
Hiện tất cả
Sao chép

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 gây 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 đây example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Sao chép

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 riêng của chuỗi khối. Một trạng thái có thể ở trạng thái sẵn sàng hoặc bị hủy, nghĩa là nó đạt đến một lệnh THROW hoặc REVERT:

• m.ready_states (opens in a new tab): danh sách các trạng thái đã sẵn sàng (chúng không thực thi REVERT/INVALID)
• m.killed_states (opens in a new tab): danh sách các trạng thái bị hủy
• m.all_states (opens in a new tab): tất cả các trạng thái

1for state in m.all_states:
2    # làm gì đó với trạng thái
Sao chép

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ụ:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
Sao chép

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ử:

1m.generate_testcase(state, 'BugFound')
Sao chép

Tóm tắt

• Bạn có thể lặp qua trạng thái với 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 gây lỗi

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Kiểm tra xem một lần thực thi có kết thúc bằng REVERT hoặc INVALID không
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Throw found {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Hiện tất cả
Sao chép

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 minh họa cách thao tác Giao diện Lập trình Ứng dụng.

Thêm 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 tham khảo của f() nói rằng hàm không bao giờ được gọi với a == 65, do đó, bất kỳ lỗi nào với a == 65 không phải là một lỗi thực sự. Mục tiêu vẫn là hợp đồng thông minh sau đây example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Sao chép

Toán tử

Mô-đun Toán tử (opens in a new tab) tạo điều kiện cho việc thao tác 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 dòng lệnh sau:

1from manticore.core.smtlib import Operators
Sao chép

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ị để được kiểm tra so với một giá trị khác:

1last_return = Operators.CONCAT(256, *last_return)
Sao chép

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ỉ ký hiệu và giới hạn địa chỉ này ở các giá trị cụ thể:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
Sao chép

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 với 65 và kiểm tra xem trạng thái có còn khả thi không:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # trạng thái là khả thi
Sao chép

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

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

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Kiểm tra xem một lần thực thi có kết thúc bằng REVERT hoặc INVALID không
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # chúng ta không xem xét đường dẫn có a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Đã tìm thấy lỗi, kết quả nằm trong {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Không tìm thấy lỗi nào')
Hiện tất cả
Sao chép

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

Lần cập nhật trang lần cuối: 26 tháng 4, 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+5

Xem những người đóng góp