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

Lời mở đầu

Move là một ngôn ngữ hợp đồng thông minh có thể chạy trong môi trường blockchain thực hiện MoveVM. Ngay từ khi ra đời, nó đã xem xét nhiều vấn đề an ninh của blockchain và hợp đồng thông minh, đồng thời tham khảo một số thiết kế an ninh của ngôn ngữ RUST. Là một ngôn ngữ hợp đồng thông minh thế hệ mới với đặc điểm chính là tính an toàn, Move có độ an toàn như thế nào? Liệu nó có thể tránh được các mối đe dọa an ninh phổ biến của các máy ảo hợp đồng như EVM, WASM ở cấp độ ngôn ngữ hoặc cơ chế liên quan không? Nó có tồn tại những rủi ro an ninh đặc thù nào không?

Bài viết này sẽ khám phá vấn đề an ninh 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 minh.

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

Khác với nhiều ngôn ngữ lập trình hiện có, Move được thiết kế để vừa hỗ trợ tương tác an toàn với mã không đáng tin cậy, vừa hỗ trợ xác minh tĩnh. Move có những đặc điểm an toàn này vì nó loại 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, cũng như không hỗ trợ gọi bên ngoài đệ quy, mà thay vào đó 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ế. Ví dụ, Move loại bỏ các tính năng lập lịch động và gọi đệ quy có thể dẫn đến lỗ hổng tái nhập.

Các tính năng an toàn chính của Move bao gồm:

1. Mô-đun (Module): Mỗi mô-đun Move bao gồm một loạt các loại cấu trúc và định nghĩa quy trình. Mô-đun có thể nhập các định nghĩa loại được khai báo bởi các mô-đun khác và gọi quy trình của chúng.

2. Cấu trúc (: có thể được định nghĩa là loại tài nguyên, biểu thị cho những gì có thể lưu trữ trong kho khóa/giá trị toàn cầu bền vững.

3. quá trình )function (: định nghĩa chức năng cụ thể của mô-đun.

4. 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, những dữ liệu này chỉ có thể được đọc và ghi theo cách lập trình bởi các mô-đun sở hữu nó.

5. Kiểm tra bất biến: có thể định nghĩa kiểm tra tĩnh bất biến, đảm bảo tính toàn vẹn của tài nguyên trong hệ thống.

6. Trình xác thực bytecode: xác thực loại an toàn và tuyến tính, ngăn chặn việc tạo, sửa đổi hoặc tiêu hủy giá trị nhạy cảm một cách trái phép.

![Phân tích an toàn Move: Thay đổi cuộc chơi ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

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. Chương trình thực thi trên ngăn xếp, bộ nhớ toàn cầu được chia thành hai phần: bộ nhớ ), ngăn xếp ( và biến toàn cục ).

Hướng dẫn bytecode của Move được thực thi trong bộ thông dịch kiểu ngăn xếp, cách này dễ dàng để triển khai và kiểm soát, yêu cầu phần cứng thấp, phù hợp với các tình huống blockchain. Đồng thời, so với bộ thông dịch kiểu thanh ghi, bộ thông dịch kiểu ngăn xếp dễ dàng hơn trong việc kiểm soát và phát hiện việc sao chép và di chuyển giữa các biến.

Trong quá trình thực thi, trạng thái của chương trình Move đượ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. Ngăn xếp gọi chứa tất cả thông tin ngữ cảnh của quá trình thực thi. Khi thực hiện lệnh Call, một đối tượng ngăn xếp gọi mới sẽ được tạo ra. Khi gặp lệnh phân nhánh, sẽ có một sự nhảy tĩnh trong nội bộ quá trình.

Khác với EVM, MoveVM tách biệt việc lưu trữ dữ liệu và ngăn xếp gọi, phù hợp hơn với nhu cầu quản lý an toàn tài sản trên blockchain. Thiết kế này mang lại sự cải thiện lớn về tính bảo mật và hiệu suất thực thi.

3. Move Prover

Move Prover là một công cụ xác minh hình thức dựa trên suy diễn, sử dụng ngôn ngữ hình thức để mô tả hành vi chương trình và sử dụng thuật toán suy diễn để xác minh xem chương trình có phù hợp với mong đợi hay không. Nó có thể giúp các nhà phát triển đảm bảo tính chính xác của hợp đồng thông minh, giảm thiểu rủi ro giao dịch.

Move Prover sử dụng thuật toán xác minh suy diễn, dựa trên thông tin đã biết để suy ra hành vi của chương trình, đảm bảo nó khớp với hành vi dự kiến. Điều này giúp đảm bảo tính chính xác của chương trình, giảm khối lượng công việc kiểm tra thủ công.

Quy trình làm việc của Move Prover như sau:

1. Nhận tệp nguồn Move làm đầu vào
2. Trích xuất quy chuẩn và biên dịch thành mã byte
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 thực
6. Sử dụng trình giải Z3 để xác minh công thức SMT
7. Tạo báo cáo chẩn đoán và phục hồi thành lỗi cấp mã nguồn

Ngôn ngữ đặc tả Move được sử dụng để mô tả hệ thống quy định, là một tập con của ngôn ngữ Move, hỗ trợ mô tả tĩnh hành vi đúng đắn của chương trình.

Nói chung, Move Prover là một công cụ rất hữu ích, có thể giúp các nhà phát triển đảm bảo tính chính xác của hợp đồng thông minh, giảm thiểu rủi ro giao dịch và tăng cường sự tự tin khi triển khai hợp đồng thông minh.

4. Tóm tắt

Ngôn ngữ Move có thiết kế an toàn rất xuất sắc, đã xem xét toàn diện ở các khía cạnh như tính năng ngôn ngữ, thực thi máy ảo và công cụ an toàn. Nó hy sinh một phần tính linh hoạt, kiểm tra kiểu bắt buộc và logic tuyến tính, thuận tiện cho việc kiểm tra biên dịch và xác minh hình thức. MoveVM tách biệt trạng thái và logic, phù hợp hơn với nhu cầu quản lý an toàn tài sản blockchain.

Ngôn ngữ Move có thể hiệu quả trong việc tránh các lỗ hổng phổ biến trong EVM như tấn công tái nhập, tràn số, tiêm Call/DeleGateCall. Tuy nhiên, các vấn đề như xác thực, logic mã, và tràn cấu trúc số lớn vẫn cần sự chú ý thêm từ các nhà phát triển. Mặc dù Move Prover cung cấp xác minh hình thức, nhưng không thể bù đắp cho những thiếu sót trong thiết kế tổng thể.

Mặc dù Move đã xem xét nhiều khía cạnh về an ninh, nhưng không có ngôn ngữ và chương trình nào hoàn toàn an toàn. Đề xuất các nhà phát triển hợp đồng thông minh Move vẫn nên sử dụng dịch vụ kiểm toán của các công ty an ninh bên thứ ba và để phần viết và xác minh quy định cho các đội ngũ an ninh chuyên nghiệp.