Hướng dẫn về các công cụ bảo mật hợp đồng thông minh

Chúng ta sẽ sử dụng ba kỹ thuật kiểm thử và phân tích chương trình đặc biệt:

• Phân tích tĩnh bằng Slither. Tất cả các đường dẫn của chương trình đều được ước tính và phân tích cùng lúc, thông qua các bản trình bày chương trình khác nhau (ví dụ: biểu đồ luồng điều khiển)
• Thử nghiệm mờ bằng Echidna. Mã được thực thi với việc tạo các giao dịch giả ngẫu nhiên. Trình thử nghiệm mờ sẽ cố gắng tìm một chuỗi các giao dịch để vi phạm một thuộc tính nhất định.
• Thực thi tượng trưng bằng Manticore. Một kỹ thuật xác minh chính thức, giúp dịch từng đường dẫn thực thi sang một công thức toán học, trên đó các ràng buộc có thể được kiểm tra.

Mỗi kỹ thuật đều có ưu và nhược điểm, và sẽ hữu ích trong các trường hợp cụ thể:

* nếu tất cả các đường dẫn được khám phá mà không hết thời gian

Slither phân tích các hợp đồng trong vòng vài giây, tuy nhiên, phân tích tĩnh có thể dẫn đến các cảnh báo sai và sẽ kém phù hợp hơn cho các kiểm tra phức tạp (ví dụ: kiểm tra số học). Chạy Slither thông qua Giao diện Lập trình Ứng dụng (API) để truy cập bằng một nút nhấn vào các trình phát hiện được tích hợp sẵn hoặc thông qua Giao diện Lập trình Ứng dụng (API) để kiểm tra do người dùng xác định.

Echidna cần chạy trong vài phút và sẽ chỉ tạo ra các kết quả dương tính thực. Echidna kiểm tra các thuộc tính bảo mật do người dùng cung cấp, được viết bằng Solidity. Nó có thể bỏ sót lỗi vì nó dựa trên thăm dò ngẫu nhiên.

Manticore thực hiện phân tích \ Giống như Echidna, Manticore xác minh các thuộc tính do người dùng cung cấp. Nó sẽ cần nhiều thời gian hơn để chạy, nhưng nó có thể chứng minh tính hợp lệ của một thuộc tính và sẽ không báo cáo các cảnh báo sai.

Quy trình làm việc được đề xuất

Bắt đầu với các trình phát hiện tích hợp sẵn của Slither để đảm bảo không có lỗi đơn giản nào hiện có hoặc sẽ được đưa vào sau này. Sử dụng Slither để kiểm tra các thuộc tính liên quan đến tính kế thừa, sự phụ thuộc của biến và các vấn đề về cấu trúc. Khi cơ sở mã phát triển, hãy sử dụng Echidna để kiểm tra các thuộc tính phức tạp hơn của máy trạng thái. Xem lại Slither để phát triển các kiểm tra tùy chỉnh cho các biện pháp bảo vệ không có sẵn từ Solidity, chẳng hạn như bảo vệ chống lại một hàm bị ghi đè. Cuối cùng, sử dụng Manticore để thực hiện xác minh có mục tiêu các thuộc tính bảo mật quan trọng, ví dụ như các phép toán số học.

• Sử dụng CLI của Slither để phát hiện các sự cố thường gặp
• Sử dụng Echidna để kiểm tra các thuộc tính bảo mật cấp cao của hợp đồng của bạn
• Sử dụng Slither để viết các kiểm tra tĩnh tùy chỉnh
• Sử dụng Manticore khi bạn muốn đảm bảo chuyên sâu về các thuộc tính bảo mật quan trọng

Lưu ý về kiểm thử đơn vị. Kiểm thử đơn vị là cần thiết để xây dựng phần mềm chất lượng cao. Tuy nhiên, những kỹ thuật này không phải là phù hợp nhất để tìm ra các lỗ hổng bảo mật. Chúng thường được sử dụng để kiểm tra các hành vi tích cực của mã (tức là mã hoạt động như mong đợi trong bối cảnh bình thường), trong khi các lỗ hổng bảo mật có xu hướng nằm ở các trường hợp cạnh mà các nhà phát triển không xem xét. Trong nghiên cứu của chúng tôi về hàng chục bài đánh giá bảo mật hợp đồng thông minh, phạm vi kiểm thử đơn vị không ảnh hưởng đến số lượng hoặc mức độ nghiêm trọng của các lỗ hổng bảo mật (opens in a new tab) mà chúng tôi tìm thấy trong mã của khách hàng.

Xác định các thuộc tính bảo mật

Để kiểm tra và xác minh mã của bạn một cách hiệu quả, bạn phải xác định các khu vực cần chú ý. Vì tài nguyên dành cho bảo mật của bạn có hạn, việc xác định phạm vi các phần yếu hoặc có giá trị cao trong cơ sở mã của bạn là rất quan trọng để tối ưu hóa nỗ lực của bạn. Lập mô hình mối đe dọa có thể giúp ích. Hãy cân nhắc xem xét:

• Đánh giá rủi ro nhanh (opens in a new tab) (phương pháp ưa thích của chúng tôi khi thời gian eo hẹp)
• Hướng dẫn về Lập mô hình mối đe dọa hệ thống tập trung vào dữ liệu (opens in a new tab) (còn gọi là NIST 800-154)
• Lập mô hình mối đe dọa Shostack (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Sử dụng các khẳng định (opens in a new tab)

Các thành phần

Biết những gì bạn muốn kiểm tra cũng sẽ giúp bạn chọn đúng công cụ.

Các lĩnh vực rộng thường liên quan đến hợp đồng thông minh bao gồm:

• Máy trạng thái. Hầu hết các hợp đồng có thể được biểu diễn dưới dạng một máy trạng thái. Hãy cân nhắc kiểm tra rằng (1) Không thể đạt được trạng thái không hợp lệ, (2) nếu một trạng thái hợp lệ thì nó có thể đạt được, và (3) không có trạng thái nào bẫy hợp đồng.

  • Echidna và Manticore là những công cụ được ưu tiên để kiểm tra các đặc tả máy trạng thái.

• Kiểm soát truy cập. Nếu hệ thống của bạn có người dùng đặc quyền (ví dụ: chủ sở hữu, người điều khiển, ...) bạn phải đảm bảo rằng (1) mỗi người dùng chỉ có thể thực hiện các hành động được ủy quyền và (2) không người dùng nào có thể chặn các hành động của người dùng có đặc quyền cao hơn.

  • Slither, Echidna và Manticore có thể kiểm tra các kiểm soát truy cập chính xác. Ví dụ: Slither có thể kiểm tra rằng chỉ các hàm trong danh sách trắng mới thiếu công cụ sửa đổi onlyOwner. Echidna và Manticore rất hữu ích cho việc kiểm soát truy cập phức tạp hơn, chẳng hạn như quyền chỉ được cấp nếu hợp đồng đạt đến một trạng thái nhất định.

• Các phép toán số học. Việc kiểm tra tính hợp lý của các phép toán số học là rất quan trọng. Sử dụng SafeMath ở mọi nơi là một bước tốt để ngăn chặn tràn số/tràn số dưới, tuy nhiên, bạn vẫn phải xem xét các sai sót số học khác, bao gồm các vấn đề làm tròn và các sai sót bẫy hợp đồng.

  • Manticore là lựa chọn tốt nhất ở đây. Echidna có thể được sử dụng nếu phép toán số học nằm ngoài phạm vi của trình giải SMT.

• Tính đúng đắn của kế thừa. Các hợp đồng Solidity phụ thuộc nhiều vào đa kế thừa. Các lỗi như hàm che bóng thiếu lệnh gọi super và thứ tự tuyến tính hóa c3 bị diễn giải sai có thể dễ dàng được đưa vào.

  • Slither là công cụ để đảm bảo phát hiện các vấn đề này.

• Tương tác bên ngoài. Các hợp đồng tương tác với nhau và không nên tin cậy một số hợp đồng bên ngoài. Ví dụ: nếu hợp đồng của bạn dựa vào các oracle bên ngoài, nó có còn bảo mật không nếu một nửa số oracle có sẵn bị xâm phạm?

  • Manticore và Echidna là lựa chọn tốt nhất để kiểm tra các tương tác bên ngoài với hợp đồng của bạn. Manticore có một cơ chế tích hợp để sơ khai các hợp đồng bên ngoài.

• Tuân thủ tiêu chuẩn. Các tiêu chuẩn Ethereum (ví dụ: ERC20) có lịch sử về các sai sót trong thiết kế của chúng. Hãy nhận thức được những hạn chế của tiêu chuẩn mà bạn đang xây dựng.

  • Slither, Echidna và Manticore sẽ giúp bạn phát hiện các sai lệch so với một tiêu chuẩn nhất định.

Bảng tra cứu nhanh lựa chọn công cụ

Các lĩnh vực khác sẽ cần được kiểm tra tùy thuộc vào mục tiêu của bạn, nhưng những lĩnh vực tập trung bao quát này là một khởi đầu tốt cho bất kỳ hệ thống hợp đồng thông minh nào.

Các cuộc kiểm tra công khai của chúng tôi chứa các ví dụ về các thuộc tính đã được xác minh hoặc thử nghiệm. Hãy cân nhắc đọc các phần Kiểm thử và xác minh tự động của các báo cáo sau để xem xét các thuộc tính bảo mật trong thế giới thực:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)

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

p (opens in a new tab)

m (opens in a new tab)

c (opens in a new tab)

+9

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