Phân tích an toàn ngôn ngữ Move: Nhà cách mạng trong 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 từ khi bắt đầu, và đã tham khảo một số nguyên tắc 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, tính an toàn của Move như thế nào? 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? Liệu Move có tồn tại những rủi ro an ninh độc đáo nào không?
Bài viết này sẽ thảo luận về 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. Các 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 thực tĩnh. Move đạt được mục tiêu này bằng cách từ bỏ tất cả các 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 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 một số mô hình lập trình thay thế.
Dưới đây là một số tính năng bảo mật chính của ngôn ngữ Move:
Tính mô-đun: 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 kiểu được khai báo trong mô-đun khác và gọi các quy trình của nó.
Loại tài nguyên: Cấu trúc được định nghĩa bằng cú pháp has key là loại tài nguyên, có thể được lưu trữ trong kho khóa-giá trị toàn cục bền vững.
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ó, nhưng được lưu trữ trong sổ cái công cộng có thể được các mô-đun khác xem.
Hệ thống kiểu tĩnh: Move có một hệ thống kiểu tĩnh mạnh mẽ, có thể phát hiện nhiều lỗi trong quá trình biên dịch.
Loại tuyến tính: Loại tài nguyên mặc định là loại tuyến tính, ngăn chặn việc sao chép hoặc hủy bỏ ngầm.
Quy tắc bất biến: có thể định nghĩa bất biến bảo tồn trạng thái, dùng để xác minh hình thức.
Trình xác thực bytecode: Thực thi hệ thống kiểu ở cấp độ bytecode, ngăn chặn hành vi độc hại.
Những đặc điểm này cùng nhau xây dựng nền tảng an toàn cho ngôn ngữ Move, giúp nó tránh được nhiều lỗ hổng hợp đồng thông minh phổ biến.
2. Cơ chế vận hành 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 thực thi an toàn trong môi trường không đáng tin cậy.
Move sử dụng trình thông dịch kiểu ngăn xếp để thực thi các chỉ thị bytecode. Trạng thái của nó bao gồm ngăn gọi, bộ nhớ, biến toàn cục và ngăn chứa toán hạng. Thiết kế này giúp việc sao chép và di chuyển giữa các biến dễ dàng kiểm soát và phát hiện hơn.
MoveVM tách biệt việc lưu trữ dữ liệu và ngăn xếp gọi, đây là sự khác biệt lớn nhất giữa nó và 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 và tài nguyên. Thiết kế này hy sinh một phần sự linh hoạt, nhưng cải thiện đáng kể tính bảo mật và hiệu suất thực thi.
![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-372ff914a241634ca57784dc9685a03d.webp(
3. Chuyển Prover
Move Prover là công cụ xác minh hình thức của 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 hành vi mong đợi hay không. Nó có thể suy luận hành vi chương trình dựa trên thông tin đã biết, đảm bảo rằng nó khớp với mong đợi, giúp đảm bảo tính đúng đắn của chương trình và 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:
Nhận tệp nguồn Move làm đầu vào, tệp này cần chứa các yêu cầu chương trình.
Trích xuất quy chuẩn và biên dịch tệp nguồn thành mã byte.
Chuyển đổi các quy chuẩn và mã byte thành mô hình đối tượng xác thực.
Dịch mô hình sang ngôn ngữ trung gian Boogie.
Hệ thống xác minh Boogie tạo ra các điều kiện xác minh.
Bộ giải Z3 kiểm tra xem các điều kiện xác minh có được thỏa mãn hay không.
Tạo báo cáo chẩn đoán và chuyển đổi thành lỗi mức mã nguồn.
Ngôn ngữ đặc tả Move được sử dụng để mô tả quy định chương trình, là một tập con của ngôn ngữ Move. Nó hỗ trợ mô tả tĩnh hành vi đúng đắn của chương trình, không ảnh hưởng đến mã sản xuất. Các quy định có thể được viết độc lập, thuận tiện cho việc tách biệt mã kinh doanh và mã xác minh.
![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(
4. Tóm tắt
Ngôn ngữ Move có thiết kế rất xuất sắc về mặt an toàn, từ các đặc điểm ngôn ngữ, thực thi máy ảo đến các công cụ an ninh đều được xem xét một cách toàn diện. Nó đã hy sinh một phần tính linh hoạt, tăng cường kiểm tra kiểu 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 xác minh hình thức. Thiết kế của 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ả tránh được các lỗ hổng thường gặp trong EVM như 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 được các nhà phát triển chú ý thêm. Mặc dù Move đã xem xét kỹ lưỡng về mặt 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 là an toàn tuyệt đối. 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 của các công ty an ninh bên thứ ba, và giao việc viết mã chuẩn và xác thực cho các đội ngũ an ninh chuyên nghiệp.
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.
17 thích
Phần thưởng
17
5
Đăng lại
Chia sẻ
Bình luận
0/400
OptionWhisperer
· 07-15 10:34
Nhanh chóng đến giá sàn xem move
Xem bản gốcTrả lời0
NftCollectors
· 07-14 08:08
Move bẫy an toàn này không thua kém tỷ lệ vàng trong nghệ thuật Byzantine, từ góc độ lịch sử nghệ thuật Blockchain, hoàn toàn là một cột mốc.
Xem bản gốcTrả lời0
BearMarketSurvivor
· 07-14 03:19
An toàn chỉ là những lời nói suông.
Xem bản gốcTrả lời0
ForkTongue
· 07-14 03:08
Có đồ chơi mới để viết hợp đồng rồi sao?
Xem bản gốcTrả lời0
FancyResearchLab
· 07-14 03:05
Một cái hố mới mà Lỗ Ban thích, lý thuyết thì cũng khá an toàn.
Phân tích an toàn 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 ngôn ngữ Move: Nhà cách mạng trong 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 từ khi bắt đầu, và đã tham khảo một số nguyên tắc 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, tính an toàn của Move như thế nào? 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? Liệu Move có tồn tại những rủi ro an ninh độc đáo nào không?
Bài viết này sẽ thảo luận về 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. Các 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 thực tĩnh. Move đạt được mục tiêu này bằng cách từ bỏ tất cả các 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 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 một số mô hình lập trình thay thế.
Dưới đây là một số tính năng bảo mật chính của ngôn ngữ Move:
Tính mô-đun: 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 kiểu được khai báo trong mô-đun khác và gọi các quy trình của nó.
Loại tài nguyên: Cấu trúc được định nghĩa bằng cú pháp has key là loại tài nguyên, có thể được lưu trữ trong kho khóa-giá trị toàn cục bền vững.
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ó, nhưng được lưu trữ trong sổ cái công cộng có thể được các mô-đun khác xem.
Hệ thống kiểu tĩnh: Move có một hệ thống kiểu tĩnh mạnh mẽ, có thể phát hiện nhiều lỗi trong quá trình biên dịch.
Loại tuyến tính: Loại tài nguyên mặc định là loại tuyến tính, ngăn chặn việc sao chép hoặc hủy bỏ ngầm.
Quy tắc bất biến: có thể định nghĩa bất biến bảo tồn trạng thái, dùng để xác minh hình thức.
Trình xác thực bytecode: Thực thi hệ thống kiểu ở cấp độ bytecode, ngăn chặn hành vi độc hại.
Những đặc điểm này cùng nhau xây dựng nền tảng an toàn cho ngôn ngữ Move, giúp nó tránh được nhiều lỗ hổng hợp đồng thông minh phổ biến.
2. Cơ chế vận hành 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 thực thi an toàn trong môi trường không đáng tin cậy.
Move sử dụng trình thông dịch kiểu ngăn xếp để thực thi các chỉ thị bytecode. Trạng thái của nó bao gồm ngăn gọi, bộ nhớ, biến toàn cục và ngăn chứa toán hạng. Thiết kế này giúp việc sao chép và di chuyển giữa các biến dễ dàng kiểm soát và phát hiện hơn.
MoveVM tách biệt việc lưu trữ dữ liệu và ngăn xếp gọi, đây là sự khác biệt lớn nhất giữa nó và 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 và tài nguyên. Thiết kế này hy sinh một phần sự linh hoạt, nhưng cải thiện đáng kể tính bảo mật và hiệu suất thực thi.
![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-372ff914a241634ca57784dc9685a03d.webp(
3. Chuyển Prover
Move Prover là công cụ xác minh hình thức của 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 hành vi mong đợi hay không. Nó có thể suy luận hành vi chương trình dựa trên thông tin đã biết, đảm bảo rằng nó khớp với mong đợi, giúp đảm bảo tính đúng đắn của chương trình và 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:
Ngôn ngữ đặc tả Move được sử dụng để mô tả quy định chương trình, là một tập con của ngôn ngữ Move. Nó hỗ trợ mô tả tĩnh hành vi đúng đắn của chương trình, không ảnh hưởng đến mã sản xuất. Các quy định có thể được viết độc lập, thuận tiện cho việc tách biệt mã kinh doanh và mã xác minh.
![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(
4. Tóm tắt
Ngôn ngữ Move có thiết kế rất xuất sắc về mặt an toàn, từ các đặc điểm ngôn ngữ, thực thi máy ảo đến các công cụ an ninh đều được xem xét một cách toàn diện. Nó đã hy sinh một phần tính linh hoạt, tăng cường kiểm tra kiểu 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 xác minh hình thức. Thiết kế của 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ả tránh được các lỗ hổng thường gặp trong EVM như 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 được các nhà phát triển chú ý thêm. Mặc dù Move đã xem xét kỹ lưỡng về mặt 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 là an toàn tuyệt đối. 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 của các công ty an ninh bên thứ ba, và giao việc viết mã chuẩn và xác thực cho các đội ngũ an ninh chuyên nghiệp.