Formal verification hợp đồng thông minh là gì
Nội dung bài9 phần
Độ khó: Nâng cao
Kiểm thử chạy mã với vài trăm đầu vào mẫu rồi thấy "không lỗi". Formal verification hỏi khác: có đầu vào nào làm mã sai không, trên toàn bộ đầu vào có thể. Cách này dùng toán học để chứng minh một tính chất luôn đúng.
Bài giải thích bằng ví dụ số, không cần nền toán. Nội dung chỉ nhằm giải thích kiến thức, không phải khuyến nghị đầu tư.
Điểm chính
- Formal verification kiểm tra mã theo một đặc tả viết bằng logic, không chỉ chạy thử.
- Chứng minh được bao nhiêu thì tuỳ đặc tả: đặc tả thiếu thì lỗi vẫn lọt.
- Ba kỹ thuật chính: model checking, theorem proving, symbolic execution.
- Nó đắt và cần chuyên gia, nên thường dùng cho phần lõi giữ tiền.
Khác kiểm thử và kiểm toán
Kiểm thử | Kiểm toán | Formal verification | |
|---|---|---|---|
Cách làm | Chạy mã với đầu vào mẫu | Chuyên gia đọc mã | Chứng minh tính chất bằng logic |
Chứng minh được | Có lỗi ở đầu vào đã thử | Không chứng minh | Tính chất đúng với mọi đầu vào, trong phạm vi đặc tả |
Chi phí | Thấp | Trung bình | Cao, cần kỹ năng chuyên sâu |
Ethereum.org nhận xét kiểm thử có thể lộ lỗi nhưng không chứng minh được là hết lỗi. Phần kiểm toán nằm ở bài kiểm toán hợp đồng thông minh.
Ví dụ số: cộng tràn số
Giả sử một biến chỉ chứa số từ 0 đến 255 (8 bit). Hàm cong(a, b) cộng hai số mà không kiểm tra tràn.
Thử 3 + 4 = 7, đúng. Thử 10 + 20 = 30, đúng.
Nhưng 200 + 100 = 300, vượt 255, nên máy quay vòng và trả về 44 (300 trừ 256). Kiểm thử ngẫu nhiên có thể bỏ sót trường hợp này. Với formal verification, ta viết đặc tả "kết quả luôn bằng a + b hoặc hàm báo lỗi", và công cụ tìm ra ngay cặp (200, 100) làm đặc tả sai.
Đặc tả: viết điều gì phải luôn đúng
Đặc tả là danh sách tính chất của hợp đồng. Ethereum.org chia thành hai nhóm:
- Tính an toàn (safety): điều xấu không bao giờ xảy ra. Ví dụ: chuyển token thì số dư người gửi không bao giờ âm.
- Tính sống còn (liveness): điều tốt rồi sẽ xảy ra. Ví dụ: người đã gửi tiền luôn rút được.
Sự cố ví đa chữ ký Parity là ví dụ cho liveness: Ethereum.org ghi hơn 300 triệu USD ETH bị khoá vĩnh viễn, tức người dùng không còn rút được tiền của mình.
Ba kỹ thuật chính
Kỹ thuật | Cách làm | Điểm mạnh | Điểm yếu |
|---|---|---|---|
Model checking | Thuật toán duyệt các trạng thái của hợp đồng để kiểm tính chất | Tự động | Số trạng thái bùng nổ nên phải đơn giản hoá |
Theorem proving | Biến mã và đặc tả thành mệnh đề logic rồi chứng minh | Xử lý được hệ thống vô hạn trạng thái | Cần người dẫn dắt, tốn kém |
Symbolic execution | Chạy mã với đầu vào "ký hiệu" rồi nhờ bộ giải tìm giá trị cụ thể đi tới một nhánh | Tìm được đầu vào gây lỗi | Số nhánh bùng nổ |
Ethereum.org liệt kê công cụ như Certora Prover, Solidity SMTChecker, solc-verify và KEVM cho kiểm chứng chương trình; Mythril, hevm và Manticore cho symbolic execution.
Ví dụ: tính chất K của Uranium
Một sàn hoán đổi kiểu Uniswap cần giữ một bất biến: sau mỗi lần hoán đổi, tích hai số dư (đã trừ phí) không được nhỏ hơn tích trước đó. Đây là tính chất an toàn điển hình.
Trong vụ Uranium Finance ngày 28/04/2021, theo Immunefi, hệ số phí đổi sang 10000 nhưng phép so sánh vẫn dùng 1000, nên phép kiểm tra lỏng hơn 100 lần và hơn 50 triệu USD bị lấy trên 26 cặp.
Về nguyên tắc, nếu tính chất trên được viết thành đặc tả và chứng minh đúng trên phiên bản mã đó, mã có hằng số lệch sẽ không qua được. Đây là ví dụ minh hoạ cho loại tính chất mà phương pháp này kiểm tra, không khẳng định công cụ cụ thể nào đã dùng trong vụ việc.
Giới hạn cần biết
- Đặc tả sai hoặc thiếu thì lỗi vẫn lọt. Ethereum.org gọi đây là nguy cơ âm tính giả: công cụ chỉ kiểm mã có khớp đặc tả hay không.
- Đắt và cần kỹ năng. Tốn nhiều công sức thủ công, đắt hơn kiểm thử hay kiểm toán.
- Có tính chất không chứng minh được. Bùng nổ trạng thái, bộ giải nặng và tính không quyết định có thể khiến vài tính chất không kết luận được.
- Chỉ đúng với phiên bản mã đã chứng minh. Sửa mã là phải chứng minh lại.
- Không phủ phần ngoài chuỗi, như khoá quản trị, máy chủ hay giao diện. Rủi ro cầu nối, nơi phần ngoài chuỗi hay hỏng, có ở bài lỗ hổng bảo mật cầu nối.
Cách làm: đọc tuyên bố kiểm chứng
- Hỏi tính chất nào đã được chứng minh. Đừng chấp nhận câu "đã chứng minh toàn bộ".
- Hỏi phiên bản mã nào, so với mã đang chạy trên chuỗi.
- Xem đặc tả có công khai không. Đặc tả kín thì không đánh giá được.
- Xem dự án có kết hợp kiểm toán và bug bounty không; các lớp này bổ sung cho nhau.
- Nhớ mã dùng cho tiền còn dính tới ví và khoá, không chỉ hợp đồng.
Học tiếp trong khoá Crypto
Các bài học liên quan trong Khoá học Crypto của HODL.VN:
Câu hỏi thường gặp
Formal verification có thay được kiểm toán không?
Không. Nó chứng minh các tính chất đã viết, còn kiểm toán nhìn bức tranh rộng hơn như logic kinh tế và cách vận hành. Hai cách bổ sung cho nhau.
Hợp đồng đã formal verification thì không bị hack?
Không đảm bảo. Nếu đặc tả bỏ sót một tính chất quan trọng, lỗi tương ứng vẫn lọt.
Vì sao ít dự án dùng?
Vì tốn kém và cần chuyên gia hiếm. Thường chỉ phần lõi giữ nhiều tiền mới đáng đầu tư.
Khác gì kiểm thử thông thường?
Kiểm thử thử một số đầu vào; formal verification chứng minh tính chất cho mọi đầu vào trong phạm vi đặc tả.
Người dùng phổ thông có cần hiểu sâu?
Không cần. Chỉ cần biết hỏi: chứng minh tính chất nào, trên phiên bản nào.
Duyệt bởi Ban biên tập HODL.VN · Cập nhật 09/11/2026
Ứng dụng HODL
Tải app HODL
Bảng giá, cảnh báo giá và bài phân tích ngay trên điện thoại.
