Phân tích an ninh ngôn ngữ Move: Người cải cách hợp đồng thông minh

Ngôn ngữ Move là một ngôn ngữ hợp đồng thông minh có thể biên dịch và chạy trong môi trường blockchain triển khai MoveVM. 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, tính an toàn của nó như thế nào? Có thể tránh được các mối đe dọa an toàn phổ biến của các máy ảo hợp đồng như EVM, WASM 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ế 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

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ợ 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 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 bộ đệ 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 các mô hình lập trình thay thế.

Dưới đây là một ví dụ về việc triển khai tài sản token bằng ngôn ngữ Move:

di chuyển module 0x1::TestCoin { sử dụng 0x1::signer;

const ADMIN: address = @0x1;

struct Coin có key, store { 
    giá trị: u64
}

struct Info có khóa {
    tổng_cung: u64  
}

mô-đun spec {
    bất biến forall addr: địa chỉ nơi tồn tại<coin>(addr):
        global\u003cinfo\u003e(ADMIN).total_supply \u003e= global\u003ccoin\u003e(addr).value;
}

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 1);
    chuyển_đến(tài_khoản, Thông_tin { tổng_cung: 0 })
}

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let coin = Coin { value: amount };
    let info = borrow_global_mut\u003cinfo\u003e(ADMIN);
    info.total_supply = info.total_supply + amount;
    đồng tiền
}

public fun value(coin: &Coin): u64 {
    coin.value  
}

}

Ví dụ này trình bày một số tính năng bảo mật chính của ngôn ngữ Move:

1. Tính mô-đun: Mỗi mô-đun Move bao gồm các định nghĩa kiểu cấu trúc và quy trình, có thể nhập định nghĩa kiểu từ các mô-đun khác và gọi các quy trình từ các mô-đun khác.

2. Loại tài nguyên: Được định nghĩa là loại tài nguyên thông qua cấu trúc được đánh dấu bằng has key hoặc store, có thể được lưu trữ trong kho dữ liệu khóa-giá trị toàn cầu bền vững.

3. 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, chỉ có thể được đọc và viết bằng cách lập trình bởi các mô-đun sở hữu, nhưng lưu trữ trong sổ cái công cộng có thể được các mô-đun khác xem.

4. Kiểm soát truy cập: Có thể thực hiện kiểm soát truy cập đối với các thao tác quan trọng thông qua các cách như khẳng định.

5. Quy tắc bất biến: có thể định nghĩa bất biến kiểm tra tĩnh, được sử dụng để xác minh hình thức.

6. Xác minh bytecode: bao gồm loại an toàn và xác minh tuyến tính, ngăn chặn các thao tác trái phép trên loại tài nguyên.

Những đặc điểm này cùng đảm bảo tính an toàn của ngôn ngữ Move 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, 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 đáng tin cậy.

Chương trình Move thực thi 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 ). Bộ nhớ không thể lưu trữ con trỏ đến ô nhớ, biến toàn cầu được sử dụng để lưu trữ con trỏ đến ô nhớ.

Bytecode của Move được thực thi trong trình thông dịch ngăn xếp, thuận tiện cho việc triển khai và kiểm soát, phù hợp với các tình huống blockchain. Giá trị của loại tài nguyên chỉ có thể được di chuyển một cách hủy hoại.

Trạng thái chạy của chương trình Move là một tứ tuple ⟨C, M, G, S⟩, bao gồm ngăn gọi, bộ nhớ, biến toàn cục và toán hạng. Trong quá trình thực thi, việc gọi hàm tạo ra một đối tượng ngăn gọi mới, các chỉ thị nhánh thực hiện nhảy tĩnh, tránh việc phân phối động.

MoveVM tách biệt lưu trữ dữ liệu và ngăn xếp gọi, khác với thiết kế của EVM. Thiết kế này tuy hy sinh tính linh hoạt nhưng nâng cao độ an toàn và hiệu suất thực thi.

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, 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 mong đợi hay không.

Kiến trúc Move Prover như sau:

1. Nhận tệp nguồn Move đầu vào, bao gồm quy định chương trình.
2. Trình phân tích cú pháp trích xuất quy tắc, trình biên dịch biên dịch mã nguồn thành mã byte.
3. Chuyển đổi thành mô hình đối tượng xác thực.
4. Dịch sang ngôn ngữ trung gian Boogie.
5. Hệ thống xác thực Boogie tạo ra các điều kiện xác thực.
6. Bộ giải Z3 kiểm tra xem công thức SMT có không thể thỏa mãn hay không.
7. Tạo báo cáo chẩn đoán và phục hồi về lỗi mức mã nguồn.

Move sử dụng Ngôn ngữ Đặc tả Move để mô tả quy tắc, là một tập con của ngôn ngữ Move.

Move Prover là 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, giảm thiểu rủi ro giao dịch.

Tóm tắt

Ngôn ngữ Move có thiết kế an ninh rất xuất sắc, đã xem xét toàn diện từ đặc điểm ngôn ngữ, thực thi máy ảo và công cụ bảo mật. Nó hy sinh một phần tính linh hoạt, củng cố 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à xác minh hình thức. 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ả trong việc tránh các lỗ hổng phổ biến của EVM như tái nhập, tràn số và tiêm mã, nhưng các vấn đề như xác thực, logic và tràn số lớn vẫn cần sự chú ý của các nhà phát triển. Mặc dù Move đã xem xét kỹ lưỡng về mặt an toàn, nhưng vẫn khuyến nghị sử dụng dịch vụ kiểm toán của công ty an toàn bên thứ ba, và giao việc chuẩn hóa mã viết và xác minh cho các đội ngũ an toàn chuyên nghiệp.