Cách sử dụng Echidna để kiểm thử hợp đồng thông minh

Cài đặt

Echidna có thể được cài đặt thông qua docker hoặc sử dụng tệp nhị phân đã biên dịch trước.

Echidna 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 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/training

Nhị phân

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

Giới thiệu về fuzzing dựa trên thuộc tính

Echidna là một fuzzer dựa trên thuộc tính, chúng tôi đã mô tả trong các bài đăng blog trước đây của chúng tôi (1 (opens in a new tab), 2 (opens in a new tab), 3 (opens in a new tab)).

Fuzzing

Fuzzing (opens in a new tab) là một kỹ thuật nổi tiếng trong cộng đồng bảo mật. Nó bao gồm việc tạo ra các đầu vào ít nhiều ngẫu nhiên để tìm lỗi trong chương trình. Các fuzzer cho phần mềm truyền thống (chẳng hạn như AFL (opens in a new tab) hoặc LibFuzzer (opens in a new tab)) được biết đến là những công cụ hiệu quả để tìm lỗi.

Ngoài việc tạo ra các đầu vào hoàn toàn ngẫu nhiên, có nhiều kỹ thuật và chiến lược để tạo ra các đầu vào tốt, bao gồm:

• Nhận phản hồi từ mỗi lần thực thi và sử dụng nó để định hướng cho việc tạo. Ví dụ, nếu một đầu vào mới được tạo dẫn đến việc phát hiện ra một đường dẫn mới, việc tạo ra các đầu vào mới gần với nó có thể là hợp lý.
• Tạo đầu vào tôn trọng một ràng buộc cấu trúc. Ví dụ, nếu đầu vào của bạn chứa một tiêu đề có tổng kiểm, sẽ hợp lý nếu để fuzzer tạo ra đầu vào xác thực tổng kiểm.
• Sử dụng các đầu vào đã biết để tạo các đầu vào mới: nếu bạn có quyền truy cập vào một bộ dữ liệu lớn gồm các đầu vào hợp lệ, fuzzer của bạn có thể tạo các đầu vào mới từ chúng, thay vì bắt đầu tạo từ đầu. Chúng thường được gọi là seeds.

Fuzzing dựa trên thuộc tính

Echidna thuộc về một họ fuzzer cụ thể: fuzzing dựa trên thuộc tính lấy cảm hứng nhiều từ QuickCheck (opens in a new tab). Trái ngược với fuzzer cổ điển sẽ cố gắng tìm các sự cố, Echidna sẽ cố gắng phá vỡ các bất biến do người dùng định nghĩa.

Trong các hợp đồng thông minh, các bất biến là các hàm Solidity, có thể đại diện cho bất kỳ trạng thái không chính xác hoặc không hợp lệ nào mà hợp đồng có thể đạt tới, bao gồm:

• Kiểm soát truy cập không chính xác: kẻ tấn công đã trở thành chủ sở hữu của hợp đồng.
• Máy trạng thái không chính xác: các token có thể được chuyển trong khi hợp đồng bị tạm dừng.
• Số học không chính xác: người dùng có thể làm tràn dưới số dư của họ và nhận được token miễn phí không giới hạn.

Kiểm thử một thuộc tính với Echidna

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

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
Hiện tất cả
Sao chép

Chúng ta sẽ giả định rằng token này phải có các thuộc tính sau:

• Bất kỳ ai cũng có thể có tối đa 1000 token
• Token không thể được chuyển (nó không phải là một token ERC20)

Viết một thuộc tính

Các thuộc tính của Echidna là các hàm Solidity. Một thuộc tính phải:

• Không có đối số
• Trả về true nếu nó thành công
• Có tên bắt đầu bằng echidna

Echidna sẽ:

• Tự động tạo các giao dịch tùy ý để kiểm thử thuộc tính.
• Báo cáo bất kỳ giao dịch nào dẫn đến việc một thuộc tính trả về false hoặc phát sinh lỗi.
• Loại bỏ tác dụng phụ khi gọi một thuộc tính (tức là, nếu thuộc tính thay đổi một biến trạng thái, nó sẽ bị loại bỏ sau khi kiểm thử)

Thuộc tính sau đây kiểm tra rằng người gọi không có nhiều hơn 1000 token:

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}
Sao chép

Sử dụng tính kế thừa để tách hợp đồng của bạn ra khỏi các thuộc tính của bạn:

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }
Sao chép

token.sol (opens in a new tab) triển khai thuộc tính và kế thừa từ token.

Khởi tạo một hợp đồng

Echidna cần một hàm khởi tạo không có đối số. Nếu hợp đồng của bạn cần một khởi tạo cụ thể, bạn cần thực hiện nó trong hàm khởi tạo.

Có một số địa chỉ cụ thể trong Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 gọi hàm khởi tạo.
• 0x10000, 0x20000, và 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 gọi ngẫu nhiên các hàm khác.

Chúng ta không cần bất kỳ khởi tạo cụ thể nào trong ví dụ hiện tại của mình, do đó hàm khởi tạo của chúng ta trống.

Chạy Echidna

Echidna được khởi chạy với:

echidna-test contract.sol

Nếu contract.sol chứa nhiều hợp đồng, bạn có thể chỉ định mục tiêu:

echidna-test contract.sol --contract MyContract

Tóm tắt: Kiểm thử một thuộc tính

Phần sau đây tóm tắt việc chạy echidna trên ví dụ của chúng ta:

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }
Sao chép

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Hiện tất cả

Echidna đã phát hiện ra rằng thuộc tính bị vi phạm nếu backdoor được gọi.

Lọc các hàm để gọi trong một chiến dịch fuzzing

Chúng ta sẽ xem cách lọc các hàm sẽ được fuzz. Mục tiêu là hợp đồng thông minh sau:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
Hiện tất cả
Sao chép

Ví dụ nhỏ này buộc Echidna phải tìm một chuỗi giao dịch nhất định để thay đổi một biến trạng thái. Điều này khó đối với một fuzzer (khuyến nghị sử dụng một công cụ thực thi tượng trưng như Manticore (opens in a new tab)). Chúng ta có thể chạy Echidna để xác minh điều này:

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

Lọc hàm

Echidna gặp khó khăn trong việc tìm ra trình tự chính xác để kiểm thử hợp đồng này bởi vì hai hàm đặt lại (reset1 và reset2) sẽ đặt tất cả các biến trạng thái thành false. Tuy nhiên, chúng ta có thể sử dụng một tính năng đặc biệt của Echidna để đưa hàm đặt lại vào danh sách đen hoặc chỉ đưa các hàm f, g, h và i vào danh sách trắng.

Để đưa các hàm vào danh sách đen, chúng ta có thể sử dụng tệp cấu hình này:

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

Một cách tiếp cận khác để lọc các hàm là liệt kê các hàm trong danh sách trắng. Để làm điều đó, chúng ta có thể sử dụng tệp cấu hình này:

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

• filterBlacklist là true theo mặc định.
• Việc lọc sẽ chỉ được thực hiện theo tên (không có tham số). Nếu bạn có f() và f(uint256), bộ lọc "f" sẽ khớp với cả hai hàm.

Chạy Echidna

Để chạy Echidna với một tệp cấu hình blacklist.yaml:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

Echidna sẽ tìm thấy chuỗi giao dịch để làm sai thuộc tính gần như ngay lập tức.

Tóm tắt: Lọc hàm

Echidna có thể đưa các hàm vào danh sách đen hoặc danh sách trắng để gọi trong một chiến dịch fuzzing bằng cách sử dụng:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

Echidna bắt đầu một chiến dịch fuzzing hoặc bằng cách đưa f1, f2 và f3 vào danh sách đen hoặc chỉ gọi chúng, tùy thuộc vào giá trị của boolean filterBlacklist.

Cách kiểm thử khẳng định của Solidity với Echidna

Trong hướng dẫn ngắn này, chúng ta sẽ chỉ ra cách sử dụng Echidna để kiểm thử việc kiểm tra khẳng định trong các hợp đồng. Giả sử chúng ta có một hợp đồng như thế này:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
Hiện tất cả
Sao chép

Viết một khẳng định

Chúng ta muốn đảm bảo rằng tmp nhỏ hơn hoặc bằng counter sau khi trả về hiệu của chúng. Chúng ta có thể viết một thuộc tính Echidna, nhưng chúng ta sẽ cần lưu trữ giá trị tmp ở đâu đó. Thay vào đó, chúng ta có thể sử dụng một khẳng định như thế này:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Hiện tất cả
Sao chép

Chạy Echidna

Để bật kiểm thử lỗi khẳng định, tạo một tệp cấu hình Echidna (opens in a new tab) config.yaml:

1checkAsserts: true

Khi chúng ta chạy hợp đồng này trong Echidna, chúng ta nhận được kết quả mong đợi:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Hiện tất cả

Như bạn có thể thấy, Echidna báo cáo một số lỗi khẳng định trong hàm inc. Có thể thêm nhiều hơn một khẳng định cho mỗi hàm, nhưng Echidna không thể cho biết khẳng định nào đã thất bại.

Khi nào và cách sử dụng các khẳng định

Các khẳng định có thể được sử dụng như là các phương án thay thế cho các thuộc tính rõ ràng, đặc biệt là nếu các điều kiện cần kiểm tra có liên quan trực tiếp đến việc sử dụng đúng một số hoạt động f. Việc thêm các khẳng định sau một đoạn mã sẽ buộc việc kiểm tra phải diễn ra ngay sau khi nó được thực thi:

1function f(..) public {
2    // một số mã phức tạp
3    ...
4    assert (condition);
5    ...
6}
7
Sao chép

Ngược lại, việc sử dụng một thuộc tính echidna rõ ràng sẽ thực thi các giao dịch một cách ngẫu nhiên và không có cách nào dễ dàng để buộc chính xác khi nào nó sẽ được kiểm tra. Vẫn có thể thực hiện giải pháp này:

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}
Sao chép

Tuy nhiên, có một số vấn đề:

• Nó sẽ thất bại nếu f được khai báo là internal hoặc external.
• Không rõ nên sử dụng đối số nào để gọi f.
• Nếu f hoàn lại, thuộc tính sẽ thất bại.

Nhìn chung, chúng tôi khuyên bạn nên làm theo khuyến nghị của John Regehr (opens in a new tab) về cách sử dụng các khẳng định:

• Không ép buộc bất kỳ tác dụng phụ nào trong quá trình kiểm tra khẳng định. Ví dụ: assert(ChangeStateAndReturn() == 1)
• Đừng khẳng định những câu lệnh hiển nhiên. Ví dụ assert(var >= 0) trong đó var được khai báo là uint.

Cuối cùng, vui lòng không sử dụng require thay vì assert, vì Echidna sẽ không thể phát hiện ra nó (nhưng hợp đồng dù sao cũng sẽ hoàn lại).

Tóm tắt: Kiểm tra Khẳng định

Phần sau đây tóm tắt việc chạy echidna trên ví dụ của chúng ta:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Hiện tất cả
Sao chép

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Hiện tất cả

Echidna đã phát hiện ra rằng khẳng định trong inc có thể thất bại nếu hàm này được gọi nhiều lần với các đối số lớn.

Thu thập và sửa đổi một kho văn bản Echidna

Chúng ta sẽ xem cách thu thập và sử dụng một kho văn bản giao dịch với Echidna. Mục tiêu là hợp đồng thông minh sau magic.sol (opens in a new tab):

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
Hiện tất cả
Sao chép

Ví dụ nhỏ này buộc Echidna phải tìm các giá trị nhất định để thay đổi một biến trạng thái. Điều này khó đối với một fuzzer (khuyến nghị sử dụng một công cụ thực thi tượng trưng như Manticore (opens in a new tab)). Chúng ta có thể chạy Echidna để xác minh điều này:

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
Seed: 2221503356319272685

Tuy nhiên, chúng ta vẫn có thể sử dụng Echidna để thu thập kho văn bản khi chạy chiến dịch fuzzing này.

Thu thập một kho văn bản

Để bật thu thập kho văn bản, tạo một thư mục kho văn bản:

mkdir corpus-magic

Và một tệp cấu hình Echidna (opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

Bây giờ chúng ta có thể chạy công cụ của mình và kiểm tra kho văn bản đã thu thập:

echidna-test magic.sol --config config.yaml

Echidna vẫn không thể tìm thấy các giá trị magic chính xác, nhưng chúng ta có thể xem kho văn bản mà nó đã thu thập. Ví dụ, một trong những tệp này là:

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
Hiện tất cả
Sao chép

Rõ ràng, đầu vào này sẽ không kích hoạt sự thất bại trong thuộc tính của chúng ta. Tuy nhiên, trong bước tiếp theo, chúng ta sẽ xem cách sửa đổi nó cho mục đích đó.

Gieo mầm một kho văn bản

Echidna cần một số trợ giúp để xử lý hàm magic. Chúng ta sẽ sao chép và sửa đổi đầu vào để sử dụng các tham số phù hợp cho nó:

cp corpus/2712688662897926208.txt corpus/new.txt

Chúng ta sẽ sửa đổi new.txt để gọi magic(42,129,333,0). Bây giờ, chúng ta có thể chạy lại Echidna:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
Hiện tất cả

Lần này, nó đã phát hiện ra rằng thuộc tính bị vi phạm ngay lập tức.

Tìm các giao dịch có mức tiêu thụ gas cao

Chúng ta sẽ xem cách tìm các giao dịch có mức tiêu thụ gas cao với Echidna. Mục tiêu là hợp đồng thông minh sau:

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
Hiện tất cả
Sao chép

Ở đây expensive có thể có mức tiêu thụ gas lớn.

Hiện tại, Echidna luôn cần một thuộc tính để kiểm thử: ở đây echidna_test luôn trả về true. Chúng ta có thể chạy Echidna để xác minh điều này:

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

Đo lường mức tiêu thụ gas

Để bật tính năng đo lường mức tiêu thụ gas với Echidna, tạo một tệp cấu hình config.yaml:

1estimateGas: true

Trong ví dụ này, chúng ta cũng sẽ giảm kích thước của chuỗi giao dịch để làm cho kết quả dễ hiểu hơn:

1seqLen: 2
2estimateGas: true

Chạy Echidna

Sau khi chúng ta đã tạo tệp cấu hình, chúng ta có thể chạy Echidna như thế này:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
Hiện tất cả

• Lượng gas được hiển thị là một ước tính được cung cấp bởi HEVM (opens in a new tab).

Lọc ra các lệnh gọi giảm gas

Hướng dẫn về lọc các hàm để gọi trong một chiến dịch fuzzing ở trên chỉ ra cách loại bỏ một số hàm khỏi quá trình kiểm thử của bạn.
Điều này có thể rất quan trọng để có được ước tính gas chính xác. Hãy xem xét ví dụ sau:

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
Hiện tất cả
Sao chép

Nếu Echidna có thể gọi tất cả các hàm, nó sẽ không dễ dàng tìm thấy các giao dịch có chi phí gas cao:

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
Hiện tất cả

Đó là bởi vì chi phí phụ thuộc vào kích thước của addrs và các lệnh gọi ngẫu nhiên có xu hướng để lại mảng gần như trống rỗng. Tuy nhiên, việc đưa pop và clear vào danh sách đen cho chúng ta kết quả tốt hơn nhiều:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

Tóm tắt: Tìm các giao dịch có mức tiêu thụ gas cao

Echidna có thể tìm thấy các giao dịch có mức tiêu thụ gas cao bằng cách sử dụng tùy chọn cấu hình estimateGas:

1estimateGas: true

echidna-test contract.sol --config config.yaml
...

Echidna sẽ báo cáo một chuỗi có mức tiêu thụ gas tối đa cho mọi hàm, sau khi chiến dịch fuzzing kết thúc.

Lần cập nhật trang lần cuối: 21 tháng 10, 2025

p (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+8

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