Bài viết này là một đóng góp từ cộng đồng. Tác giả là David Tarditi, Phó Giám đốc Kỹ thuật tại CertiK, một công ty kiểm định hợp đồng thông minh trên Web3.
TL;DR
Kiểm định chính thức là quy trình kiểm định nhằm đảm bảo hợp đồng thông minh không có lỗi, lỗ hổng bảo mật và hành vi ngoài ý muốn khác. Quy trình này liên quan đến việc một là chuyên gia là con người trình bày logic của hợp đồng thông minh dưới dạng các câu lệnh toán học, sau đó vận hành chúng thông qua một quy trình tự động để kiểm tra logic thực tế dựa trên các mô hình hành vi dự kiến của hợp đồng. Sự kết hợp giữa kiểm định chính thức và kiểm định thủ công sẽ cung cấp đánh giá toàn diện về tính bảo mật của hợp đồng thông minh.
Giới thiệu
Hợp đồng thông minh là các chương trình được lưu trữ trên blockchain dùng để thực thi một tác vụ khi một số điều kiện nhất định được đáp ứng. Chúng có thể đơn giản hoặc cực kỳ phức tạp và có thể nắm giữ tài sản trị giá hàng triệu, thậm chí hàng tỷ USD.
Các lỗ hổng bảo mật trong mã hợp đồng thông minh có thể gây ra những hậu quả nghiêm trọng, bao gồm cả việc đánh cắp tất cả tài sản được nắm giữ bởi một hợp đồng thông minh. Vào năm 2021, Uranium Finance, một công cụ tạo thị trường tự động (AMM) đã bị đánh cắp 50 triệu USD chỉ vì một lỗi đánh máy trong hợp đồng thông minh.
Cũng trong năm 2021, Compound Finance đã trao sai 80 triệu USD tiền thưởng được chỉ vì một lỗi ký tự. Vào năm 2022, 320 triệu USD đã bị đánh cắp khỏi Cầu Wormhole do lỗi đến từ một trong các hợp đồng thông minh của nó.
Việc hợp đồng thông minh đúng ngay từ ban đầu rất quan trọng. Hợp đồng thông minh là mã nguồn mở, nghĩa là code được cung cấp công khai sau khi hợp đồng được triển khai. Nếu một hacker tìm thấy một lỗi, họ có thể tận dụng nó ngay lập tức. Ngoài ra, việc vá các lỗ hổng bảo mật theo thời gian không phải là một lựa chọn, vì code của hợp đồng thông minh thường không thể được sửa sau khi được triển khai.
Việc kiểm định hợp đồng thông minh diễn ra như thế nào?
Việc kiểm định chính thức hợp đồng thông minh diễn ra bằng cách trình bày logic và hành vi mong muốn của hợp đồng thông minh dưới dạng các câu lệnh toán học. Sau đó, các kiểm định viên sử dụng các công cụ tự động để kiểm tra xem những tuyên bố này có chính xác hay không.
Quá trình này bao gồm:
Xác định các thông số kỹ thuật và các thuộc tính mong muốn của một hợp đồng bằng ngôn ngữ chính thức.
Dịch code của hợp đồng thành một hình thức hiển thị chính thức, chẳng hạn như các mô hình toán học hoặc logic.
Sử dụng trình chứng minh định lý tự động hoặc trình kiểm tra mô hình để xác thực các thông số kỹ thuật và thuộc tính của hợp đồng.
Lặp lại quy trình kiểm định để tìm và sửa bất kỳ lỗi hoặc sai lệch nào so với các thuộc tính mong muốn.
Tại sao việc kiểm định hợp đồng thông minh lại quan trọng
Việc sử dụng lý luận toán học giúp đảm bảo rằng các hợp đồng thông minh được kiểm định chính thức không có lỗi, lỗ hổng bảo mật và hành vi ngoài ý muốn khác. Nó cũng giúp tăng niềm tin và sự tự tin trong hợp đồng, vì các thuộc tính của nó đã được chứng minh một cách chặt chẽ là đúng.
Dưới đây là một số ví dụ về cách kiểm định lại hợp đồng thông minh đã giúp ngăn ngừa tổn thất tài chính đáng kể và các hậu quả tai hại khác.
Uniswap
Uniswap là một AMM nổi tiếng. Khi hợp đồng thông minh Uniswap V1 được phát triển, nó đã được thực hiện việc kiểm định chính thức. Trước khi phát hành, quy trình kiểm định chính thức này đã phát hiện và sửa các lỗi làm tròn số có thể dẫn đến việc Uniswap V1 bị cạn kiệt tiền.
Balancer
Balancer V2 cũng là một AMM đã được kiểm định chính thức. Việc kiểm định chính thức đã tìm thấy và sửa lỗi tính phí không chính xác liên quan đến chức năng cho vay nhanh trong hợp đồng thông minh, điều này có thể khiến sàn giao dịch này dễ dàng bị đánh cắp.
SafeMoon
SafeMoon V1 chứa một lỗi tinh vi được tìm thấy bằng cách kiểm định chính thức sau khi nó được triển khai. Chủ sở hữu có thể từ bỏ quyền sở hữu hợp đồng và sau đó yêu cầu lại hợp đồng nếu một số hoạt động nhất định đã được thực hiện trước khi từ bỏ quyền sở hữu.
Lỗi này đã bị bỏ qua trong hầu hết các lần kiểm tra thủ công các nhánh SafeMoon V1 vì việc tìm ra lỗi này yêu cầu phân tích các kết hợp cụ thể của các giá trị biến chương trình. Đây là thứ mà con người dễ bỏ sót và máy móc dễ dàng nhận ra.
Cách kiểm định chính thức và kiểm định thủ công kết hợp với nhau
Kiểm định chính thức cung cấp một cách có hệ thống và tự động để kiểm tra logic và hành vi của hợp đồng đối với các thuộc tính mong muốn của nó. Điều này giúp dễ dàng xác định và sửa bất kỳ lỗi hoặc lỗi tiềm ẩn nào. Nó đặc biệt hữu ích cho việc tìm kiếm các vấn đề phức tạp và tế nhị có thể khó phát hiện thông qua kiểm tra thủ công.
Kiểm định thủ công liên quan đến việc chuyên gia xem xét code, thiết kế và triển khai của hợp đồng. Kiểm toán viên sử dụng kinh nghiệm và chuyên môn của họ để xác định các rủi ro bảo mật và đánh giá tình trạng bảo mật tổng thể của hợp đồng. Họ cũng có thể xác nhận rằng quy trình kiểm định chính thức đã được thực hiện chính xác và kiểm tra mọi vấn đề có thể không phát hiện được bằng các công cụ tự động.
Việc kết hợp kiểm định chính thức và kiểm định thủ công mang lại sự đánh giá toàn diện và kỹ lưỡng về tính bảo mật của hợp đồng thông minh. Điều này làm tăng cơ hội tìm và sửa bất kỳ lỗ hổng nào. Kết quả là một cách tiếp cận chuyên sâu về bảo mật, tận dụng các khả năng độc đáo của cả con người và máy móc.
Tổng kết
Để đảm bảo tính bảo mật của hợp đồng thông minh, điều cần thiết là sử dụng cả kiểm định chính thức và kiểm định thủ công để đảm bảo đánh giá toàn diện và kỹ lưỡng về tình trạng bảo mật của hợp đồng thông minh.
Mặc dù việc kiểm định chính thức có thể tốn nhiều nguồn lực, nhưng đây là một khoản đầu tư đáng giá cho các hợp đồng có giá trị cao hoặc các yếu tố rủi ro cao. Tóm lại, việc ưu tiên bảo mật và đảm bảo các hợp đồng thông minh không có lỗi, lỗ hổng bảo mật và hành vi ngoài ý muốn là rất quan trọng.
Đọc thêm:
Tuyên bố miễn trừ trách nhiệm và Cảnh báo rủi ro: Nội dung này được trình bày cho bạn trên cơ sở “nguyên trạng”, chỉ là các thông tin chung và với mục đích giáo dục, không đại diện hay bảo đảm cho bạn dưới bất kỳ hình thức nào. Bài viết này không nên được hiểu là lời khuyên tài chính, cũng như không nhằm mục đích đề xuất cho việc mua bất kỳ sản phẩm hoặc dịch vụ cụ thể nào. Giá tài sản kỹ thuật số có thể biến động mạnh. Giá trị khoản đầu tư của bạn có thể giảm hoặc tăng và có thể bạn sẽ không nhận lại được số tiền đã đầu tư. Bạn hoàn toàn chịu trách nhiệm về các quyết định đầu tư của mình và Binance Academy không chịu trách nhiệm pháp lý cho bất kỳ tổn thất nào bạn có thể phải chịu. Đây không phải lời khuyên tài chính.