Kiểm toán hợp đồng thông minh

Hợp đồng thông minh là một loại phần mềm khác thường. Chúng trực tiếp nắm giữ tiền, chạy công khai để ai cũng có thể nghiên cứu, và một khi đã triển khai thì khó hoặc không thể thay đổi. Một dòng mã bị bỏ sót có thể cho phép kẻ tấn công rút cạn một giao thức chỉ trong một giao dịch. Kiểm toán là tuyến phòng thủ chính trước khi ra mắt: các chuyên gia đọc mã trước khi kẻ tấn công kịp đọc.

Kiểm toán viên tìm kiếm điều gì

• Lỗi logic: mã làm đúng như nó viết nhưng không đúng như dự định, chẳng hạn một công thức phần thưởng trả hai lần.
• Kiểm soát truy cập: những hàm ai cũng gọi được trong khi lẽ ra chỉ quản trị viên mới được gọi.
• Reentrancy (tái nhập): một lệnh gọi ra bên ngoài cho phép kẻ tấn công quay lại một hàm trước khi lệnh gọi đầu tiên kết thúc, lỗi đứng sau vụ tấn công The DAO năm 2016.
• Thao túng giá: logic tin vào một mức giá có thể bị dịch chuyển trong một giao dịch, thường thông qua một oracle yếu.
• Thiết kế kinh tế: các cơ chế khuyến khích mà một bên có nhiều vốn có thể lợi dụng ngay cả khi từng dòng mã chạy đúng như viết.

Kiểm toán viên kết hợp rà soát thủ công với công cụ tự động và, ngày càng nhiều, xác minh hình thức (formal verification), phương pháp chứng minh bằng toán học rằng mã đáp ứng một đặc tả đã viết.

Hai mô hình kiểm toán

Trong một cuộc kiểm toán truyền thống của công ty kiểm toán, một nhóm nhỏ kỹ sư bảo mật nghiên cứu bộ mã trong một khoảng thời gian cố định và giao một báo cáo. Trong một cuộc kiểm toán cạnh tranh, nhiều nhà nghiên cứu độc lập cùng lúc rà soát cùng một bộ mã và được trả tiền theo các vấn đề họ tìm ra. Hai mô hình thường phát hiện những thứ khác nhau, nên các giao thức thường dùng cả hai.

Cách đọc báo cáo kiểm toán

Bắt đầu với phạm vi: những hợp đồng nào, phiên bản mã nào và những ngày nào. Một cuộc kiểm toán phiên bản một nói rất ít về phiên bản hai. Sau đó đọc các phát hiện theo mức độ nghiêm trọng. Phát hiện mức nghiêm trọng (critical) và cao có thể dẫn đến mất tiền; mức trung bình thường cần những điều kiện cụ thể; mức thấp và mức thông tin liên quan đến vệ sinh mã. Với mỗi phát hiện, hãy kiểm tra xem nó được đánh dấu đã sửa, đã ghi nhận hay đang tranh luận, và bản sửa có được rà soát lại hay không.

Ví dụ đơn giản

Một báo cáo liệt kê một phát hiện mức cao: một lỗi làm tròn cho phép người dùng rút ra nhiều hơn một chút so với số đã đưa vào, và lặp lại qua hàng nghìn giao dịch có thể rút cạn một vault. Nhóm phát triển sửa lỗi trước khi ra mắt và kiểm toán viên xác nhận bản sửa. Không ai bên ngoài biết đến lỗi đó. Đó là một cuộc kiểm toán làm đúng việc của nó, và là lý do phần phát hiện quan trọng hơn logo trên trang bìa.

Rủi ro và giới hạn

Một cuộc kiểm toán là một ảnh chụp tại một thời điểm. Mã thay đổi sau đợt rà soát, các hợp đồng mới tương tác với nó và kỹ thuật tấn công ngày càng tinh vi. Một số vụ khai thác DeFi gây thiệt hại lớn đã nhắm vào các giao thức đã được kiểm toán, thường qua phần mã nằm ngoài phạm vi hoặc qua cách nhiều giao thức tương tác với nhau. Kiểm toán cũng không thể đánh giá các phần offchain của hệ thống, chẳng hạn cách quản lý khóa hay dự trữ gồm những gì. Đó là lý do kiểm toán hữu ích nhất khi là một lớp trong nhiều lớp: một chương trình bug bounty tiếp tục trả thưởng cho nhà nghiên cứu sau khi ra mắt, giám sát runtime theo dõi các giao dịch đang diễn ra, và bằng chứng dự trữ cho chính các tài sản.

Các hợp đồng thông minh của Tori Finance được kiểm toán bởi Sherlock và Nethermind. Kiểm toán là một lớp trong hệ thống bảo mật của Tori Finance, cùng với giám sát runtime của Hypernative và bằng chứng dự trữ của Accountable.