Làm thế nào AI có thể trao quyền cho bảo mật hợp đồng thông minh? Chia sẻ thực tiễn từ mô hình chung đến mô hình kiểm toán ba lớp
- Quan điểm cốt lõi: Hiện tại, AI trong kiểm toán hợp đồng thông minh có ranh giới năng lực rõ ràng, giỏi quét các mẫu lỗ hổng đã biết, nhưng khó xử lý các lỗ hổng sâu phụ thuộc vào tương tác xuyên hợp đồng và logic nghiệp vụ phức tạp. Do đó, Beosin đã xây dựng mô hình kiểm toán bổ sung ba lớp: "Kiểm tra cơ sở AI được tăng cường kỹ năng + Kiểm toán sâu thủ công + Xác minh hình thức".
- Yếu tố then chốt:
- Khi kiểm toán các hợp đồng token tiêu chuẩn, mô hình AI chung mặc dù có thể xác định các vấn đề về quy chuẩn mã, nhưng do thiếu ngữ cảnh nghiệp vụ, nó thường đánh giá sai các thiết kế dự kiến như quyền đúc token của chủ sở hữu trong các hợp đồng như USDT thành các lỗ hổng nguy hiểm cao.
- Khi kiểm toán các giao thức DeFi phức tạp (như IPC Protocol), AI có tỷ lệ phát hiện thấp đối với các lỗ hổng sâu cần hiểu đường dẫn trạng thái xuyên thành phần (như phát lại chữ ký, tái nhập trạng thái cụ thể) và tỷ lệ báo động sai cao.
- Beosin bằng cách xây dựng cơ sở kiến thức kỹ năng chuyên biệt, đã cấu trúc hóa và đưa kinh nghiệm của chuyên gia kiểm toán vào AI, trong các bài kiểm tra đã nâng tỷ lệ phát hiện lỗ hổng nguy hiểm cao trong hợp đồng phức tạp từ 11% lên 44%, đồng thời giảm tỷ lệ báo động sai từ 55% xuống khoảng 30%.
- Kiểm tra cơ sở AI có thể kết hợp với sách trắng dự án để thực hiện kiểm tra tính nhất quán, giảm hiệu quả các báo động sai do ý đồ thiết kế không rõ ràng, và phát hiện sự sai lệch giữa triển khai mã và cam kết trong tài liệu.
- Kiểm toán thủ công chịu trách nhiệm hiểu sâu cấp độ giao thức và nhận diện các cuộc tấn công mới, trong khi xác minh hình thức cung cấp sự đảm bảo chắc chắn về mặt toán học cho logic nghiệp vụ then chốt. Ba yếu tố này phối hợp cùng nhau xây dựng một hệ thống an toàn hoàn chỉnh.
Nguồn gốc bài viết: Beosin
Trong những năm gần đây, các mô hình ngôn ngữ lớn như GPT-4, Claude, Gemini đã có khả năng hiểu mã mạnh mẽ, có thể đọc tốt các ngôn ngữ hợp đồng thông minh như Solidity, Rust, Go, và cũng có thể nhận diện các lỗ hổng kinh điển có đặc điểm mã rõ ràng như tấn công reentrancy, tràn số nguyên. Điều này khiến ngành công nghiệp bắt đầu suy nghĩ: Liệu có thể sử dụng mô hình lớn để hỗ trợ hoặc thậm chí thay thế con người trong việc kiểm toán hợp đồng không?
Do các mô hình tổng quát thiếu hiểu biết sâu về logic nghiệp vụ của các dự án cụ thể, khi đối mặt với các giao thức DeFi phức tạp, tỷ lệ báo động sai khá cao, và cũng dễ bỏ sót những lỗ hổng chỉ có thể phát hiện được khi kết hợp tương tác xuyên hợp đồng hoặc mô hình kinh tế. Sau này, ngành công nghiệp đã đề xuất phương án thêm cơ chế "Skill" – trên nền tảng mô hình lớn tổng quát, tiêm vào cơ sở kiến thức chuyên sâu về bảo mật hợp đồng thông minh, quy tắc phát hiện và ngữ cảnh nghiệp vụ, giúp mô hình có cơ sở đánh giá rõ ràng hơn khi kiểm toán, thay vì chỉ dựa vào khả năng tổng quát để đánh giá mã có vấn đề hay không.
Ngay cả khi được tăng cường bằng Skill, kiểm toán AI vẫn có phạm vi áp dụng rõ ràng. Nó giỏi trong việc quét các mẫu lỗ hổng đã biết và kiểm tra quy chuẩn mã, nhưng đối với các lỗ hổng phức tạp đòi hỏi hiểu sâu về thiết kế tổng thể giao thức, logic tương tác xuyên hợp đồng hoặc mô hình kinh tế, hiện tại vẫn khó xử lý hiệu quả. Loại vấn đề này vẫn cần các chuyên gia kiểm toán giàu kinh nghiệm phụ trách, và trong các tình huống liên quan đến logic tính toán phức tạp, cần đưa vào xác minh hình thức để cung cấp đảm bảo mạnh mẽ hơn. Trong bối cảnh này, Beosin đã xây dựng mô hình kiểm toán ba lớp: Kiểm tra cơ sở AI tăng cường Skill + Kiểm toán sâu thủ công + Xác minh hình thức, mỗi lớp có trọng tâm riêng và bổ sung cho nhau.

I. Ranh giới năng lực kiểm toán của mô hình AI tổng quát: Kiểm tra đối chứng có kiểm soát và phân tích trường hợp
Bài viết này chọn hai loại hợp đồng có độ phức tạp khác biệt lớn từ kho dự án đã hoàn thành kiểm toán thủ công để làm trường hợp thử nghiệm: một loại là hợp đồng đơn giản có logic tương đối độc lập, ranh giới chức năng rõ ràng, loại dự án này thường là kịch bản mà công cụ kiểm toán AI có dữ liệu huấn luyện dồi dào nhất và về lý thuyết có lợi thế nhất; loại còn lại là hợp đồng phức tạp liên quan đến tương tác đa hợp đồng, máy trạng thái phức tạp hoặc phụ thuộc xuyên giao thức, đây cũng chính là kịch bản rủi ro cao thường được đưa ra thảo luận khi ngành công nghiệp bàn về "AI có thể thay thế kiểm toán thủ công không".
Khi so sánh, chúng tôi sử dụng cùng một kho mã, để AI chạy kiểm toán độc lập trước, sau khi tạo báo cáo thì so sánh từng mục với báo cáo kiểm toán thủ công. Quá trình tạo ra hai báo cáo hoàn toàn không can thiệp lẫn nhau – kiểm toán viên thủ công khi xuất báo cáo hoàn toàn không biết kết quả của AI, tránh ảnh hưởng lẫn nhau. Cuối cùng, chúng tôi sẽ phân tích kết quả từ bốn khía cạnh sau:

Trường hợp A · Hợp đồng token tiêu chuẩn (BSC-USDT / BEP20USDT.sol)
Thử nghiệm đầu tiên, chúng tôi chọn một hợp đồng token BEP-20 tiêu chuẩn, được viết bằng Solidity 0.5.16. Logic của nó tương đối độc lập, ranh giới chức năng rất rõ ràng, không liên quan đến bất kỳ tương tác xuyên hợp đồng nào, rủi ro bảo mật chủ yếu tập trung vào một số mẫu lỗ hổng phổ biến, đã biết. Về lý thuyết, loại hợp đồng này hiện là kịch bản có lợi thế nhất cho kiểm toán AI – có rất nhiều hợp đồng token tiêu chuẩn loại này trong dữ liệu huấn luyện, đặc điểm lỗ hổng mang tính quy tắc cũng khá rõ ràng.

AI xuất ra tổng cộng 6 cảnh báo (2 nguy cơ cao, 1 nguy cơ trung bình, 3 nguy cơ thấp/đề xuất), xét về số lượng khá đáng kể. Các mục nguy cơ thấp và đề xuất về cơ bản chính xác, bao phủ các vấn đề quy chuẩn mã phổ biến như phiên bản Solidity quá cũ, cách thức expose biến trạng thái, có giá trị tham khảo nhất định. Tuy nhiên, hai mục "nguy cơ cao" mà AI xuất ra đều là đánh giá sai. AI đánh dấu quyền mint và tập trung quyền của owner là lỗ hổng nguy cơ cao – thực tế đối với stablecoin tập trung (loại USDT), việc owner có quyền mint thuộc về thiết kế dự kiến, đánh giá rủi ro nên kết hợp xem xét tổng hợp cơ chế kiểm soát đa chữ ký, quản trị quyền và chiến lược nâng cấp hợp đồng. Tính hợp lý của cấu trúc quyền hạn này, về cơ bản phụ thuộc vào mô hình nghiệp vụ của dự án chứ không phải bản thân mã, AI thiếu lớp ngữ cảnh này, chỉ có thể đưa ra đánh giá dựa trên khớp mẫu.

Trường hợp thử nghiệm này cho thấy, AI có thể nhận diện cấu trúc quyền hạn, nhưng không thể kết hợp ngữ cảnh nghiệp vụ để đánh giá quyền hạn có hợp lý hay không, vì vậy đã đánh dấu trực tiếp quyền mint của owner trong hợp đồng loại USDT là "lỗ hổng nguy cơ cao", đây là đánh giá sai điển hình tách rời logic thực tế nghiệp vụ – loại báo động sai này có thể gây nhiễu cho việc đánh giá rủi ro thực sự của phía dự án.
Trường hợp B · Hợp đồng nghiệp vụ phức tạp (IPC Protocol / 2025-02-recall)
Thử nghiệm thứ hai chọn dự án IPC Protocol từ báo cáo công khai trên nền tảng Code4rena (liên kết báo cáo: code4rena.com/reports/2025-02-recall). Dự án này bao gồm nhiều thành phần cốt lõi phụ thuộc lẫn nhau như Gateway, SubnetActor, mô hình proxy Diamond, tính bảo mật phụ thuộc cao vào việc hiểu sâu về kiến trúc tổng thể giao thức và logic tương tác xuyên thành phần, đây là kịch bản điển hình xảy ra các cuộc tấn công giá trị cao trong hệ sinh thái DeFi. Dưới đây là kết quả kiểm toán AI:

Đối với hợp đồng phức tạp, kiểm toán AI xuất ra tổng cộng 3 cảnh báo nguy cơ cao, 6 cảnh báo nguy cơ trung bình, xét về khối lượng đầu ra không hề kém cạnh. Nhưng một tỷ lệ đáng kể trong số đó bị kiểm toán viên đánh giá là báo động sai – AI đã đưa ra đánh giá rủi ro sai đối với các đoạn mã thiếu ngữ cảnh. Đồng thời, trong số 9 lỗ hổng cấp High được kiểm toán viên xác nhận, AI chỉ bao phủ hoàn toàn 1 mục, 2 mục khác được phát hiện nhưng xếp hạng rõ ràng thấp hơn (thực tế là High, báo cáo AI là Medium), 6 mục còn lại hoàn toàn không được phát hiện. Trong 4 lỗ hổng cấp Medium, AI bao phủ 1 mục, 3 mục hoàn toàn thiếu.
Đặc điểm chung của các lỗ hổng này là: đều phụ thuộc vào việc suy luận hoàn chỉnh đường dẫn chuyển đổi trạng thái xuyên thành phần của giao thức, chứ không phải khớp mẫu đối với một hàm đơn lẻ. Lấy ví dụ H-01 (replay signature) trong báo cáo kiểm toán thủ công, đường dẫn khai thác lỗ hổng cần hiểu ý đồ thiết kế của xác minh đa chữ ký, cách kẻ tấn công tạo tập hợp chữ ký lặp lại, và hành vi này làm thế nào để vượt qua ngưỡng trọng số. H-06 (tấn công reentrancy hàm leave()) cũng tương tự: lỗ hổng chỉ tồn tại trong trạng thái tới hạn bootstrap của mạng con, cần hiểu sự phụ thuộc chéo giữa luân chuyển staking, điều kiện kích hoạt bootstrap và trình tự thời gian gọi ngoài. Các lỗ hổng logic sâu tương tự, không có bất kỳ ghi chép nào trong danh sách cảnh báo của AI.

Kết quả này cho thấy trong kiểm toán hợp đồng phức tạp: Năng lực kiểm toán của AI nằm ở nhận diện mẫu mã cục bộ, trong khi lỗ hổng cấp giao thức có thể tồn tại sự hiểu lệch về logic nghiệp vụ tổng thể. Khi điều kiện kích hoạt lỗ hổng vượt qua nhiều hợp đồng, nhiều trạng thái, nhiều cấp độ gọi, khả năng suy luận hiện tại của AI vẫn chưa thể bao phủ hiệu quả.
Tổng hợp hai trường hợp, kiểm toán AI không phải không có giá trị – nó có đóng góp thực chất trong việc bao phủ các mẫu lỗ hổng đã biết, kiểm tra quy chuẩn mã, cũng như phát hiện từ một số góc nhìn độc lập. Nhưng ranh giới giá trị của nó rất rõ ràng: có thể dùng làm quét cơ sở, nhưng không thể trực tiếp dùng làm kết luận bảo mật. Đối với giao thức phức tạp, chỉ dựa vào báo cáo AI để đưa ra đánh giá bảo mật, không chỉ bỏ sót các lỗ hổng có rủi ro cao, mà còn vì lượng lớn cảnh báo chất lượng thấp chiếm nhiều thời gian sàng lọc của đội ngũ. Đây chính là lý do cốt lõi Beosin xây dựng cơ sở kiến thức Skill chuyên dụng, và đưa cơ chế mô hình ba lớp kiểm toán vào quy trình kiểm toán.
II. Cơ sở kiến thức Skill chuyên dụng: Con đường kỹ thuật hóa nâng cao chất lượng kiểm tra cơ sở AI
Để đưa kiểm toán AI vào quy trình kiểm toán như một bước kiểm tra cơ sở, nhất thiết phải giải quyết vấn đề tỷ lệ báo động sai và bỏ sót cao khi nó kiểm toán các giao thức DeFi thực tế. Dù là quản lý quyền hạn, cơ chế thanh khoản AMM, xác minh tin nhắn của cầu nối chuỗi chéo, hay logic thanh lý của giao thức cho vay, AI hiện tại chỉ có thể thực hiện khớp mẫu đơn giản dựa trên đặc điểm bề mặt của mã, rất khó kết hợp ngữ cảnh nghiệp vụ cụ thể và logic tấn công-phòng thủ để đánh giá xem một đoạn mã có vấn đề hay không. Cốt lõi để giải quyết vấn đề này là tiêm kinh nghiệm tích lũy nhiều năm của chuyên gia kiểm toán vào quá trình đánh giá của AI một cách có cấu trúc, giúp nó có khả năng hiểu nghiệp vụ nhất định.
Tuy nhiên cần làm rõ, ngay cả khi đưa vào tăng cường Skill, vị trí của AI trong kiểm toán cũng sẽ không thay đổi. Đối với những vấn đề phức tạp liên quan đến tương tác đa hợp


