Tác giả: BitsLab
Move, với tư cách là một ngôn ngữ không thể bỏ qua đối với các nhà phát triển Web3, sở hữu hệ thống kiểu mạnh và ngữ nghĩa tài nguyên, rất “cứng cáp” trong các vấn đề như quyền sở hữu tài sản, chuyển nhượng bất hợp pháp, cạnh tranh dữ liệu, v.v.
Các hệ sinh thái như Sui, Aptos ngày càng đặt nhiều tài sản quan trọng và giao thức cốt lõi lên Move, cũng chính nhờ các đặc tính cốt lõi của ngôn ngữ Move, giúp xây dựng các hợp đồng thông minh an toàn hơn, ít rủi ro hơn.
Tuy nhiên, qua quá trình kiểm toán và thực chiến tấn công-phòng thủ lâu dài, chúng tôi nhận thấy thực tế là: phần lớn các vấn đề nan giải thường không xảy ra ở những vị trí dễ thấy như “lỗi cú pháp” hay “không khớp kiểu”, mà lại xuất hiện ở các tầng hệ thống phức tạp và thực tế hơn—tương tác liên mô-đun, giả định về quyền hạn, ranh giới máy trạng thái, cũng như các chuỗi gọi hàm mà từng bước riêng lẻ đều hợp lý nhưng khi kết hợp lại lại có thể bị khai thác.
Chính vì vậy, dù ngôn ngữ Move có mô hình an ninh hoàn thiện hơn, nhưng trong hệ sinh thái của nó vẫn từng xảy ra những sự cố tấn công nghiêm trọng. Rõ ràng, nghiên cứu an ninh về Move vẫn cần tiến xa hơn nữa.
Chúng tôi đã nhận ra một vấn đề cốt lõi: trong ngôn ngữ Move, thiếu một công cụ kiểm thử ngẫu nhiên (Fuzzing) hiệu quả. Do Move có nhiều ràng buộc hơn, các công cụ Fuzzing hợp đồng thông minh truyền thống gặp phải một điểm đau lớn trong bối cảnh Move: việc tạo ra chuỗi giao dịch “đúng kiểu” và “có thể đạt được về mặt ngữ nghĩa” là vô cùng phức tạp. Nếu đầu vào không đủ chính xác, cuộc gọi sẽ không thực hiện được; không gọi được thì không thể bao phủ các nhánh sâu, chạm tới trạng thái quan trọng, và dễ bỏ lỡ các đường dẫn thực sự có thể kích hoạt lỗ hổng.
Dựa trên điểm đau này, chúng tôi đã hợp tác với nhóm nghiên cứu đại học, cùng hoàn thành và công bố thành quả nghiên cứu:
《Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts》
arXiv:2512.02918 (bản preprint)
Liên kết bài báo:
Bài báo này hiện được công bố trên arXiv dưới dạng preprint, ý nghĩa là để cộng đồng có thể sớm theo dõi tiến độ nghiên cứu và phản hồi. Chúng tôi đang gửi công trình này tới PLDI’26 và chờ quy trình peer review. Sau khi có kết quả và hoàn thành đánh giá đồng cấp, chúng tôi sẽ cập nhật tiến triển liên quan ngay lập tức.
Để Fuzzing thực sự “chạy được” trên Move: Từ thử-sai ngẫu nhiên đến dẫn dắt bởi kiểu dữ liệu
Ý tưởng cốt lõi của Belobog rất trực tiếp: vì hệ thống kiểu của Move là ràng buộc nền tảng của nó, nên Fuzzing cũng nên coi kiểu dữ liệu là chỉ dẫn, thay vì là trở ngại.
Cách làm truyền thống thường dựa vào tạo ngẫu nhiên và biến dị, nhưng trên Move, điều này sẽ nhanh chóng tạo ra hàng loạt mẫu thử vô hiệu: không khớp kiểu, tài nguyên không thể truy cập, tham số không thể xây dựng đúng, chuỗi gọi hàm bị tắc nghẽn—cuối cùng bạn không có được độ bao phủ kiểm thử mà chỉ có một đống “thất bại ngay từ đầu”.
Phương pháp của Belobog giống như trang bị cho Fuzzer một “bản đồ”. Nó xuất phát từ hệ thống kiểu của Move, xây dựng type graph dựa trên ngữ nghĩa kiểu cho hợp đồng mục tiêu, rồi dựa vào đồ thị này để tạo hoặc biến dị chuỗi giao dịch. Nói cách khác, nó không ghép nối các cuộc gọi một cách mù quáng, mà xây dựng các tổ hợp cuộc gọi hợp lý, khả thi và dễ dàng đi sâu vào không gian trạng thái hơn dựa trên quan hệ kiểu dữ liệu.
Đối với nghiên cứu an ninh, thay đổi này không mang lại “thuật toán hoa mỹ” mà là lợi ích rất thực tế và then chốt:
Tỷ lệ mẫu thử hợp lệ cao hơn, hiệu quả khám phá tốt hơn, và có nhiều cơ hội tiếp cận các đường dẫn sâu nơi lỗ hổng thực sự thường xuất hiện.
Đối mặt với ràng buộc phức tạp: Belobog tích hợp Concolic Execution để “mở cửa”
Trong hợp đồng Move thực tế, logic quan trọng thường bị bao quanh bởi nhiều lớp kiểm tra, xác nhận và ràng buộc. Nếu chỉ dựa vào biến dị truyền thống, bạn rất dễ “đâm đầu vào cửa”: điều kiện không bao giờ thỏa mãn, nhánh không vào được, trạng thái không đạt tới.
Để giải quyết vấn đề này, Belobog tiếp tục thiết kế và hiện thực hóa concolic execution (kết hợp thực thi cụ thể và suy diễn ký hiệu). Nói đơn giản là:
Một mặt nó duy trì thực thi cụ thể “có thể chạy được”, mặt khác tận dụng suy diễn ký hiệu để tiếp cận có định hướng hơn tới các điều kiện nhánh, từ đó xuyên qua các kiểm tra phức tạp và tăng độ sâu bao phủ.
Điều này đặc biệt quan trọng với hệ sinh thái Move, vì “cảm giác an toàn” của hợp đồng Move thường dựa trên nhiều lớp ràng buộc, trong khi vấn đề thực sự lại ẩn trong các khe hở giữa các ràng buộc đó. Điều Belobog muốn làm là đẩy kiểm thử đến gần các khe hở này.
Tiệm cận thế giới thực: Không chỉ chạy demo mà còn tiếp cận đường tấn công thực tế
Chúng tôi không muốn công trình này chỉ dừng lại ở “chạy được demo”. Đánh giá của Belobog hướng thẳng tới dự án thực và kết luận lỗ hổng thực tế. Theo kết quả thực nghiệm trong bài báo: Belobog được đánh giá trên 109 dự án hợp đồng thông minh Move thực tế, kết quả cho thấy Belobog phát hiện được 100% lỗ hổng Critical và 79% lỗ hổng Major đã được chuyên gia an ninh xác nhận bằng tay.
Điều đáng chú ý hơn: Belobog có thể tái hiện toàn bộ tấn công (full exploits) trên các sự kiện on-chain thực tế mà không cần dựa vào kiến thức lỗ hổng tiên nghiệm. Giá trị của năng lực này là nó gần với tình huống thực tế chúng ta đối mặt trong tấn công-phòng thủ: kẻ tấn công không chỉ dựa vào “lỗi hàm đơn lẻ” mà thành công, mà là dựa vào đường dẫn hoàn chỉnh và tiến hóa trạng thái.
Điều mà công trình này muốn truyền tải không chỉ là “làm ra một công cụ”
Lý do bài báo này đáng đọc không chỉ vì nó đề xuất một framework mới, mà còn vì nó đại diện cho một hướng đi thực tiễn hơn: trừu tượng hóa kinh nghiệm an ninh tuyến đầu thành phương pháp có thể tái sử dụng, và hiện thực hóa nó bằng kỹ thuật có thể kiểm chứng.
Chúng tôi cho rằng ý nghĩa của Belobog không nằm ở “thêm một Fuzzer nữa”, mà ở chỗ nó giúp Fuzzing trên Move gần với thực tế hơn—có thể chạy, đi sâu, và tiệm cận đường tấn công thực tế. Belobog không phải là công cụ đóng dành cho số ít chuyên gia an ninh, mà là một framework thân thiện với developer: nó cố gắng giảm rào cản sử dụng, giúp developer liên tục tích hợp kiểm thử an ninh vào quy trình phát triển quen thuộc, thay vì biến Fuzzing thành công việc làm một lần, sau sự kiện.
Chúng tôi cũng sẽ phát hành Belobog dưới dạng mã nguồn mở, hy vọng nó trở thành hạ tầng mà cộng đồng có thể cùng sử dụng, mở rộng và phát triển, thay vì chỉ là dự án thử nghiệm ở “tầng công cụ”.
Bài báo (preprint):
(Đồng thời công trình này đang gửi tới PLDI’26, chờ đánh giá đồng cấp.)
Về MoveBit
MoveBit (Mobi Security), thương hiệu con thuộc BitsLab, là một công ty an ninh blockchain tập trung vào hệ sinh thái Move, tiên phong sử dụng xác minh hình thức để biến hệ sinh thái Move trở thành hệ sinh thái Web3 an toàn nhất. MoveBit đã hợp tác với nhiều dự án nổi tiếng toàn cầu, cung cấp dịch vụ kiểm toán an ninh toàn diện cho đối tác. Đội ngũ MoveBit gồm các chuyên gia an ninh hàng đầu trong giới học thuật và doanh nghiệp, có 10 năm kinh nghiệm an ninh, từng công bố nghiên cứu tại các hội nghị an ninh quốc tế hàng đầu như NDSS, CCS. Họ cũng là những người đóng góp sớm nhất cho hệ sinh thái Move, cùng các nhà phát triển Move xây dựng tiêu chuẩn ứng dụng Move an toàn.
