Nhóm Monad chia sẻ thực tiễn xác minh hình thức, phát hiện nhiều lỗ hổng an toàn trên chuỗi bị bỏ sót trong quá trình kiểm tra của các mô hình AI

Theo tin tức từ Foresight News, nhóm phát triển Monad thuộc Category Labs đã đăng bài chia sẻ kinh nghiệm sử dụng phương pháp xác minh hình thức (Formal Verification) để phát hiện lỗ hổng trong các mô-đun quan trọng của chuỗi khối Monad, công bố nhiều lỗ hổng mà các mô hình lớn tiên tiến như Claude Opus 4.8, Codex... không phát hiện ra trong quá trình kiểm tra mã, nhưng đã bị phát hiện thành công bằng phương pháp chứng minh hình thức. Các vấn đề này liên quan đến thiết kế “Reserve Balance (Số dư dự trữ)” trong cơ chế thực thi bất đồng bộ của Monad và hành vi không xác định của C++ trong tối ưu hóa lưu trữ MIP-8. Nhóm nghiên cứu cho rằng so với việc yêu cầu mô hình “kiểm tra mã” trực tiếp, việc viết ra các định đề về tính chính xác một cách chính xác rồi yêu cầu mô hình tìm phản ví dụ sẽ dễ dàng phát hiện các lỗ hổng tiềm ẩn hơn. Xác minh hình thức hiện đã có thể được hỗ trợ đáng kể bởi AI.