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ó ra đời với sự cân nhắc đến nhiều vấn đề an ninh của blockchain và hợp đồng thông minh, và tham khảo một số 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 toàn, tính an toàn của Move thực sự như thế nào? Nó có thể tránh được các mối đe dọa an ninh phổ biến của máy ảo hợp đồng như EVM, WASM trên cấp độ ngôn ngữ hoặc các cơ chế liên quan không? Nó có tồn tại các vấn đề an ninh đặc thù của riêng nó 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ế vận hành và công cụ xác minh.
1. Tính năng an toàn của ngôn ngữ Move
Việc viết mã chính xác là rất khó, ngay cả sau nhiều lần kiểm tra cũng không thể đảm bảo rằng mã hoàn toàn không có lỗ hổng. Khi tương tác với mã không đáng tin cậy, việc viết mã có thể duy trì các thuộc tính an toàn quan trọng còn khó khăn hơn. Có nhiều kỹ thuật có thể thực thi an toàn thời gian chạy, như sandbox, phân tách quy trình, khóa đối tượng và các mô hình lập trình khác; cũng có thể chỉ định an toàn tĩnh tại thời điểm biên dịch, như ép kiểu tĩnh hoặc kiểm tra khẳng định.
Đôi khi cũng có thể sử dụng phân tích ngữ nghĩa và các công cụ phân tích tĩnh để đảm bảo mã tuân thủ các quy tắc an toàn, ngay cả khi tương tác với mã không đáng tin cậy cũng có thể giữ nguyên một số quy tắc logic có thể chứng minh.
Các giải pháp này có vẻ tốt, có thể tránh chi phí thời gian chạy và phát hiện sớm các vấn đề an ninh. Nhưng thật đáng tiếc, độ an toàn mà ngôn ngữ lập trình đạt được thông qua những phương pháp này là cực kỳ hạn chế, chủ yếu có hai lý do: trước tiên, chúng thường có những đặc điểm không thể sử dụng công cụ phân tích tĩnh, chẳng hạn như phân phối động, chia sẻ tính biến đổi và phản xạ, vi phạm quy tắc bất biến an toàn, cung cấp cho hacker một bề mặt tấn công rộng. Thứ hai, hầu hết các ngôn ngữ lập trình khó mở rộng bằng các công cụ tĩnh liên quan đến an ninh hoặc ngôn ngữ quy chuẩn mạnh mẽ. Mặc dù cả hai loại mở rộng này đều rất quan trọng và có thể được định nghĩa trước.
Khác với nhiều ngôn ngữ lập trình hiện có, ngôn ngữ Move được thiết kế từ đầu để hỗ trợ viết các chương trình 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 có những đặc điểm an toàn như vậy vì đã từ bỏ tất cả các logic phi tuyến tính dựa trên sự linh hoạt, không hỗ trợ phân phối động, cũng như không hỗ trợ gọi ngoại vi đệ 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ế. Ví dụ, Move đã bỏ qua các đặc điểm như lập lịch động và gọi đệ quy, những đặc điểm này trong các ngôn ngữ hợp đồng thông minh khác đã dẫn đến các lỗ hổng tái nhập tốn kém.
Để hiểu rõ hơn về các đặc điểm của ngôn ngữ Move, chúng ta hãy xem một chương trình mẫu:
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 {
total_supply: u64
}
mô-đun spec {
bất biến forall addr: address where exists<coin>(addr):
toàn cầu<info>(QUẢN TRỊ).tổng_cung >= toàn cầu<coin>(addr).giá_trị;
}
công khai vui lòng khởi tạo(tài khoản: &người ký) {
assert!(signer::address_of(account) == ADMIN, 0);
chuyển_đến(tài_khoản, Thông_tin { tổng_cung: 0 })
}
public fun mint(account: &signer, amount: u64): Coin acquires Info {
assert!(signer::address_of(account) == ADMIN, 0);
let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
supply.total_supply = supply.total_supply + amount;
Coin { value: amount }
}
public fun value(coin: &Coin): u64 {
coin.value
}
public fun value_mut(coin: &mut Coin): &mut u64 {
&mut coin.value
}
}
a) Module(: 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 định nghĩa kiểu và gọi các quy trình được khai báo trong các mô-đun khác. Tên đầy đủ của mô-đun bắt đầu bằng địa chỉ tài khoản 16 byte nơi mã mô-đun được lưu trữ. Địa chỉ tài khoản đóng vai trò như một không gian tên, được sử dụng để phân biệt các mô-đun có cùng tên.
b) Cấu trúc )Structs(: Mô-đun này định nghĩa hai cấu trúc Coin và Info. Coin đại diện cho các token được phân phối cho người dùng, Info ghi lại tổng số lượng token. Cả hai cấu trúc đều được định nghĩa là loại tài nguyên, có thể được lưu trữ trong kho lưu trữ khóa/giá trị toàn cầu vĩnh viễn.
c) quá trình ) function (: mã định nghĩa một quá trình khởi tạo, một quá trình an toàn và một quá trình không an toàn. Trước khi tạo Coin, quá trình initialize phải được gọi để khởi tạo giá trị total_supply của Info singleton thành không. signer là một loại đặc biệt, đại diện cho người dùng được xác thực bởi logic bên ngoài Move. Assertion đảm bảo rằng chỉ tài khoản quản trị viên được chỉ định mới có thể gọi quá trình này. Quá trình mint cho phép quản trị viên tạo ra token mới, cũng có kiểm soát truy cập. Quá trình value_mut chấp nhận tham chiếu biến của Coin, trả về tham chiếu biến đến trường value.
Cấu trúc hợp đồng tương tự như các ngôn ngữ hợp đồng thông minh khác, nhưng loại tài nguyên và lưu trữ toàn cầu là cơ chế quan trọng để lưu trữ và bảo mật tài nguyên trong ngôn ngữ Move.
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ác mô-đun sở hữu nó đọc và ghi theo cách lập trình, nhưng được lưu trữ trong sổ cái công cộng, các người dùng của mô-đun khác có thể xem. Mỗi khóa trong lưu trữ toàn cầu bao gồm tên loại được xác định đầy đủ và địa chỉ tài khoản lưu trữ giá trị của loại đó. Mặc dù lưu trữ toàn cầu được chia sẻ giữa tất cả các mô-đun, nhưng mỗi mô-đun có quyền truy cập đọc và ghi độc quyền đối với các khóa mà nó đã khai báo.
Các mô-đun khai báo loại tài nguyên có thể:
• Đưa giá trị vào bộ nhớ toàn cục thông qua lệnh move_to
• Xóa giá trị từ bộ nhớ toàn cầu bằng lệnh move_from
• Lấy tham chiếu đến giá trị trong bộ nhớ toàn cầu thông qua lệnh borrow_global_mut
Các mô-đun có thể áp đặt các ràng buộc đối với bộ nhớ toàn cầu mà chúng kiểm soát. Ví dụ, đảm bảo rằng chỉ có địa chỉ tài khoản ADMIN có thể giữ cấu trúc loại Info, điều này được thực hiện thông qua việc định nghĩa quá trình khởi tạo, quá trình này sử dụng move_to trên loại Info và áp đặt điều kiện tiên quyết cho việc gọi move_to trên địa chỉ ADMIN.
Dưới đây là hai cơ chế đặc tính kiểm tra tĩnh đảm bảo mã của mô-đun này an toàn: quy tắc bất biến và bộ xác thực bytecode.
a) Kiểm tra bất biến ) Kiểm tra quy ước (: Dòng 10 của mô-đun chỉ ra kiểm tra tĩnh của bất biến - tổng của các trường giá trị của tất cả các đối tượng Coin trong hệ thống phải bằng trường total_value được lưu trữ trong đối tượng Info tại địa chỉ ADMIN. Bất biến là một thuật ngữ trong xác minh hình thức, biểu thị sự bảo tồn trạng thái. Thuộc tính bảo tồn này áp dụng cho tất cả các khách hàng có thể của mô-đun.
b) Trình xác thực bytecode: Loại an toàn và tuyến tính là phạm vi xác thực chính của trình xác thực bytecode. Mặc dù các mô-đun khác không thể truy cập các đơn vị lưu trữ toàn cầu do 0x1::TestCoin::Coin kiểm soát, nhưng chúng có thể sử dụng loại này trong các khai báo quy trình và cấu trúc của riêng mình.
Move có trình xác thực bytecode ), thực thi hệ thống kiểu ở cấp độ bytecode (, cho phép chủ sở hữu mô-đun ngăn chặn các kết quả không mong muốn. Chỉ các mô-đun khai báo kiểu cấu trúc Coin mới có thể:
• Tạo giá trị loại Coin
• Giải nén giá trị loại Coin vào các trường thành phần của nó
• Nhận tham chiếu đến trường Coin thông qua borrow có thể thay đổi hoặc không thay đổi theo phong cách rust
Trình xác thực cũng buộc cấu trúc mặc định là tuyến tính, nhằm đảm bảo ngăn chặn sao chép và phá hủy một cách tuyến tính bên ngoài mô-đun nơi khai báo cấu trúc. Đồng thời, trình xác thực cũng sẽ thực hiện kiểm tra bắt buộc đối với một số vấn đề bộ nhớ phổ biến.
Quá trình kiểm tra chủ yếu có ba loại:
Kiểm tra tính hợp pháp của cấu trúc: đảm bảo tính toàn vẹn của bytecode, phát hiện lỗi tham chiếu bất hợp pháp, thực thể tài nguyên trùng lặp và chữ ký loại bất hợp pháp, v.v.
Kiểm tra ngữ nghĩa của logic quá trình: bao gồm lỗi kiểu tham số, chỉ số vòng lặp, chỉ số rỗng và định nghĩa biến lặp lại.
Lỗi khi kết nối, gọi quy trình nội bộ không hợp pháp, hoặc quy trình không khớp với tuyên bố và định nghĩa kết nối.
Các trình xác thực trước tiên tạo ra CFG) đồ thị luồng điều khiển (, sau đó kiểm tra phạm vi truy cập của người gọi trong ngăn xếp, đảm bảo rằng người gọi hợp đồng không thể truy cập không gian ngăn xếp của người gọi. Đồng thời, để kiểm tra kiểu, mỗi ngăn xếp Value đều duy trì một ngăn xếp Type tương ứng.
Tiếp theo là kiểm tra tài nguyên và kiểm tra tham chiếu. Tài nguyên chủ yếu kiểm tra các ràng buộc như không thể chi tiêu gấp đôi, không thể tiêu hủy, phải có quyền sở hữu, v.v. Kiểm tra tham chiếu kết hợp phân tích động và tĩnh, sử dụng cơ chế kiểm tra mượn tương tự như hệ thống kiểu rust.
Cuối cùng là kiểm tra liên kết, cần kiểm tra lại xem đối tượng liên kết và tuyên bố có khớp nhau hay không, cũng như kiểm soát quyền truy cập trong quá trình.
![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-419437619d55298077789e6eca578b48.webp(
) 2. Cơ chế hoạt động của Move
Đầu tiên, 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 đáng tin cậy, không bị phá hủy hoặc lạm dụng.
Thứ hai, chương trình Move được 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 ). Bộ nhớ là bộ lưu trữ bậc một, các đơn vị của nó không thể lưu trữ con trỏ trỏ đến các đơn vị bộ nhớ. Biến toàn cầu được sử dụng để lưu trữ con trỏ trỏ đến các đơn vị bộ nhớ, nhưng cách chỉ mục khác nhau. Khi truy cập biến toàn cầu, mã cung cấp địa chỉ và kiểu được gán cho địa chỉ đó. Sự phân chia này đơn giản hóa các thao tác, làm cho ngữ nghĩa của ngôn ngữ Move dễ dàng hình thức hóa hơn.
Các lệnh bytecode Move được thực thi trong trình 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 ít về môi trường phần cứng, phù hợp với các tình huống blockchain. So với trình thông dịch kiểu thanh ghi, trình 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 Move, giá trị được định nghĩa là tài nguyên chỉ có thể bị di chuyển một cách phá hủy ( khiến vị trí lưu trữ trước đó của giá trị đó trở nên không hợp lệ ), nhưng một số giá trị ( như số nguyên ) có thể được sao chép.
Khi chương trình Move chạy trên ngăn xếp, trạng thái của nó là bốn tử ⟨C, M, G, S⟩, được cấu thành từ 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 ( để phân tích các lệnh chứa thân hàm.
Ngăn xếp gọi chứa tất cả thông tin ngữ cảnh và số chỉ thị của quá trình thực thi. Khi thực hiện chỉ thị Call, tạo một đối tượng ngăn xếp gọi mới, lưu trữ tham số gọi vào bộ nhớ và biến toàn cục, sau đó trình thông dịch thực thi các chỉ thị của hợp đồng mới. Khi gặp chỉ thị nhánh, xảy ra nhảy tĩnh trong quá trình này. Các quy trình trong mô-đun phụ thuộc vào vòng không, cùng với việc mô-đun không có chỉ định động, đã tăng cường tính bất biến của việc gọi hàm trong suốt quá trình thực thi: khung gọi của quy trình phải liền kề, tránh khả năng gọi lại. Gọi return kết thúc cuộc gọi, giá trị trả về được đặt ở đỉnh ngăn xếp.
Nghiên cứu mã MoveVM cho thấy, 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 so với EVM. Trong EVM, việc triển khai Token ERC20 cần viết logic trong một hợp đồng và ghi lại trạng thái của từng người dùng, trong khi trong MoveVM, trạng thái người dùng ( được lưu trữ độc lập dưới nguồn tài nguyên tại địa chỉ tài khoản ), việc gọi chương trình phải tuân thủ quyền hạn và các quy tắc bắt buộc về nguồn tài nguyên. Mặc dù điều này hy sinh một phần tính linh hoạt, nhưng về an toàn và hiệu suất thực thi ( giúp cải thiện đáng kể khả năng thực thi đồng thời ).
( 3. Di chuyển Prover
Cuối cùng, chúng ta hãy tìm hiểu về công cụ hỗ trợ kiểm toán tự động Move prover mà Move cung cấp.
Move Prover là 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ó đáp ứng được 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, giảm thiểu rủi ro giao dịch. Nói một cách đơn giản, xác minh hình thức là việc sử dụng phương pháp toán học để chứng minh rằng hệ thống không có lỗi.
Hiện nay, các thuật toán xác minh phần mềm tự động chính chủ yếu dựa trên bộ giải lý thuyết sự thỏa mãn )SMT solver(. Bộ giải SMT thực tế là một bộ giải công thức. Các thuật toán xác minh phần mềm trên sẽ phân tách mục tiêu xác minh thành các công thức, giao cho bộ giải SMT giải quyết, dựa trên kết quả để phân tích thêm, cuối cùng báo cáo mục tiêu xác minh có tồn tại hay không hoặc phát hiện phản ví dụ.
Thuật toán xác minh cơ bản là xác minh suy diễn )deductive verification###, cùng với các thuật toán xác minh khác như kiểm tra mô hình giới hạn, phương pháp quy nạp k, trừu tượng hóa mệnh đề và trừu tượng hóa đường đi.
Move Prover sử dụng thuật toán xác minh 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 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, đảm bảo rằng nó khớp với hành vi dự kiến. Đ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 kiểm tra thủ công.
Kiến trúc tổng thể của Move Prover như sau:
Trước tiên, Move Prover nhận tệp nguồn Move chứa đặc tả đầu vào chương trình (specification). Move Parser trích xuất đặc tả từ mã nguồn. Trình biên dịch Move biên dịch tệp nguồn thành mã byte, cùng với hệ thống đặc tả chuyển đổi thành mô hình đối tượng xác nhận (Prover Object Model).
Mô hình này được dịch sang ngôn ngữ trung gian Boogie. Mã Boogie được đưa vào hệ thống xác minh Boogie để "tạo điều kiện xác minh". Điều kiện xác minh được đưa vào bộ giải Z3 (, bộ giải SMT do Microsoft phát triển ).
Sau khi VC được truyền vào Z3, trình xác minh kiểm tra mã chương trình SMT ( có thỏa mãn tiêu chuẩn specification ) hay không. Nếu có, điều đó có nghĩa là tiêu chuẩn được thỏa mãn. Nếu không, tạo ra một mô hình thỏa mãn điều kiện, chuyển đổi lại về định dạng Boogie để phát hành báo cáo chẩn đoán. Báo cáo chẩn đoán được khôi phục thành lỗi cấp mã nguồn tương tự như lỗi của trình biên dịch chuẩn.
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
SchrodingerAirdrop
· 08-09 21:11
move vẫn chưa đủ an toàn, hãy tin tôi
Xem bản gốcTrả lời0
DataBartender
· 08-07 02:38
Lại đang nói về move một cách phấn khích quá mức rồi.
Xem bản gốcTrả lời0
AirdropHarvester
· 08-07 02:29
Move? Nghe có vẻ phiền phức, học cũng khó như Rust.
Xem bản gốcTrả lời0
MoneyBurner
· 08-07 02:28
Lại muốn lừa tôi nhập một vị thế để xem chuỗi công cộng mới à? Lần trước đã lỗ nặng rồi.
Xem bản gốcTrả lời0
StableNomad
· 08-07 02:28
hmm một "ngôn ngữ" "an toàn" khác... khiến tôi nhớ đến solana vào năm 2021 thật ra
Phân tích độ sâu về an ninh của ngôn ngữ Move: Đặc điểm ngôn ngữ, Cơ chế hoạt động và Kiểm toán tự động
Lời mở đầu
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ó ra đời với sự cân nhắc đến nhiều vấn đề an ninh của blockchain và hợp đồng thông minh, và tham khảo một số 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 toàn, tính an toàn của Move thực sự như thế nào? Nó có thể tránh được các mối đe dọa an ninh phổ biến của máy ảo hợp đồng như EVM, WASM trên cấp độ ngôn ngữ hoặc các cơ chế liên quan không? Nó có tồn tại các vấn đề an ninh đặc thù của riêng nó 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ế vận hành và công cụ xác minh.
1. Tính năng an toàn của ngôn ngữ Move
Việc viết mã chính xác là rất khó, ngay cả sau nhiều lần kiểm tra cũng không thể đảm bảo rằng mã hoàn toàn không có lỗ hổng. Khi tương tác với mã không đáng tin cậy, việc viết mã có thể duy trì các thuộc tính an toàn quan trọng còn khó khăn hơn. Có nhiều kỹ thuật có thể thực thi an toàn thời gian chạy, như sandbox, phân tách quy trình, khóa đối tượng và các mô hình lập trình khác; cũng có thể chỉ định an toàn tĩnh tại thời điểm biên dịch, như ép kiểu tĩnh hoặc kiểm tra khẳng định.
Đôi khi cũng có thể sử dụng phân tích ngữ nghĩa và các công cụ phân tích tĩnh để đảm bảo mã tuân thủ các quy tắc an toàn, ngay cả khi tương tác với mã không đáng tin cậy cũng có thể giữ nguyên một số quy tắc logic có thể chứng minh.
Các giải pháp này có vẻ tốt, có thể tránh chi phí thời gian chạy và phát hiện sớm các vấn đề an ninh. Nhưng thật đáng tiếc, độ an toàn mà ngôn ngữ lập trình đạt được thông qua những phương pháp này là cực kỳ hạn chế, chủ yếu có hai lý do: trước tiên, chúng thường có những đặc điểm không thể sử dụng công cụ phân tích tĩnh, chẳng hạn như phân phối động, chia sẻ tính biến đổi và phản xạ, vi phạm quy tắc bất biến an toàn, cung cấp cho hacker một bề mặt tấn công rộng. Thứ hai, hầu hết các ngôn ngữ lập trình khó mở rộng bằng các công cụ tĩnh liên quan đến an ninh hoặc ngôn ngữ quy chuẩn mạnh mẽ. Mặc dù cả hai loại mở rộng này đều rất quan trọng và có thể được định nghĩa trước.
Khác với nhiều ngôn ngữ lập trình hiện có, ngôn ngữ Move được thiết kế từ đầu để hỗ trợ viết các chương trình 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 có những đặc điểm an toàn như vậy vì đã từ bỏ tất cả các logic phi tuyến tính dựa trên sự linh hoạt, không hỗ trợ phân phối động, cũng như không hỗ trợ gọi ngoại vi đệ 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ế. Ví dụ, Move đã bỏ qua các đặc điểm như lập lịch động và gọi đệ quy, những đặc điểm này trong các ngôn ngữ hợp đồng thông minh khác đã dẫn đến các lỗ hổng tái nhập tốn kém.
Để hiểu rõ hơn về các đặc điểm của ngôn ngữ Move, chúng ta hãy xem một chương trình mẫu:
di chuyển module 0x1::TestCoin { sử dụng 0x1::signer;
}
a) Module(: 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 định nghĩa kiểu và gọi các quy trình được khai báo trong các mô-đun khác. Tên đầy đủ của mô-đun bắt đầu bằng địa chỉ tài khoản 16 byte nơi mã mô-đun được lưu trữ. Địa chỉ tài khoản đóng vai trò như một không gian tên, được sử dụng để phân biệt các mô-đun có cùng tên.
b) Cấu trúc )Structs(: Mô-đun này định nghĩa hai cấu trúc Coin và Info. Coin đại diện cho các token được phân phối cho người dùng, Info ghi lại tổng số lượng token. Cả hai cấu trúc đều được định nghĩa là loại tài nguyên, có thể được lưu trữ trong kho lưu trữ khóa/giá trị toàn cầu vĩnh viễn.
c) quá trình ) function (: mã định nghĩa một quá trình khởi tạo, một quá trình an toàn và một quá trình không an toàn. Trước khi tạo Coin, quá trình initialize phải được gọi để khởi tạo giá trị total_supply của Info singleton thành không. signer là một loại đặc biệt, đại diện cho người dùng được xác thực bởi logic bên ngoài Move. Assertion đảm bảo rằng chỉ tài khoản quản trị viên được chỉ định mới có thể gọi quá trình này. Quá trình mint cho phép quản trị viên tạo ra token mới, cũng có kiểm soát truy cập. Quá trình value_mut chấp nhận tham chiếu biến của Coin, trả về tham chiếu biến đến trường value.
Cấu trúc hợp đồng tương tự như các ngôn ngữ hợp đồng thông minh khác, nhưng loại tài nguyên và lưu trữ toàn cầu là cơ chế quan trọng để lưu trữ và bảo mật tài nguyên trong ngôn ngữ Move.
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ác mô-đun sở hữu nó đọc và ghi theo cách lập trình, nhưng được lưu trữ trong sổ cái công cộng, các người dùng của mô-đun khác có thể xem. Mỗi khóa trong lưu trữ toàn cầu bao gồm tên loại được xác định đầy đủ và địa chỉ tài khoản lưu trữ giá trị của loại đó. Mặc dù lưu trữ toàn cầu được chia sẻ giữa tất cả các mô-đun, nhưng mỗi mô-đun có quyền truy cập đọc và ghi độc quyền đối với các khóa mà nó đã khai báo.
Các mô-đun khai báo loại tài nguyên có thể: • Đưa giá trị vào bộ nhớ toàn cục thông qua lệnh move_to • Xóa giá trị từ bộ nhớ toàn cầu bằng lệnh move_from • Lấy tham chiếu đến giá trị trong bộ nhớ toàn cầu thông qua lệnh borrow_global_mut
Các mô-đun có thể áp đặt các ràng buộc đối với bộ nhớ toàn cầu mà chúng kiểm soát. Ví dụ, đảm bảo rằng chỉ có địa chỉ tài khoản ADMIN có thể giữ cấu trúc loại Info, điều này được thực hiện thông qua việc định nghĩa quá trình khởi tạo, quá trình này sử dụng move_to trên loại Info và áp đặt điều kiện tiên quyết cho việc gọi move_to trên địa chỉ ADMIN.
Dưới đây là hai cơ chế đặc tính kiểm tra tĩnh đảm bảo mã của mô-đun này an toàn: quy tắc bất biến và bộ xác thực bytecode.
a) Kiểm tra bất biến ) Kiểm tra quy ước (: Dòng 10 của mô-đun chỉ ra kiểm tra tĩnh của bất biến - tổng của các trường giá trị của tất cả các đối tượng Coin trong hệ thống phải bằng trường total_value được lưu trữ trong đối tượng Info tại địa chỉ ADMIN. Bất biến là một thuật ngữ trong xác minh hình thức, biểu thị sự bảo tồn trạng thái. Thuộc tính bảo tồn này áp dụng cho tất cả các khách hàng có thể của mô-đun.
b) Trình xác thực bytecode: Loại an toàn và tuyến tính là phạm vi xác thực chính của trình xác thực bytecode. Mặc dù các mô-đun khác không thể truy cập các đơn vị lưu trữ toàn cầu do 0x1::TestCoin::Coin kiểm soát, nhưng chúng có thể sử dụng loại này trong các khai báo quy trình và cấu trúc của riêng mình.
Move có trình xác thực bytecode ), thực thi hệ thống kiểu ở cấp độ bytecode (, cho phép chủ sở hữu mô-đun ngăn chặn các kết quả không mong muốn. Chỉ các mô-đun khai báo kiểu cấu trúc Coin mới có thể: • Tạo giá trị loại Coin • Giải nén giá trị loại Coin vào các trường thành phần của nó • Nhận tham chiếu đến trường Coin thông qua borrow có thể thay đổi hoặc không thay đổi theo phong cách rust
Trình xác thực cũng buộc cấu trúc mặc định là tuyến tính, nhằm đảm bảo ngăn chặn sao chép và phá hủy một cách tuyến tính bên ngoài mô-đun nơi khai báo cấu trúc. Đồng thời, trình xác thực cũng sẽ thực hiện kiểm tra bắt buộc đối với một số vấn đề bộ nhớ phổ biến.
Quá trình kiểm tra chủ yếu có ba loại:
Các trình xác thực trước tiên tạo ra CFG) đồ thị luồng điều khiển (, sau đó kiểm tra phạm vi truy cập của người gọi trong ngăn xếp, đảm bảo rằng người gọi hợp đồng không thể truy cập không gian ngăn xếp của người gọi. Đồng thời, để kiểm tra kiểu, mỗi ngăn xếp Value đều duy trì một ngăn xếp Type tương ứng.
Tiếp theo là kiểm tra tài nguyên và kiểm tra tham chiếu. Tài nguyên chủ yếu kiểm tra các ràng buộc như không thể chi tiêu gấp đôi, không thể tiêu hủy, phải có quyền sở hữu, v.v. Kiểm tra tham chiếu kết hợp phân tích động và tĩnh, sử dụng cơ chế kiểm tra mượn tương tự như hệ thống kiểu rust.
Cuối cùng là kiểm tra liên kết, cần kiểm tra lại xem đối tượng liên kết và tuyên bố có khớp nhau hay không, cũng như kiểm soát quyền truy cập trong quá trình.
![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-419437619d55298077789e6eca578b48.webp(
) 2. Cơ chế hoạt động của Move
Đầu tiên, 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 đáng tin cậy, không bị phá hủy hoặc lạm dụng.
Thứ hai, chương trình Move được 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 ). Bộ nhớ là bộ lưu trữ bậc một, các đơn vị của nó không thể lưu trữ con trỏ trỏ đến các đơn vị bộ nhớ. Biến toàn cầu được sử dụng để lưu trữ con trỏ trỏ đến các đơn vị bộ nhớ, nhưng cách chỉ mục khác nhau. Khi truy cập biến toàn cầu, mã cung cấp địa chỉ và kiểu được gán cho địa chỉ đó. Sự phân chia này đơn giản hóa các thao tác, làm cho ngữ nghĩa của ngôn ngữ Move dễ dàng hình thức hóa hơn.
Các lệnh bytecode Move được thực thi trong trình 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 ít về môi trường phần cứng, phù hợp với các tình huống blockchain. So với trình thông dịch kiểu thanh ghi, trình 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 Move, giá trị được định nghĩa là tài nguyên chỉ có thể bị di chuyển một cách phá hủy ( khiến vị trí lưu trữ trước đó của giá trị đó trở nên không hợp lệ ), nhưng một số giá trị ( như số nguyên ) có thể được sao chép.
Khi chương trình Move chạy trên ngăn xếp, trạng thái của nó là bốn tử ⟨C, M, G, S⟩, được cấu thành từ 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 ( để phân tích các lệnh chứa thân hàm.
Ngăn xếp gọi chứa tất cả thông tin ngữ cảnh và số chỉ thị của quá trình thực thi. Khi thực hiện chỉ thị Call, tạo một đối tượng ngăn xếp gọi mới, lưu trữ tham số gọi vào bộ nhớ và biến toàn cục, sau đó trình thông dịch thực thi các chỉ thị của hợp đồng mới. Khi gặp chỉ thị nhánh, xảy ra nhảy tĩnh trong quá trình này. Các quy trình trong mô-đun phụ thuộc vào vòng không, cùng với việc mô-đun không có chỉ định động, đã tăng cường tính bất biến của việc gọi hàm trong suốt quá trình thực thi: khung gọi của quy trình phải liền kề, tránh khả năng gọi lại. Gọi return kết thúc cuộc gọi, giá trị trả về được đặt ở đỉnh ngăn xếp.
Nghiên cứu mã MoveVM cho thấy, 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 so với EVM. Trong EVM, việc triển khai Token ERC20 cần viết logic trong một hợp đồng và ghi lại trạng thái của từng người dùng, trong khi trong MoveVM, trạng thái người dùng ( được lưu trữ độc lập dưới nguồn tài nguyên tại địa chỉ tài khoản ), việc gọi chương trình phải tuân thủ quyền hạn và các quy tắc bắt buộc về nguồn tài nguyên. Mặc dù điều này hy sinh một phần tính linh hoạt, nhưng về an toàn và hiệu suất thực thi ( giúp cải thiện đáng kể khả năng thực thi đồng thời ).
( 3. Di chuyển Prover
Cuối cùng, chúng ta hãy tìm hiểu về công cụ hỗ trợ kiểm toán tự động Move prover mà Move cung cấp.
Move Prover là 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ó đáp ứng được 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, giảm thiểu rủi ro giao dịch. Nói một cách đơn giản, xác minh hình thức là việc sử dụng phương pháp toán học để chứng minh rằng hệ thống không có lỗi.
Hiện nay, các thuật toán xác minh phần mềm tự động chính chủ yếu dựa trên bộ giải lý thuyết sự thỏa mãn )SMT solver(. Bộ giải SMT thực tế là một bộ giải công thức. Các thuật toán xác minh phần mềm trên sẽ phân tách mục tiêu xác minh thành các công thức, giao cho bộ giải SMT giải quyết, dựa trên kết quả để phân tích thêm, cuối cùng báo cáo mục tiêu xác minh có tồn tại hay không hoặc phát hiện phản ví dụ.
Thuật toán xác minh cơ bản là xác minh suy diễn )deductive verification###, cùng với các thuật toán xác minh khác như kiểm tra mô hình giới hạn, phương pháp quy nạp k, trừu tượng hóa mệnh đề và trừu tượng hóa đường đi.
Move Prover sử dụng thuật toán xác minh 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 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, đảm bảo rằng nó khớp với hành vi dự kiến. Đ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 kiểm tra thủ công.
Kiến trúc tổng thể của Move Prover như sau:
Trước tiên, Move Prover nhận tệp nguồn Move chứa đặc tả đầu vào chương trình (specification). Move Parser trích xuất đặc tả từ mã nguồn. Trình biên dịch Move biên dịch tệp nguồn thành mã byte, cùng với hệ thống đặc tả chuyển đổi thành mô hình đối tượng xác nhận (Prover Object Model).
Mô hình này được dịch sang ngôn ngữ trung gian Boogie. Mã Boogie được đưa vào hệ thống xác minh Boogie để "tạo điều kiện xác minh". Điều kiện xác minh được đưa vào bộ giải Z3 (, bộ giải SMT do Microsoft phát triển ).
Sau khi VC được truyền vào Z3, trình xác minh kiểm tra mã chương trình SMT ( có thỏa mãn tiêu chuẩn specification ) hay không. Nếu có, điều đó có nghĩa là tiêu chuẩn được thỏa mãn. Nếu không, tạo ra một mô hình thỏa mãn điều kiện, chuyển đổi lại về định dạng Boogie để phát hành báo cáo chẩn đoán. Báo cáo chẩn đoán được khôi phục thành lỗi cấp mã nguồn tương tự như lỗi của trình biên dịch chuẩn.
![Move安