Phân tích lỗ hổng tràn số nguyên trong xác thực an toàn tham chiếu ngôn ngữ Move

Gần đây, trong quá trình nghiên cứu sâu về ngôn ngữ Move, chúng tôi đã phát hiện ra một lỗ hổng tràn số nguyên mới. Lỗ hổng này tồn tại trong quá trình xác minh an toàn tham chiếu, và quá trình kích hoạt của nó rất thú vị. Bài viết này sẽ phân tích sâu về lỗ hổng này và khám phá một số kiến thức nền tảng liên quan đến ngôn ngữ Move.

Ngôn ngữ Move sẽ tiến hành xác thực đơn vị mã trước khi thực thi bytecode, chia thành bốn bước. Lỗ hổng này xảy ra trong bước reference_safety.

Mô-đun xác minh an toàn tham chiếu định nghĩa hàm chuyển đổi được sử dụng để xác minh an toàn tham chiếu của thực thể quá trình. Nội dung kiểm tra bao gồm xác minh không có tham chiếu lơ lửng, truy cập vào tham chiếu có thể thay đổi có an toàn hay không, truy cập vào tham chiếu lưu trữ toàn cục có an toàn hay không, v.v.

Hàm nhập xác thực bảo mật được gọi là analyze_function, xác thực từng khối cơ bản. Khối cơ bản là đoạn mã không có lệnh nhánh ngoại trừ lệnh vào và lệnh ra. Ngôn ngữ Move xác định khối cơ bản bằng cách duyệt mã byte, tìm tất cả các lệnh nhánh và chuỗi lệnh vòng lặp.

Ngôn ngữ Move hỗ trợ hai loại tham chiếu: tham chiếu bất biến & và tham chiếu biến đổi &mut. Tham chiếu bất biến được sử dụng để đọc dữ liệu, tham chiếu biến đổi được sử dụng để sửa đổi dữ liệu. Sử dụng hợp lý các loại tham chiếu sẽ giúp duy trì an toàn và nhận diện các mô-đun đọc.

Mô-đun an toàn tham chiếu sẽ quét từng hàm theo đơn vị hàm, kiểm tra các lệnh bytecode của khối cơ bản trong hàm, xác minh rằng tất cả các thao tác tham chiếu là hợp pháp. Quá trình xác minh chủ yếu liên quan đến cấu trúc AbstractState, bao gồm đồ thị mượn (borrow graph) và các biến cục bộ (locals), nhằm đảm bảo tính an toàn của tham chiếu trong hàm.

Trong quá trình xác thực, sẽ so sánh trạng thái trước và sau khi thực thi khối cơ bản, thông qua việc xem join_result có thay đổi hay không để hợp nhất trạng thái trước và trạng thái sau. Nếu có sự thay đổi và khối hiện tại có một cạnh quay lại chính nó (biểu thị sự tồn tại của vòng lặp), sẽ quay lại đầu vòng lặp và tiếp tục thực thi khối cơ bản đó, cho đến khi trạng thái sau bằng với trạng thái trước hoặc dừng lại do lỗi.

Lỗi xuất hiện trong quá trình xác định xem kết quả join có thay đổi hay không. Khi tổng chiều dài của tham số và chiều dài biến cục bộ lớn hơn 256, việc sử dụng loại u8 để lặp qua locals sẽ dẫn đến tràn số nguyên. Mặc dù Move có quy trình kiểm tra số lượng locals, nhưng mô-đun kiểm tra giới hạn chỉ kiểm tra locals mà không bao gồm chiều dài tham số.

Lỗ hổng tràn số nguyên này có thể dẫn đến cuộc tấn công từ chối dịch vụ (DoS). Kẻ tấn công có thể tạo ra các khối mã lặp và lợi dụng sự tràn để thay đổi trạng thái của khối, làm cho bản đồ locals mới khác với trước đây. Khi hàm execute_block được thực thi lại, việc phân tích chuỗi các lệnh bytecode trong basic block sẽ truy cập vào bản đồ locals mới. Nếu chỉ số mà lệnh cần truy cập không tồn tại trong bản đồ locals của AbstractState mới, sẽ dẫn đến DoS.

Để xác minh lỗ hổng này, có thể tái hiện PoC trong git. Khối mã trong PoC chứa một chỉ thị nhánh vô điều kiện, mỗi lần thực thi chỉ thị cuối cùng đều nhảy về chỉ thị đầu tiên, dẫn đến việc gọi nhiều lần hàm execute_block và hàm join.

Lỗ hổng này cho thấy ngay cả những ngôn ngữ chú trọng đến an toàn như Move cũng có thể tồn tại rủi ro an ninh. Nó nhấn mạnh tầm quan trọng của việc kiểm tra mã, đồng thời cũng gợi ý cho các nhà thiết kế ngôn ngữ Move nên thêm nhiều kiểm tra mã hơn trong thời gian thực để ngăn chặn các tình huống không mong muốn xảy ra. Hiện tại, Move chủ yếu thực hiện kiểm tra an toàn ở giai đoạn xác minh, nhưng một khi việc xác minh bị bỏ qua, giai đoạn chạy thiếu sự gia cố an toàn đủ có thể dẫn đến những vấn đề nghiêm trọng hơn.

Là người dẫn đầu nghiên cứu an ninh ngôn ngữ Move, chúng tôi sẽ tiếp tục đào sâu nghiên cứu các vấn đề an ninh của Move và sẽ chia sẻ thêm nhiều phát hiện trong thời gian tới.