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