Phân tích an ninh ngôn ngữ Move: Người cách mạng của ngôn ngữ hợp đồng thông minh thế hệ mới

Ngôn ngữ Move, như một loại ngôn ngữ hợp đồng thông minh mới, đã được thiết kế từ đầu với sự xem xét đầy đủ về vấn đề an ninh của blockchain và hợp đồng thông minh, và đã tham khảo một số nguyên tắc thiết kế an ninh của ngôn ngữ Rust. 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ế hoạt động và công cụ xác thực.

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

Ngôn ngữ Move trong thiết kế đã từ bỏ nhiều logic phi tuyến dựa trên tính linh hoạt, không hỗ trợ gọi ngoài động và đệ quy, mà thay vào đó giới thiệu 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 đặc điểm này giúp tránh các lỗ hổng thường gặp như tấn công gọi lại trong các ngôn ngữ hợp đồng thông minh khác.

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

• Mô-đun (Module): Được cấu thành từ một loạt các loại cấu trúc và định nghĩa quy trình.
• Cấu trúc (Structs): có thể được định nghĩa là loại tài nguyên, được lưu trữ trong kho khóa/giá trị toàn cầu bền vững.
• quá trình (function): định nghĩa chức năng cụ thể của hợp đồng thông minh

Hai khái niệm quan trọng của ngôn ngữ Move là loại tài nguyên và lưu trữ toàn cầu. Lưu trữ toàn cầu cho phép chương trình Move lưu trữ dữ liệu bền vững, dữ liệu này chỉ có thể được đọc và viết theo cách lập trình bởi mô-đun sở hữu nó, nhưng được lưu trữ trong sổ cái công khai để có thể xem. Loại tài nguyên đảm bảo quyền truy cập độc quyền vào lưu trữ toàn cầu.

Ngôn ngữ Move đảm bảo tính an toàn của mã trong quá trình biên dịch thông qua hai cơ chế: kiểm tra bất biến và bộ xác thực mã byte.

• Kiểm tra bất biến: Định nghĩa sự bảo toàn trạng thái hệ thống thông qua ngôn ngữ quy tắc.
• Trình xác minh bytecode: thực hiện kiểm tra kiểu an toàn và xác minh tuyến tính, bao gồm kiểm tra tính hợp pháp của cấu trúc, kiểm tra ngữ nghĩa của logic quy trình và kiểm tra lỗi liên kết.

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 bộ nhớ hệ thống trong quá trình thực thi, điều này đảm bảo an toàn khi hoạt động trong môi trường không tin cậy.

Chương trình Move thực thi trên ngăn xếp, trạng thái của nó bao gồm ngăn xếp gọi, bộ nhớ, biến toàn cục và các thao tác. Các lệnh bytecode của Move được thực thi trong trình giải thích kiểu ngăn xếp, thuận lợi cho việc sao chép và kiểm soát di chuyển giữa các biến.

Move VM tách biệt lưu trữ dữ liệu và ngăn xếp gọi, điều này khác biệt lớn với EVM. Trạng thái người dùng được lưu trữ độc lập, các cuộc gọi chương trình phải tuân thủ quy tắc quyền hạn và tài nguyên, trong khi hy sinh một phần tính linh hoạt, nâng cao tính an toàn và hiệu suất thực thi.

3. Di chuyển Prover

Move Prover là công cụ xác minh hình thức được cung cấp bởi ngôn ngữ Move, sử dụng thuật toán xác minh suy diễn để kiểm tra xem chương trình có phù hợp với kỳ vọng hay không. Quy trình làm việc của nó như sau:

1. Nhận tệp nguồn Move và tiêu chuẩn làm đầu vào
2. Trích xuất quy tắc và biên dịch tệp nguồn thành bytecode
3. Chuyển đổi thành mô hình đối tượng xác thực
4. Dịch sang ngôn ngữ trung gian Boogie
5. Tạo điều kiện xác minh
6. Sử dụng bộ giải Z3 để kiểm tra tính thỏa mãn của công thức
7. Tạo báo cáo chẩn đoán

Move Prover sử dụng Ngôn ngữ đặc tả Move để mô tả hệ thống quy chuẩn, là một tập con của ngôn ngữ Move.

Tóm tắt

Ngôn ngữ Move đã xem xét đầy đủ về tính năng ngôn ngữ, thực thi máy ảo và công cụ an ninh. Nó có thể hiệu quả tránh được các lỗ hổng phổ biến như tái nhập, tràn, tiêm, nhưng vẫn không thể hoàn toàn tránh được vấn đề xác thực, logic. Khuyến nghị các nhà phát triển hợp đồng thông minh Move sử dụng dịch vụ kiểm toán an ninh bên thứ ba, và ủy thác việc viết mã quy chuẩn xác minh.