Phân tích tính an toàn của ngôn ngữ Move

Ngôn ngữ Move, như một ngôn ngữ hợp đồng thông minh thế hệ mới, đã xem xét vấn đề an toàn của blockchain và hợp đồng thông minh ngay từ khi thiết kế ban đầu. Bài viết này sẽ khám phá tính an toàn của ngôn ngữ Move từ ba khía cạnh: đặc điểm ngôn ngữ, cơ chế thực thi và công cụ xác minh.

1. Các tính năng bảo mật của ngôn ngữ Move

Ngôn ngữ Move đã từ bỏ logic phi tuyến tính dựa trên tính linh hoạt, không hỗ trợ phân phối động và gọi bên ngoài đệ quy, mà sử dụng các khái niệm như kiểu tổng quát, lưu trữ toàn cầu, tài nguyên để thực hiện các mô hình lập trình thay thế. Những thiết kế này giúp tránh các lỗ hổng bảo mật như tấn công tái nhập.

Các thành phần chính của ngôn ngữ Move bao gồm:

• Mô-đun: được cấu thành từ các kiểu cấu trúc và định nghĩa quy trình, có thể nhập các định nghĩa kiểu từ mô-đun khác và gọi quy trình từ các mô-đun khác.

• Cấu trúc: có thể được định nghĩa là loại tài nguyên, lưu trữ trong kho khóa giá trị toàn cầu.

• Quá trình: Định nghĩa chức năng của mô-đun, có thể bao gồm quá trình khởi tạo, an toàn và không an toàn.

Cơ chế lưu trữ toàn cầu của ngôn ngữ Move cho phép các mô-đun lưu trữ dữ liệu bền vững và có quyền truy cập đọc/ghi độc quyền đối với các loại tài nguyên mà nó khai báo. Cơ chế này giúp thực thi các ràng buộc an toàn.

Hai đặc điểm kiểm tra tĩnh quan trọng của ngôn ngữ Move:

1. Kiểm tra bất biến: Định nghĩa tính bảo toàn trạng thái hệ thống bằng ngôn ngữ quy ước.

2. Trình xác thực bytecode: Thực thi các loại an toàn và tuyến tính, ngăn chặn các thao tác bất hợp pháp.

2. Cơ chế hoạt động của Move

Chương trình Move chạy trong máy ảo, không thể truy cập trực tiếp vào bộ nhớ hệ thống. Việc thực hiện chương trình dựa trên stack, bộ nhớ toàn cục được chia thành bộ nhớ ( heap ) và biến toàn cục ( stack ).

Trạng thái thực thi của Move VM được cấu thành từ ngăn xếp gọi, bộ nhớ, biến toàn cục và các thao tác. Các đặc điểm của nó bao gồm:

• Chuyển hướng tĩnh, tránh phân phối động
• Gọi ngăn xếp liền kề, ngăn chặn tái nhập
• Tách biệt lưu trữ và gọi dữ liệu.

Thiết kế này nâng cao tính bảo mật và hiệu quả thực thi.

3. Di chuyển Prover

Move Prover là một công cụ xác minh hình thức, sử dụng thuật toán xác minh suy diễn để kiểm tra xem chương trình có đáp ứng mong đợi hay không. Quy trình làm việc của nó:

1. Nhận tệp nguồn Move và quy định
2. Biên dịch thành mã byte và mô hình đối tượng xác thực
3. Chuyển đổi sang ngôn ngữ trung gian Boogie
4. Tạo điều kiện xác minh
5. Sử dụng bộ giải Z3 để xác minh
6. Tạo báo cáo chẩn đoán

Ngôn ngữ đặc tả di chuyển được sử dụng để mô tả quy tắc hành vi của chương trình, có thể được viết độc lập với mã nghiệp vụ.

Tóm tắt

Ngôn ngữ Move đã xem xét toàn diện ở nhiều khía cạnh như đặc điểm ngôn ngữ, thực thi máy ảo và công cụ bảo mật, có thể tránh hiệu quả nhiều lỗ hổng phổ biến. Tuy nhiên, vẫn khuyên nên sử dụng dịch vụ kiểm toán bảo mật bên thứ ba và để các công ty bảo mật thực hiện việc viết và xác minh mã theo tiêu chuẩn.