Phân tích an ninh ngôn ngữ Move: Người đổi mới trong lĩnh vực hợp đồng thông minh

Ngôn ngữ Move là một ngôn ngữ hợp đồng thông minh có thể chạy trong môi trường chuỗi khối hỗ trợ MoveVM. Thiết kế của nó đã xem xét nhiều vấn đề an toàn của chuỗi khối và hợp đồng thông minh, đồng thời tham khảo một số nguyên tắc thiết kế an toàn 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 an toàn là cốt lõi, tính an toàn của Move thực sự ra sao? Nó có thể tránh được các mối đe dọa an toàn 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? Liệu Move có tồn tại những rủi ro an toàn độc đáo nào không?

Bài viết này sẽ thảo luận về vấn đề 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 minh.

1. Tính năng an toàn của ngôn ngữ Move

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

Các tính năng bảo mật cốt lõi của Move bao gồm:

1. Mô-đun: Mỗi mô-đun Move đượ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. Mô-đun có thể nhập các định nghĩa loại được khai báo trong các mô-đun khác và gọi các quy trình.

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ể được lưu trữ trong kho khóa/giá trị toàn cầu vĩnh viễn.

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

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

6. Trình xác minh bytecode: Thực thi hệ thống kiểu tại cấp độ bytecode, ngăn chặn các thao tác bất hợp pháp.

Thông qua những tính năng bảo mật này, Move cung cấp một môi trường lập trình an toàn và đáng tin cậy hơn cho việc phát triển hợp đồng thông minh.

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 cho phép Move chạy an toàn trong môi trường không đáng tin cậy.

Chương trình Move 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ầu (. Bộ nhớ là lưu trữ cấp một, không thể lưu trữ con trỏ đến các ô nhớ. Biến toàn cầu được sử dụng để lưu trữ con trỏ đến các ô nhớ, nhưng cách chỉ mục thì khác với bộ nhớ.

Bytecode instructions của Move được thực thi trong trình thông dịch kiểu ngăn xếp. So với trình thông dịch kiểu thanh ghi, trình 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 các thao tác sao chép và di chuyển giữa các biến.

Trạng thái khi chạy chương trình Move là một bộ tứ ⟨C, M, G, S⟩, bao gồm ngăn xếp gọi )C(, bộ nhớ )M(, biến toàn cục )G( và toán hạng )S(. Ngăn xếp cũng duy trì bảng chức năng để giải mã các lệnh chứa thân hàm.

MoveVM tách biệt logic quy trình lưu trữ và ngăn xếp gọi dữ liệu ), đây là sự khác biệt chính với EVM. Tài nguyên ( dưới địa chỉ tài khoản trạng thái người dùng ) được lưu trữ độc lập, việc gọi chương trình phải tuân thủ các quy tắc bắt buộc liên quan đến quyền hạn và tài nguyên. Thiết kế này mặc dù hy sinh một phần linh hoạt, nhưng đã đạt được sự nâng cao đáng kể về an toàn và hiệu suất thực thi.

3. Chuyển Prover

Move Prover là một công cụ xác thực 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 của chương trình, và sử dụng thuật toán suy diễn để xác minh liệu 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ó phù hợp với hành vi mong đợi. Điều này giúp đảm bảo tính chính xác của chương trình, giảm bớt 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, trong đó chứa thông số đầu vào chương trình.

2. Move Parser trích xuất các quy định trong mã nguồn.

3. Trình biên dịch Move biên dịch tệp nguồn thành mã byte, cùng với hệ thống quy chuẩn chuyển đổi thành mô hình đối tượng xác thực.

4. Mô hình đối tượng được dịch sang ngôn ngữ trung gian Boogie.

5. Hệ thống xác thực Boogie thực hiện "tạo điều kiện xác thực" cho đầu vào.

6. Truyền điều kiện xác thực vào bộ giải Z3 ( bộ giải SMT được phát triển bởi Microsoft ).

7. Z3 kiểm tra xem công thức SMT có thể không thỏa mãn hay không. Nếu có, điều đó có nghĩa là quy chuẩn đã được xác nhận; nếu không, tạo ra mô hình thỏa mãn điều kiện.

8. Khôi phục báo cáo chẩn đoán về lỗi cấp mã nguồn.

Move sử dụng Ngôn ngữ Đặc tả Move để mô tả hệ thống, đây 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, không ảnh hưởng đến sản xuất. Các đặc tả có thể được viết độc lập, thuận tiện cho việc tách biệt mã nghiệp vụ và mã xác minh hình thức.

Move Prover là một công cụ mạnh mẽ, 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 vào môi trường sản xuất.

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 từ các đặc điểm ngôn ngữ, việc thực thi máy ảo đến các công cụ an toàn. Đặc điểm ngôn ngữ đã 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, có lợi cho việc tự động hóa và khả năng xác minh của kiểm tra biên dịch và xác minh hình thức. Thiết kế 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.

Về mặt ngôn ngữ, Move có thể hiệu quả tránh được các lỗ hổng phổ biến của EVM như tấn công tái nhập, tràn số, tiêm Call/DeleGateCall, v.v. 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 phụ thuộc vào sự cẩn thận của nhà phát triển. Move Prover mặc dù mạnh mẽ, nhưng có thể không phát huy tác dụng khi thiết kế tổng thể bị lơ là.

Mặc dù ngôn ngữ Move cung cấp nhiều bảo đảm an toàn cho lập trình viên, 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à giao việc viết và xác minh mã phần specification cho đội ngũ an ninh chuyên nghiệp, nhằm nâng cao hơn nữa độ an toàn của hợp đồng.