Phân tích an ninh ngôn ngữ Move: kẻ thay đổi quy tắc trò chơi của ngôn ngữ hợp đồng thông minh
Ngôn ngữ Move là một loại ngôn ngữ hợp đồng thông minh có thể được biên dịch và chạy trong môi trường blockchain triển khai MoveVM. Ngay từ khi ra đời, nó đã xem xét nhiều vấn đề liên quan đến an toàn của blockchain và hợp đồng thông minh, và đã tham khảo một số 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 chính là an toàn, an toàn của Move thực sự như thế nào? Liệu nó có thể tránh được những mối đe dọa an toàn thường gặp trong 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 nó có tồn tại những rủi ro an toàn đặc thù 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ế vận hành 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ó, mục tiêu thiết kế của ngôn ngữ Move là hỗ trợ việc 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. Để đạt được mục tiêu này, 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 ngoại lệ đệ 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, v.v. để thực hiện các mô hình lập trình thay thế. Ví dụ, Move đã bỏ qua các đặc điểm lập lịch động và gọi đệ quy, những đặc điểm này có thể dẫn đến các lỗ hổng gọi lại tốn kém 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:
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 trong mô-đun khác và gọi quy trình.
Cấu trúc (Structs): có thể được định nghĩa là loại tài nguyên, đại diện cho những gì có thể được lưu trữ trong kho lưu trữ khóa/giá trị toàn cầu vĩnh viễn.
过程(Function): định nghĩa logic hành vi của module.
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à ghi theo cách lập trình bởi mô-đun 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, đảm bảo tính bảo toàn của trạng thái hệ thống.
Trình kiểm tra mã byte: Thực thi hệ thống kiểu ở cấp độ mã byte, ngăn chặn các thao tác trái phép.
Move đảm bảo tính an toàn của mã nguồn ngay từ giai đoạn biên dịch thông qua những đặc điểm này. 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 quá trình thực thi.
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 hoạt động an toàn trong môi trường không tin cậy. Chương trình Move thực thi trên ngăn xếp, bộ nhớ toàn cục được chia thành bộ nhớ ( và ngăn xếp biến toàn cục ). Bộ nhớ là bộ lưu trữ bậc một, không thể lưu trữ con trỏ đến các ô bộ nhớ. Biến toàn cục được sử dụng để lưu trữ con trỏ đến các ô bộ nhớ, nhưng cách lập chỉ mục khác với bộ nhớ.
Mã byte của Move được thực hiện trong bộ thông dị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, phù hợp với các tình huống blockchain. 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 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 chương trình Move, trạng thái của nó 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 hàm ( của chính mô-đun ) để phân giải các lệnh chứa thân hàm.
MoveVM tách biệt logic quy trình lưu trữ dữ liệu và ngăn xếp gọi (, đây là sự khác biệt lớn nhất 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 thủ các quy tắc bắt buộc liên quan đến quyền hạn và tài nguyên. Mặc dù điều này hy sinh một chút linh hoạt, nhưng về mặt an ninh và hiệu suất thực thi ) đã giúp đạt được sự cải thiện lớn trong việc thực hiện đồng thời (.
![Phân tích an toàn Move: Game Changer của ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. 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ó phù hợp với 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 thực suy diễn để xác minh chương trình có đáp ứng mong đợi hay không. Điều này có nghĩa là, Move Prover 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ó khớ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 thử nghiệm 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 được thiết lập theo quy định đầu vào của chương trình )specification(.
Move Parser từ mã nguồn trích xuất quy chuẩn.
Trình biên dịch Move sẽ biên dịch tệp nguồn thành bytecode, 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 )Prover Object Model(.
Dịch mô hình sang ngôn ngữ trung gian Boogie.
Hệ thống xác thực Boogie thực hiện "hợp đồng thông minh" điều kiện đầu vào )verification condition generation(.
Truyền điều kiện xác minh vào Z3 solver ) bộ giải SMT do Microsoft phát triển (.
Z3 kiểm tra mã chương trình SMT ) có thỏa mãn specification ( hay không.
Nếu không thể thỏa mãn, cho thấy quy chuẩn đã được thiết lập; ngược lại, tạo ra mô hình thỏa mãn điều kiện, chuyển đổi về định dạng Boogie để phát hành báo cáo chẩn đoán.
Khôi phục báo cáo chẩn đoán thành lỗi cấp mã nguồn.
Move sử dụng Ngôn ngữ Đặc tả Move để mô tả hệ thống quy chuẩn. Ngôn ngữ này là một tập con của Move, hỗ trợ mô tả tĩnh hành vi đúng đắn của chương trình mà không ảnh hưởng đến sản xuất. Có thể độc lập viết các tài liệu quy chuẩn chuyên biệt, tách biệt mã nguồn kinh doanh và mã xác minh hình thức.
Move Prover là một công cụ hữu ích, 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 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ó phù hợp với mong đợi hay không. Điều này giúp giảm rủi ro giao dịch, cho phép 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.
![Phân tích an toàn Move: Thay đổi cuộc chơi của ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
4. Tóm tắt
Ngôn ngữ Move có thiết kế an toàn rất xuất sắc, đã được xem xét toàn diện ở các khía cạnh đặc tính ngôn ngữ, thực thi máy ảo và công cụ an ninh. Đặc tính 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, thuận tiện cho việc kiểm tra biên dịch và tự động hóa cũng như khả năng xác minh an toàn. 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 được các lỗ hổng thường gặp trong EVM như tấn công gọi lại, 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 được các nhà phát triển chú ý. Move Prover có thể không hoạt động khi có sự lơ là tổng thể về ý nghĩa.
Mặc dù ngôn ngữ Move đã xem xét nhiều điều cho lập trình viên về mặt an ninh, nhưng không có ngôn ngữ nào hoàn toàn an toàn, cũng như không có chương trình nào hoàn toàn an toàn. Các nhà phát triển hợp đồng thông minh Move được khuyến nghị 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 phần mã specification cho các công ty an ninh bên thứ ba.
![Phân tích an toàn Move: Thay đổi cuộc chơi của ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
Trang này có thể chứa nội dung của bên thứ ba, được cung cấp chỉ nhằm mục đích thông tin (không phải là tuyên bố/bảo đảm) và không được coi là sự chứng thực cho quan điểm của Gate hoặc là lời khuyên về tài chính hoặc chuyên môn. Xem Tuyên bố từ chối trách nhiệm để biết chi tiết.
21 thích
Phần thưởng
21
3
Chia sẻ
Bình luận
0/400
AirdropBlackHole
· 07-20 03:29
3 năm Người khai thác tìm một người có duyên dẫn dắt!
Xem bản gốcTrả lời0
PumpBeforeRug
· 07-20 03:29
Nhìn xem move này, thú cưng mới, còn có thể ngăn chặn lỗ hổng.
Phân tích tính an toàn của ngôn ngữ Move: Vệ sĩ an toàn mới cho hợp đồng thông minh
Phân tích an ninh ngôn ngữ Move: kẻ thay đổi quy tắc trò chơi của ngôn ngữ hợp đồng thông minh
Ngôn ngữ Move là một loại ngôn ngữ hợp đồng thông minh có thể được biên dịch và chạy trong môi trường blockchain triển khai MoveVM. Ngay từ khi ra đời, nó đã xem xét nhiều vấn đề liên quan đến an toàn của blockchain và hợp đồng thông minh, và đã tham khảo một số 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 chính là an toàn, an toàn của Move thực sự như thế nào? Liệu nó có thể tránh được những mối đe dọa an toàn thường gặp trong 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 nó có tồn tại những rủi ro an toàn đặc thù 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ế vận hành 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ó, mục tiêu thiết kế của ngôn ngữ Move là hỗ trợ việc 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. Để đạt được mục tiêu này, 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 ngoại lệ đệ 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, v.v. để thực hiện các mô hình lập trình thay thế. Ví dụ, Move đã bỏ qua các đặc điểm lập lịch động và gọi đệ quy, những đặc điểm này có thể dẫn đến các lỗ hổng gọi lại tốn kém 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:
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 trong mô-đun khác và gọi quy trình.
Cấu trúc (Structs): có thể được định nghĩa là loại tài nguyên, đại diện cho những gì có thể được lưu trữ trong kho lưu trữ khóa/giá trị toàn cầu vĩnh viễn.
过程(Function): định nghĩa logic hành vi của module.
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à ghi theo cách lập trình bởi mô-đun 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, đảm bảo tính bảo toàn của trạng thái hệ thống.
Trình kiểm tra mã byte: Thực thi hệ thống kiểu ở cấp độ mã byte, ngăn chặn các thao tác trái phép.
Move đảm bảo tính an toàn của mã nguồn ngay từ giai đoạn biên dịch thông qua những đặc điểm này. 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 quá trình thực thi.
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 hoạt động an toàn trong môi trường không tin cậy. Chương trình Move thực thi trên ngăn xếp, bộ nhớ toàn cục được chia thành bộ nhớ ( và ngăn xếp biến toàn cục ). Bộ nhớ là bộ lưu trữ bậc một, không thể lưu trữ con trỏ đến các ô bộ nhớ. Biến toàn cục được sử dụng để lưu trữ con trỏ đến các ô bộ nhớ, nhưng cách lập chỉ mục khác với bộ nhớ.
Mã byte của Move được thực hiện trong bộ thông dị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, phù hợp với các tình huống blockchain. 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 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 chương trình Move, trạng thái của nó 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 hàm ( của chính mô-đun ) để phân giải các lệnh chứa thân hàm.
MoveVM tách biệt logic quy trình lưu trữ dữ liệu và ngăn xếp gọi (, đây là sự khác biệt lớn nhất 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 thủ các quy tắc bắt buộc liên quan đến quyền hạn và tài nguyên. Mặc dù điều này hy sinh một chút linh hoạt, nhưng về mặt an ninh và hiệu suất thực thi ) đã giúp đạt được sự cải thiện lớn trong việc thực hiện đồng thời (.
![Phân tích an toàn Move: Game Changer của ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. 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ó phù hợp với 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 thực suy diễn để xác minh chương trình có đáp ứng mong đợi hay không. Điều này có nghĩa là, Move Prover 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ó khớ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 thử nghiệm 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 được thiết lập theo quy định đầu vào của chương trình )specification(.
Move Parser từ mã nguồn trích xuất quy chuẩn.
Trình biên dịch Move sẽ biên dịch tệp nguồn thành bytecode, 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 )Prover Object Model(.
Dịch mô hình sang ngôn ngữ trung gian Boogie.
Hệ thống xác thực Boogie thực hiện "hợp đồng thông minh" điều kiện đầu vào )verification condition generation(.
Truyền điều kiện xác minh vào Z3 solver ) bộ giải SMT do Microsoft phát triển (.
Z3 kiểm tra mã chương trình SMT ) có thỏa mãn specification ( hay không.
Nếu không thể thỏa mãn, cho thấy quy chuẩn đã được thiết lập; ngược lại, tạo ra mô hình thỏa mãn điều kiện, chuyển đổi về định dạng Boogie để phát hành báo cáo chẩn đoán.
Khôi phục báo cáo chẩn đoán thành lỗi cấp mã nguồn.
Move sử dụng Ngôn ngữ Đặc tả Move để mô tả hệ thống quy chuẩn. Ngôn ngữ này là một tập con của Move, hỗ trợ mô tả tĩnh hành vi đúng đắn của chương trình mà không ảnh hưởng đến sản xuất. Có thể độc lập viết các tài liệu quy chuẩn chuyên biệt, tách biệt mã nguồn kinh doanh và mã xác minh hình thức.
Move Prover là một công cụ hữu ích, 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 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ó phù hợp với mong đợi hay không. Điều này giúp giảm rủi ro giao dịch, cho phép 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.
![Phân tích an toàn Move: Thay đổi cuộc chơi của ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
4. Tóm tắt
Ngôn ngữ Move có thiết kế an toàn rất xuất sắc, đã được xem xét toàn diện ở các khía cạnh đặc tính ngôn ngữ, thực thi máy ảo và công cụ an ninh. Đặc tính 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, thuận tiện cho việc kiểm tra biên dịch và tự động hóa cũng như khả năng xác minh an toàn. 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 được các lỗ hổng thường gặp trong EVM như tấn công gọi lại, 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 được các nhà phát triển chú ý. Move Prover có thể không hoạt động khi có sự lơ là tổng thể về ý nghĩa.
Mặc dù ngôn ngữ Move đã xem xét nhiều điều cho lập trình viên về mặt an ninh, nhưng không có ngôn ngữ nào hoàn toàn an toàn, cũng như không có chương trình nào hoàn toàn an toàn. Các nhà phát triển hợp đồng thông minh Move được khuyến nghị 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 phần mã specification cho các công ty an ninh bên thứ ba.
![Phân tích an toàn Move: Thay đổi cuộc chơi của ngôn ngữ hợp đồng thông minh])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(