Phân tích độ an toàn của ngôn ngữ Move: Người cách mạng ngôn ngữ 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 blockchain thực hiện MoveVM. Nó đã được thiết kế với nhiều vấn đề an ninh của blockchain và hợp đồng thông minh ngay từ đầu, và tham khảo 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à an ninh, mức độ an ninh của nó như thế nào? Liệu nó có thể tránh được những 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? Liệu bản thân nó có tồn tại những vấn đề 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 thực.
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ó, ngôn ngữ Move được thiết kế để vừa hỗ trợ viết các chương trình tương tác an toàn với mã không đáng tin cậy, vừa hỗ trợ xác thực tĩnh. Move có những đặc điểm an toàn như vậy là vì nó 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, cũng không hỗ trợ gọi 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, v.v. để thực hiện một số mẫu lập trình thay thế. Ví dụ, Move đã bỏ qua các đặc điểm như lập lịch động và gọi đệ quy, những đặc điểm này trong các ngôn ngữ hợp đồng thông minh khác dẫn đến lỗ hổng reentrancy tốn kém.
Các tính năng bảo mật chính của Move bao gồm:
mô-đun (Module): Mỗi mô-đun Move bao gồm một loạt các kiểu cấu trúc và định nghĩa quy trình. Mô-đun có thể nhập các định nghĩa kiểu và gọi các quy trình được khai báo trong các mô-đun khác.
Cấu trúc ( Structs ): có thể được định nghĩa là loại tài nguyên, biểu thị có thể lưu trữ trong lưu trữ khóa/giá trị toàn cầu bền vững.
quá trình ( Chức năng ): định nghĩa logic kinh doanh của hợp đồng.
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/ghi theo cách lập trình bởi module sở hữu nó.
Kiểm tra bất biến: có thể định nghĩa bất biến kiểm tra tĩnh, biểu thị tính bảo tồn tài nguyên trong hệ thống.
Trình xác thực bytecode: thực hiện xác thực kiểu an toàn và tuyến tính cho bytecode, thi hành các quy tắc tạo, phá hủy và truy cập tài nguyên.
Thông qua những đặc điểm này, Move có thể đảm bảo tính an toàn cao ngay từ giai đoạn biên dịch. Tiếp theo, chúng ta sẽ phân tích cơ chế hoạt động của Move, xem MoveVM làm thế nào để đảm bảo tính an toàn trong thời gian thực.
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 vào bộ nhớ hệ thống trong quá trình thực thi. Điều này cho phép Move hoạt động an toàn trong môi trường không đáng tin cậy, không bị phá hoại hoặc lạm dụng.
Chương trình Move được thực hiện 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à bộ lưu trữ bậc một, không thể lưu trữ con trỏ trỏ tới các đơn vị bộ nhớ. Biến toàn cầu được sử dụng để lưu trữ con trỏ trỏ tới các đơn vị bộ nhớ, nhưng cách lập chỉ mục khác với bộ nhớ.
Các hướng dẫn bytecode của Move được thực thi trong bộ giải thích kiểu ngăn xếp. Máy ảo kiểu ngăn xếp dễ dàng để triển khai và kiểm soát, yêu cầu phần cứng thấp hơn, thích hợp cho các tình huống blockchain. Đồng thời, so với các bộ giải thích kiểu thanh ghi, bộ giải thích kiểu ngăn xếp dễ kiểm soát và phát hiện hơn trong việc sao chép và di chuyển giữa các biến.
Trạng thái thực thi của chương trình Move là một tứ hợp ⟨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òn duy trì một bảng hàm để phân tích các lệnh chứa thân hàm.
Ngăn xếp gọi chứa tất cả thông tin ngữ cảnh và số hiệu lệ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 được tạo ra, lưu trữ các tham số gọi, sau đó thực hiện các lệnh hợp đồng mới. Khi gặp lệnh phân nhánh, sẽ thực hiện nhảy tĩnh bên trong quá trình. Thiết kế này tránh việc phân phối động, tăng cường tính không thay đổi của việc gọi hàm, từ đó tránh khả năng gọi lại.
MoveVM tách biệt việc lưu trữ dữ liệu và ngăn xếp gọi quy trình logic ), đây là sự khác biệt lớn nhất so với EVM. Trong MoveVM, 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 theo các quy tắc bắt buộc liên quan đến quyền và tài nguyên. Thiết kế này mặc dù hy sinh một phần tính linh hoạt, nhưng đã đạt được sự nâng cao lớn về tính an toàn và hiệu suất thực thi.
3. Di chuyển Prover
Move Prover là một công cụ xác minh hình thức dựa trên suy diễn. 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 xem chương trình có đáp ứng mong đợi hay không, 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, từ đó 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 để xác minh xem chương trình có phù hợp với mong đợi hay không. Nó có thể suy luận hành vi của chương trình dựa trên thông tin đã biết và đả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 đúng đắn của chương trình và 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:
Nhận tệp nguồn Move làm đầu vào, tệp này cần thiết lập quy định đầu vào cho chương trình.
Move Parser từ mã nguồn trích xuất quy chuẩn.
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.
Mô hình này được dịch thành ngôn ngữ trung gian Boogie.
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.
Truyền điều kiện xác minh vào bộ giải Z3 để kiểm tra.
Nếu quy chuẩn được thiết lập, xác minh thành công; nếu không, tạo báo cáo chẩn đoán.
Để mô tả hệ thống quy chuẩn, Move sử dụng Ngôn ngữ Đặc tả Move, nó là một tập con của ngôn ngữ Move, giới thiệu hỗ trợ cho việc mô tả tĩnh hành vi đúng đắn của chương trình. Ngôn ngữ Đặc tả Move có thể được tách biệt thành các tệp quy chuẩn chuyên dụng, từ đó cho phép 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ụ 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. 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ó đáp ứng các mong đợi hay không. Điều này giúp giảm thiểu rủi ro giao dịch, khiến các nhà phát triển tự tin hơn 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, cung cấp các cân nhắc toàn diện ở cấp độ đặc điểm ngôn ngữ, thực thi máy ảo và công cụ an toàn. Ở đặc điểm ngôn ngữ, hy sinh một phần linh hoạt, kiểm tra kiểu bắt buộc và logic tuyến tính, thuận tiện hơn trong việc kiểm tra biên dịch, xác minh hình thức có tính tự động hóa và tính an toàn có thể xác minh. 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 trên blockchain.
Về mặt ngôn ngữ, Move có thể hiệu quả tránh khỏi các lỗ hổng phổ biến trong EVM như tái nhập, tràn, tiêm Call/DeleGateCall. Tuy nhiên, các vấn đề như xác thực, logic mã, 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. Move Prover mặc dù mạnh mẽ, nhưng có thể không phát huy tác dụng khi tổng thể ý chính bị lơ là.
Mặc dù ngôn ngữ Move đã xem xét nhiều vấn đề về 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. Khuyến nghị các nhà phát triển hợp đồng thông minh Move 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 mã specification được viết và xác minh bởi các công ty an ninh bên thứ ba, nhằm nâng cao thêm tính an toàn của hợp đồng.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
Phân tích độ sâu về tính an toàn của ngôn ngữ Move: tiêu chuẩn mới cho phát triển hợp đồng thông minh
Phân tích độ an toàn của ngôn ngữ Move: Người cách mạng ngôn ngữ 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 blockchain thực hiện MoveVM. Nó đã được thiết kế với nhiều vấn đề an ninh của blockchain và hợp đồng thông minh ngay từ đầu, và tham khảo 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à an ninh, mức độ an ninh của nó như thế nào? Liệu nó có thể tránh được những 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? Liệu bản thân nó có tồn tại những vấn đề 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 thực.
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ó, ngôn ngữ Move được thiết kế để vừa hỗ trợ viết các chương trình tương tác an toàn với mã không đáng tin cậy, vừa hỗ trợ xác thực tĩnh. Move có những đặc điểm an toàn như vậy là vì nó 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, cũng không hỗ trợ gọi 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, v.v. để thực hiện một số mẫu lập trình thay thế. Ví dụ, Move đã bỏ qua các đặc điểm như lập lịch động và gọi đệ quy, những đặc điểm này trong các ngôn ngữ hợp đồng thông minh khác dẫn đến lỗ hổng reentrancy tốn kém.
Các tính năng bảo mật chính của Move bao gồm:
mô-đun (Module): Mỗi mô-đun Move bao gồm một loạt các kiểu cấu trúc và định nghĩa quy trình. Mô-đun có thể nhập các định nghĩa kiểu và gọi các quy trình được khai báo trong các mô-đun khác.
Cấu trúc ( Structs ): có thể được định nghĩa là loại tài nguyên, biểu thị có thể lưu trữ trong lưu trữ khóa/giá trị toàn cầu bền vững.
quá trình ( Chức năng ): định nghĩa logic kinh doanh của hợp đồng.
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/ghi theo cách lập trình bởi module sở hữu nó.
Kiểm tra bất biến: có thể định nghĩa bất biến kiểm tra tĩnh, biểu thị tính bảo tồn tài nguyên trong hệ thống.
Trình xác thực bytecode: thực hiện xác thực kiểu an toàn và tuyến tính cho bytecode, thi hành các quy tắc tạo, phá hủy và truy cập tài nguyên.
Thông qua những đặc điểm này, Move có thể đảm bảo tính an toàn cao ngay từ giai đoạn biên dịch. Tiếp theo, chúng ta sẽ phân tích cơ chế hoạt động của Move, xem MoveVM làm thế nào để đảm bảo tính an toàn trong thời gian thực.
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 vào bộ nhớ hệ thống trong quá trình thực thi. Điều này cho phép Move hoạt động an toàn trong môi trường không đáng tin cậy, không bị phá hoại hoặc lạm dụng.
Chương trình Move được thực hiện 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à bộ lưu trữ bậc một, không thể lưu trữ con trỏ trỏ tới các đơn vị bộ nhớ. Biến toàn cầu được sử dụng để lưu trữ con trỏ trỏ tới các đơn vị bộ nhớ, nhưng cách lập chỉ mục khác với bộ nhớ.
Các hướng dẫn bytecode của Move được thực thi trong bộ giải thích kiểu ngăn xếp. Máy ảo kiểu ngăn xếp dễ dàng để triển khai và kiểm soát, yêu cầu phần cứng thấp hơn, thích hợp cho các tình huống blockchain. Đồng thời, so với các bộ giải thích kiểu thanh ghi, bộ giải thích kiểu ngăn xếp dễ kiểm soát và phát hiện hơn trong việc sao chép và di chuyển giữa các biến.
Trạng thái thực thi của chương trình Move là một tứ hợp ⟨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òn duy trì một bảng hàm để phân tích các lệnh chứa thân hàm.
Ngăn xếp gọi chứa tất cả thông tin ngữ cảnh và số hiệu lệ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 được tạo ra, lưu trữ các tham số gọi, sau đó thực hiện các lệnh hợp đồng mới. Khi gặp lệnh phân nhánh, sẽ thực hiện nhảy tĩnh bên trong quá trình. Thiết kế này tránh việc phân phối động, tăng cường tính không thay đổi của việc gọi hàm, từ đó tránh khả năng gọi lại.
MoveVM tách biệt việc lưu trữ dữ liệu và ngăn xếp gọi quy trình logic ), đây là sự khác biệt lớn nhất so với EVM. Trong MoveVM, 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 theo các quy tắc bắt buộc liên quan đến quyền và tài nguyên. Thiết kế này mặc dù hy sinh một phần tính linh hoạt, nhưng đã đạt được sự nâng cao lớn về tính an toàn và hiệu suất thực thi.
3. Di chuyển Prover
Move Prover là một công cụ xác minh hình thức dựa trên suy diễn. 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 xem chương trình có đáp ứng mong đợi hay không, 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, từ đó 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 để xác minh xem chương trình có phù hợp với mong đợi hay không. Nó có thể suy luận hành vi của chương trình dựa trên thông tin đã biết và đả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 đúng đắn của chương trình và 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:
Để mô tả hệ thống quy chuẩn, Move sử dụng Ngôn ngữ Đặc tả Move, nó là một tập con của ngôn ngữ Move, giới thiệu hỗ trợ cho việc mô tả tĩnh hành vi đúng đắn của chương trình. Ngôn ngữ Đặc tả Move có thể được tách biệt thành các tệp quy chuẩn chuyên dụng, từ đó cho phép 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ụ 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. 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ó đáp ứng các mong đợi hay không. Điều này giúp giảm thiểu rủi ro giao dịch, khiến các nhà phát triển tự tin hơn 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, cung cấp các cân nhắc toàn diện ở cấp độ đặc điểm ngôn ngữ, thực thi máy ảo và công cụ an toàn. Ở đặc điểm ngôn ngữ, hy sinh một phần linh hoạt, kiểm tra kiểu bắt buộc và logic tuyến tính, thuận tiện hơn trong việc kiểm tra biên dịch, xác minh hình thức có tính tự động hóa và tính an toàn có thể xác minh. 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 trên blockchain.
Về mặt ngôn ngữ, Move có thể hiệu quả tránh khỏi các lỗ hổng phổ biến trong EVM như tái nhập, tràn, tiêm Call/DeleGateCall. Tuy nhiên, các vấn đề như xác thực, logic mã, 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. Move Prover mặc dù mạnh mẽ, nhưng có thể không phát huy tác dụng khi tổng thể ý chính bị lơ là.
Mặc dù ngôn ngữ Move đã xem xét nhiều vấn đề về 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. Khuyến nghị các nhà phát triển hợp đồng thông minh Move 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 mã specification được viết và xác minh bởi các công ty an ninh bên thứ ba, nhằm nâng cao thêm tính an toàn của hợp đồng.