Phân tích tính an toàn của ngôn ngữ Move: Người biến đổi trong lĩnh vực hợp đồng thông minh

Ngôn ngữ Move, như một ngôn ngữ hợp đồng thông minh thế hệ mới, đã coi tính an toàn là yếu tố được xem xét hàng đầu ngay từ giai đoạn thiết kế. Bài viết này sẽ bàn luận về tính 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. Các tính năng bảo mật của ngôn ngữ Move

Ngôn ngữ Move thông qua việc từ bỏ một số tính năng linh hoạt, áp 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ô hình lập trình an toàn. Các tính năng bảo mật chính của nó bao gồm:

• Thiết kế mô-đun, mỗi mô-đun được cấu thành từ loại cấu trúc và định nghĩa quy trình.
• Cấu trúc loại tài nguyên, có thể lưu trữ trong khoá giá trị toàn cầu
• Cơ chế lưu trữ toàn cầu, cho phép mô-đun truy cập độc quyền vào tài nguyên mà nó đã khai báo.
• Quy tắc bất biến, dùng để kiểm tra tính bảo toàn của trạng thái hệ thống.
• Trình xác thực bytecode, thực thi an toàn kiểu và logic tuyến tính

Trình xác minh bytecode chủ yếu thực hiện các kiểm tra sau:

1. Kiểm tra tính hợp pháp của cấu trúc
2. Phát hiện ngữ nghĩa của logic quy trình
3. Kiểm tra lỗi khi kết nối

Thông qua những cơ chế này, Move có thể đảm bảo tính an toàn mã cao khi biên dịch.

2. Cơ chế hoạt động của Move

Chương trình Move chạy trong máy ảo, có các đặc điểm an toàn sau:

• Không thể truy cập trực tiếp bộ nhớ hệ thống
• Thực thi trên ngăn xếp, lưu trữ toàn cầu được chia thành hai phần: bộ nhớ và biến toàn cầu.
• Thực hiện lệnh bytecode bằng cách sử dụng bộ thông dịch ngăn xếp
• Giá trị tài nguyên chỉ có thể được di chuyển một cách hủy diệt
• Trạng thái được tạo thành từ ngăn xếp gọi, bộ nhớ, biến toàn cục và các phép toán.
• Quá trình gọi không có phụ thuộc vòng, tránh vấn đề tái nhập
• Tách biệt lưu trữ dữ liệu và ngăn gọi

Thiết kế này có sự cải thiện lớn về độ 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, có thể:

• Sử dụng ngôn ngữ hình thức để mô tả hành vi chương trình
• Xác minh tính chính xác của chương trình thông qua thuật toán suy diễn
• Áp dụng thuật toán xác thực suy diễn
• Sử dụng ngôn ngữ quy ước Move để mô tả quy tắc xác minh
• Tạo báo cáo xác minh, chỉ ra các vấn đề tiềm ẩn

Move Prover là một công cụ hỗ trợ kiểm tra tự động rất hữu ích, có thể giúp các nhà phát triển nâng cao độ an toàn của hợp đồng thông minh.

Tóm tắt

Ngôn ngữ Move đã thực hiện các xem xét toàn diện về tính bảo mật ở các khía cạnh như đặc điểm ngôn ngữ, thực thi máy ảo và công cụ bảo mật. Nó có thể tránh hiệu quả các lỗ hổng EVM phổ biến, chẳng hạn như tấn công tái nhập và tràn. Tuy nhiên, vẫn cần chú ý đến các vấn đề bảo mật liên quan đến xác thực và thiết kế logic.

Mặc dù Move có nhiều ưu điểm về tính bảo mật, nhưng vẫn khuyên các nhà phát triển nên sử dụng dịch vụ kiểm toán bảo mật của bên thứ ba và để đội ngũ bảo mật chuyên nghiệp viết và xác minh mã quy ước, nhằm đảm bảo thêm tính bảo mật cho hợp đồng thông minh.