Phát hiện lỗ hổng tràn số nguyên mới trong cơ chế bảo mật tham chiếu của 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 xuất hiện trong quá trình xác thực an toàn tham chiếu, liên quan đến một số cơ chế cốt lõi của ngôn ngữ Move. Thông qua việc phân tích lỗ hổng này, chúng tôi có thể hiểu sâu hơn về thiết kế và triển khai của ngôn ngữ Move.

Quy trình xác minh ngôn ngữ Move

Ngôn ngữ Move sẽ xác thực các đơn vị mã trước khi thực thi bytecode, quá trình này được chia thành 4 bước. Lỗ hổng được phát hiện lần này xảy ra trong bước reference_safety.

Mô-đun reference_safety định nghĩa các hàm cốt lõi để xác minh tính an toàn của tham chiếu. Nó chủ yếu kiểm tra xem có tồn tại tham chiếu lơ lửng hay không, việc truy cập tham chiếu biến có an toàn hay không, và việc truy cập tham chiếu lưu trữ toàn cục có an toàn hay không.

Hàm nhập của quá trình xác thực sẽ gọi analyze_function để phân tích từng hàm. analyze_function sẽ xác thực từng khối cơ bản trong hàm. Khối cơ bản là một chuỗi mã không có lệnh nhánh ngoại trừ đầu vào và đầu ra.

An toàn tham chiếu trong ngôn ngữ Move

Ngôn ngữ Move hỗ trợ hai loại tham chiếu: tham chiếu không thay đổi (&) và tham chiếu thay đổi (&mut). Tham chiếu không thay đổi được sử dụng để đọc dữ liệu, tham chiếu thay đổi được sử dụng để sửa đổi dữ liệu. Thiết kế này giúp cải thiện tính an toàn và khả năng đọc của mã.

Mô-đun xác minh an toàn sẽ quét mã byte của từng khối cơ bản trong hàm, xác định xem tất cả các thao tác tham chiếu có hợp pháp hay không. Quá trình xác minh chủ yếu bao gồm:

1. Thực hiện mã khối cơ bản
2. Trạng thái trước và sau khi thực hiện hợp nhất
3. Cập nhật trạng thái khối
4. Truyền điều kiện hậu kiểm đến các khối tiếp theo

Quá trình này tương tự như ý tưởng Sea of Nodes trong V8 turbofan.

Phân tích lỗ hổng

Lỗi xảy ra trong quá trình trạng thái trước và sau khi thực hiện hợp nhất. Khi độ dài tham số hàm cộng với độ dài biến cục bộ lớn hơn 256, việc sử dụng loại u8 để biểu thị chỉ số biến cục bộ sẽ dẫn đến tràn số nguyên.

Mặc dù ngôn ngữ Move có quy trình kiểm tra số lượng biến cục bộ, nhưng quy trình này không bao gồm độ dài tham số. Các nhà phát triển dường như nhận ra cần kiểm tra tổng số tham số và biến cục bộ, nhưng mã thực tế chỉ kiểm tra số lượng biến cục bộ.

Sự tràn số nguyên này có thể dẫn đến tấn công từ chối dịch vụ (DoS). Kẻ tấn công có thể xây dựng một khối mã vòng lặp, lợi dụng sự tràn để thay đổi trạng thái của khối. Khi khối cơ bản được thực thi lại, nếu chỉ thị cần truy cập chỉ mục không tồn tại trong trạng thái mới, chương trình sẽ bị sập.

Khai thác lỗ hổng

Chúng tôi đã xây dựng một bằng chứng khái niệm (PoC) để trình bày lỗ hổng này:

1. Tạo một khối cơ bản chứa lệnh nhánh vô điều kiện để thực hiện nhiều lần.
2. Đặt tổng số tham số và biến cục bộ là 264, dẫn đến độ dài ánh xạ biến cục bộ mới bị tràn là 8.
3. Khi thực hiện lại khối cơ bản, cố gắng truy cập chỉ mục biến cục bộ không tồn tại, gây ra panic.

Kết luận

Lỗ hổng này một lần nữa chứng minh rằng không có mã nào hoàn toàn an toàn. Mặc dù ngôn ngữ Move đã thực hiện kiểm tra tĩnh trước khi thực thi, nhưng vẫn có thể bị vượt qua bởi lỗ hổng tràn số nguyên.

Đối với sự phát triển tương lai của ngôn ngữ Move, chúng tôi đề xuất:

1. Tăng cường mã kiểm tra trong quá trình thực thi để ngăn chặn các tình huống bất ngờ.
2. Không chỉ dựa vào kiểm tra an ninh ở giai đoạn xác thực, mà còn cần tăng cường an ninh trong giai đoạn vận hành.

Là người tiên phong trong nghiên cứu an toàn ngôn ngữ Move, chúng tôi sẽ tiếp tục nghiên cứu sâu về các vấn đề an toàn của Move, đóng góp vào sự phát triển của nó.