Phân tích độ an toàn của ngôn ngữ Move

Ngôn ngữ Move như một ngôn ngữ hợp đồng thông minh thế hệ mới, ngay từ khi thiết kế đã xem xét nhiều vấn đề an toàn. Bài viết này sẽ phân tích 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ế hoạt động 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 có các tính năng bảo mật sau:

• Bỏ qua việc phân phối động, gọi bên ngoài đệ quy và các logic phi tuyến khác, tránh được các lỗ hổng như tái nhập.
• 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ô hình lập trình an toàn
• 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 có thể được định nghĩa là loại tài nguyên, lưu trữ trong kho khóa giá trị toàn cầu
• Lưu trữ toàn cầu cho phép dữ liệu được lưu trữ vĩnh viễn, chỉ có thể được truy cập bởi các mô-đun sở hữu.
• Sử dụng quy tắc bất biến và trình xác thực bytecode để kiểm tra tĩnh

Trình xác thực bytecode chủ yếu thực hiện:

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

Thông qua các cơ chế này, ngôn ngữ Move có thể đảm bảo tính an toàn của mã trong quá trình biên dịch.

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

Chương trình Move chạy trên máy ảo, các đặc điểm chính bao gồm:

• Không thể truy cập bộ nhớ hệ thống, có thể chạy an toàn trong môi trường không tin cậy.
• Thực hiện trên ngăn xếp, bộ nhớ toàn cầu được chia thành bộ nhớ ( ngăn xếp ) và biến toàn cầu ( ngăn xếp )
• Sử dụng bộ thông dịch theo ngăn xếp để thực thi các lệnh bytecode
• Giá trị tài nguyên chỉ có thể bị di chuyển một cách phá hủy, không thể sao chép
• Trạng thái chương trình được cấu thành từ ngăn xếp gọi, bộ nhớ, biến toàn cục và mảng thao tác.
• Ngăn xếp gọi chứa ngữ cảnh thực thi, hỗ trợ nhảy tĩnh
• Tách biệt lưu trữ dữ liệu và ngăn gọi, nâng cao tính bảo mật 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, có thể thực hiện kiểm toán tự động:

• Sử dụng thuật toán xác minh suy diễn để xác minh tính chính xác của chương trình
• Nhận tệp nguồn Move và quy định làm đầu vào
• Chuyển đổi mã thành ngôn ngữ trung gian Boogie
• Sử dụng bộ giải SMT Z3 để xác minh liệu quy định có đúng hay không
• Hỗ trợ quy định mô tả Ngôn ngữ Đặc tả Move
• Có thể tự viết tài liệu quy chuẩn mà không ảnh hưởng đến mã nguồn kinh doanh

Move Prover 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.

Tóm tắt

Ngôn ngữ Move xem xét toàn diện về mặt an ninh, bao gồm các đặc điểm của ngôn ngữ, việc thực thi máy ảo và các công cụ an ninh. Nó có thể hiệu quả trong việc tránh các lỗ hổng phổ biến như tấn công lặp lại, tràn bộ nhớ, nhưng vẫn cần chú ý đến các vấn đề như xác thực, logic. Đề xuất sử dụng dịch vụ kiểm toán của công ty an ninh bên thứ ba và để các chuyên gia viết mã xác thực quy chuẩn.