MoveBit thuộc BitsLab công bố nghiên cứu｜Belobog: Khung kiểm thử mờ Move hướng tới các cuộc tấn công thực tế

Tác giả: BitsLab

Move là một ngôn ngữ không thể bỏ qua đối với các nhà phát triển Web3, với hệ thống kiểu mạnh và ngữ nghĩa tài nguyên, rất “cứng cáp” 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, 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 bởi vì 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 lâu dài và thực tiễn tấn công-phòng thủ, chúng tôi nhận thấy: 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ư những chuỗi gọi hàm mà từng bước đều hợp lý nhưng khi kết hợp lại có thể bị khai thác.

Chính vì vậy, dù ngôn ngữ Move có mô hình an toàn hoàn thiện hơn, nhưng trong hệ sinh thái của nó vẫn từng xảy ra các sự cố tấn công nghiêm trọng. Rõ ràng, nghiên cứu về an toàn của 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ử mờ (Fuzzing) hiệu quả. Do Move có nhiều ràng buộc hơn, các phương pháp Fuzzing hợp đồng thông minh truyền thống sẽ 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, lệnh 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, 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ố kết quả nghiên cứu:

《Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts》

arXiv:2512.02918 (bản preprint)

Bài báo này hiện được đăng trên arXiv dưới dạng preprint, mục đích là để cộng đồng có thể nhanh chóng theo dõi tiến độ nghiên cứu và phản hồi. Chúng tôi đang gửi bài 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 độ 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 theo kiểu

Ý tưởng cốt lõi của Belobog rất trực tiếp: Nếu hệ thống kiểu của Move là ràng buộc nền tảng, thì Fuzzing cũng nên lấy kiểu làm chỉ dẫn, chứ không phải là rào cản.

Cách làm truyền thống thường dựa vào sinh ngẫu nhiên và biến đổi, nhưng trên Move, điều này sẽ nhanh chóng tạo ra rất nhiều 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—kết quả cuối cùng không phải là bao phủ kiểm thử, mà là 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 đồ thị kiểu (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 để sinh hoặc biến đổi chuỗi giao dịch. Nói cách khác, nó không ghép nối lệnh gọi một cách mù quáng, mà xây dựng các tổ hợp gọi hàm hợp lý hơn, có thể thực thi hơn, dễ đi sâu vào không gian trạng thái hơn dựa trên quan hệ kiểu.

Đối với nghiên cứu an toàn, thay đổi này không phải là “thuật toán hoa mỹ hơn”, mà là lợi ích rất thực tế và then chốt:

Tỷ lệ mẫu thử hiệu quả cao hơn, hiệu suất khám phá tốt hơn, cũng có nhiều cơ hội tiếp cận các đường dẫn sâu nơi 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 để “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, khẳng định và ràng buộc. Nếu chỉ dựa vào biến đổi truyền thống, bạn sẽ dễ bị “đâm đầu vào cửa”: điều kiện không bao giờ thỏa mãn, không vào được nhánh, không đạt tới trạng thá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 kết hợp). 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 sử dụng suy diễn ký hiệu để tiếp cận có định hướng hơn các điều kiện nhánh, từ đó xuyên qua các kiểm tra phức tạp hiệu quả hơn, đẩy sâu độ bao phủ.

Điều này đặc biệt quan trọng với hệ sinh thái Move, bởi “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ử tới gần các khe hở này.

Tiệm cận thực tế: Không chỉ chạy được demo, mà còn tiếp cận đường tấn công thực sự

Chúng tôi không muốn công việc này chỉ dừng lại ở “chạy được demo”. Đánh giá của Belobog hướng trực tiếp tới các dự án thực tế và kết luận về 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 có thể phát hiện 100% lỗ hổng Critical và 79% lỗ hổng Major đã được chuyên gia bảo mật xác nhận bằng kiểm toán thủ công.

Điều đáng chú ý hơn là: Belobog có thể tái hiện hoàn chỉnh các cuộc tấn công thực sự (full exploits) trên chuỗi mà không cần dựa vào kiến thức lỗ hổng tiên nghiệm. Giá trị của khả năng này là nó gần với tình huống thực tế mà 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à 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ụ”

Bài báo này đáng đọc không chỉ vì nó đề xuất một khung 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 bảo mật thực chiến thành phương pháp có thể tái sử dụng, và hiện thực hóa nó bằng triển khai 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 ở “một Fuzzer nữa”, mà ở chỗ nó giúp Fuzzing trên Move tiệm cận thực tế hơn—chạy được, đi sâu được, và gần với đường tấn công thực sự hơn. Belobog không phải là công cụ đóng dành cho số ít chuyên gia bảo mật, mà là một khung thân thiện với nhà phát triển: nó cố gắng giảm tối đa rào cản sử dụng, giúp 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, 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 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 chỉ dừng lại ở dự án thử nghiệm “cấp công cụ”.

Bài báo (preprint):

(Đồng thời công trình này đang được gửi tới PLDI’26, chờ đánh giá đồng cấp.)

Về MoveBit

MoveBit (Mobi Security), thương hiệu con của BitsLab, là một công ty bảo mật blockchain tập trung vào hệ sinh thái Move, tiên phong sử dụng xác minh hình thức để giúp 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 bảo mật toàn diện cho các đối tác. Đội ngũ MoveBit gồm các chuyên gia bảo mật hàng đầu trong giới học thuật và doanh nghiệp, có 10 năm kinh nghiệm bảo mật, từng công bố các nghiên cứu bảo mật tại các hội nghị 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.