Move là một ngôn ngữ mà các nhà phát triển Web3 không thể bỏ qua, với hệ thống kiểu mạnh và ngữ nghĩa tài nguyên, nó rất "cứng cỏi" trong các khía cạnh như quyền sở hữu tài sản, chuyển giao bất hợp pháp, cạnh tranh dữ liệu. Các hệ sinh thái như Sui, Aptos đặt ngày càng nhiều tài sản quan trọng và giao thức cốt lõi trên Move cũng bởi vì các đặc tính cốt lõi của ngôn ngữ Move, cho phép xây dựng các hợp đồng thông minh an toàn hơn, ít rủi ro hơn.
Nhưng thực tế mà chúng tôi thấy trong quá trình kiểm toán và tấn công-phòng thủ lâu dài là: phần lớn các vấn đề nan giải thường không xảy ra ở những vị trí rõ ràng như "lỗi cú pháp" hoặc "không khớp kiểu", mà xảy ra ở cấp độ hệ thống phức tạp hơn, thực tế hơn — tương tác đa mô-đun, giả định quyền hạn, ranh giới máy trạng thái, và những chuỗi lệnh gọi mà từng bước xem riêng lẻ thì hợp lý nhưng kết hợp lại lại có thể bị khai thác. Cũng chính vì vậy, mặc dù ngôn ngữ Move có mô hình bảo mật hoàn thiện hơn, nhưng trong hệ sinh thái của nó vẫn xảy ra các sự kiện tấn công có ảnh hưởng lớn. Rõ ràng, nghiên cứu bảo mật Move cần phải tiến xa hơn nữa.
Chúng tôi đã nhận thấy một vấn đề cốt lõi: trong ngôn ngữ Move, thiếu một công cụ kiểm thử fuzzing hiệu quả. Bởi vì các ràng buộc của Move mạnh hơn, Fuzzing hợp đồng thông minh truyền thống trong bối cảnh Move sẽ phải đối mặt với một điểm đau nan giải: việc tạo ra các chuỗi giao dịch "đúng kiểu" và "có thể đạt được về ngữ nghĩa" là rất phức tạp. Đầu vào không đủ chính xác, lệnh gọi không thể hoàn thành; không thể gọi, thì không thể bao phủ các nhánh sâu, chạm tới các trạng thái quan trọng, và dễ dàng 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 lâu dài này, chúng tôi đã hợp tác với nhóm nghiên cứu học thuật và cùng hoàn thành, công bố kết quả nghiên cứu:
《Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts》
arXiv:2512.02918 (Bản in trước)
Liên kết bài báo:https://arxiv.org/abs/2512.02918
Bài báo này hiện được công bố trên arXiv thuộc dạng preprint (bản in trước), ý nghĩa của nó là để cộng đồng thấy được tiến độ nghiên cứu nhanh hơn và tiếp nhận phản hồi. Chúng tôi đang nộp công trình này cho PLDI’26 và đang chờ quy trình đánh giá ngang hàng (peer review). Sau khi kết quả nộp bài được xác nhận và hoàn tất đánh giá ngang hàng, chúng tôi cũng sẽ đồng bộ tiến độ liên quan trong thời gian sớm nhất.
Để Fuzzing thực sự "chạy được" Move: Từ thử sai ngẫu nhiên đến định hướng kiểu dữ liệu
Tư 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 cơ bản của nó, thì Fuzzing cũng nên lấy kiểu dữ liệu làm la bàn, chứ không phải là chướng ngại vật.
Cách làm truyền thống phần lớn dựa vào việc 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 một lượng lớn mẫu không hợp lệ: 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 chính xác, chuỗi lệnh gọi tồn tại điểm nghẽn — cuối cùng bạn nhận được không phải là độ bao phủ kiểm thử, mà là một đống "thất bại ngay từ vạch xuất phát".
Phương pháp của Belobog giống như lắp cho Fuzzer một "tấm 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 trên đồ thị này để tạo hoặc biến dị chuỗi giao dịch. Nói cách khác, nó không phải là kết nối lệnh gọi một cách mù quáng, mà là xây dựng các tổ hợp lệnh gọi hợp lý hơn, có thể thực thi được hơn, dễ dàng đi sâu vào không gian trạng thái hơn dọc theo các quan hệ kiểu.
Đối với nghiên cứu bảo mật, sự thay đổi này mang lại không phải là "thuật toán hào nhoáng hơn", mà là lợi ích đơn giản nhưng then chốt:
Tỷ lệ mẫu hợp lệ cao hơn, hiệu suất khám phá cao hơn, và cũng có nhiều cơ hội chạm tới các đường dẫn sâu nơi các lỗ hổng thực tế thường xuất hiện.
Đối mặt với ràng buộc phức tạp: Belobog đưa vào Concolic Execution để "đẩy cánh cửa"
Trong hợp đồng Move thực tế, logic then chốt thường bị bao quanh bởi nhiều tầng kiểm tra, khẳng định 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 sầm vào cửa ra vào: điều kiện mãi không thỏa mãn, nhánh mãi không vào được, trạng thái mãi không đạt tới.
Để giải quyết vấn đề này, Belobog tiếp tục thiết kế và triển khai concolic execution (thực thi cụ thể + suy diễn ký hiệu hỗn hợp). Nói đơn giản là:
Một mặt nó duy trì thực thi cụ thể "có thể chạy", mặt khác sử dụng suy diễn ký hiệu để tiệm cận các điều kiện nhánh đó một cách có định hướng hơn, từ đó xuyên thủng các kiểm tra phức tạp hiệu quả hơn, đẩy sâu độ bao phủ.
Điểm 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 được xây dựng dựa trên các ràng buộc đa tầng, và vấn đề thực sự thường ẩn trong các khe hở sau khi các ràng buộc đan xen. Điều Belobog muốn làm, là đẩy việc kiểm thử tới gần những khe hở này.
Căn chỉnh thế giới thực: Không phải chạy thử demo, mà là tiệm cận đường dẫn tấn công thực tế
Chúng tôi không mong muốn loại công việc này chỉ dừng lại ở "chạy thử demo". Đánh giá của Belobog hướng trực tiếp đến các dự án thực tế 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ả thực nghiệm cho thấy, Belobog có thể phát hiện 100% lỗ hổng Critical và 79% lỗ hổng Major đã được các chuyên gia bảo mật xác nhận thủ công.
Đáng chú ý hơn: Belobog trong tình huống không phụ thuộc vào kiến thức lỗ hổng tiên nghiệm, có thể tái hiện đầy đủ các cuộc tấn công (full exploits) trong các sự kiện trên chuỗi thực tế. Giá trị của loại năng lực này nằm ở chỗ, nó gần gũi hơn với tình huống chúng ta đối mặt trong tấn công-phòng thủ thực tế: kẻ tấn công không thành công nhờ "lỗi hàm đơn điểm", mà thành công nhờ đường dẫn đầy đủ và sự tiến hóa trạng thái.
Công việc này muốn biểu đạt, 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 khuôn khổ mới, mà vì nó đại diện cho một hướng đi thiết thực hơn: trừu tượng hóa kinh nghiệm bảo mật thực tiễn thành phương pháp có thể tái sử dụng, và dùng triển khai kỹ thuật có thể kiểm chứng để đưa nó vào thực tế.
Chúng tôi cho rằng ý nghĩa của Belobog không nằm ở "lại một Fuzzer nữa", mà ở chỗ nó làm cho Fuzzing trên Move gần với thực tế hơn — có thể chạy vào, có thể đi sâu, và cũng gần với đường dẫn tấn công thực tế hơn. Belobog không phải là công cụ khép kín thiết kế cho số ít chuyên gia bảo mật, mà là một khuôn khổ thân thiện với nhà phát triển (developer-friendly): nó cố gắng hạ thấp ngưỡng sử dụng, để nhà phát triển có thể liên tục đưa kiểm thử bảo mật vào quy trình phát triển quen thuộc, chứ không biến Fuzzing thành công việc làm một lần, làm sau sự kiện.
Chúng tôi cũng sẽ công bố Belobog theo cách mã nguồn mở, hy vọng nó trở thành cơ sở hạ tầng mà cộng đồng có thể cùng sử dụng, mở rộng và phát triển, chứ không dừng lại ở dự án thử nghiệm "cấp độ công cụ".
Bài báo (bản in trước):https://arxiv.org/abs/2512.02918
(Đồng thời công việc này đang được nộp cho PLDI’26, đang chờ đánh giá ngang hàng.)
Về MoveBit
MoveBit (Mòbǐ ānquán - Mò Bì Security), thương hiệu con thuộc BitsLab, là một công ty bảo mật blockchain chuyên sâu vào hệ sinh thái Move, thông qua việc tiên phong sử dụng xác minh hình thức (formal verification) để biến hệ sinh thái Move trở thành hệ sinh thái Web3 an toàn nhất. MoveBit đã lần lượt hợp tác với nhiều dự án nổi tiếng toàn cầu và cung cấp dịch vụ kiểm toán bảo mật toàn diện cho các đối tác. Đội ngũ MoveBit bao gồm các chuyên gia bảo mật hàng đầu từ giới học thuật và các nhân vật tiên phong trong lĩnh vực bảo mật doanh nghiệp, có kinh nghiệm bảo mật 10 năm, đã công bố thành tựu nghiên cứu bảo mật tại các hội nghị học thuật bảo mật quốc tế đỉnh cao như NDSS, CCS. Và họ là những người đóng góp sớm nhất cho hệ sinh thái Move, cùng với các nhà phát triển Move thiết lập tiêu chuẩn cho ứng dụng Move an toàn.
