/ Xác minh chính thức nâng cao ngăn xếp phần mềm hoàn chỉnh Web3/
CertiK gần đây đã phát hành báo cáo xác minh chính thức nâng cao về mô-đun Cosmos SDK Bank, theo hiểu biết của chúng tôi, đây là nỗ lực thành công đầu tiên trong việc xác minh chính thức Cosmos SDK. Xác minh chính thức là một kỹ thuật sử dụng logic toán học để đảm bảo rằng hệ thống tuân thủ các thông số kỹ thuật để nó hoạt động như mong đợi trong tất cả các điều kiện và đầu vào có thể có. Trong bài viết này, chúng tôi sẽ giới thiệu các bước cụ thể để xác minh chính thức mô-đun Cosmos SDK Bank, cũng như một số kết quả xác minh.
SDK Cosmos là gì?
Bộ công cụ phát triển phần mềm Cosmos (viết tắt là SDK) là một framework cho phép các nhà phát triển xây dựng các ứng dụng blockchain tùy chỉnh. Sử dụng SDK Cosmos, các nhà phát triển có thể dễ dàng khởi chạy chuỗi khối Lớp 1 của riêng mình mà không phải lo lắng về việc thiết kế và triển khai từ lớp đồng thuận đến lớp ứng dụng. SDK Cosmos cung cấp các mô-đun lõi tiêu chuẩn có thể được nhập và sử dụng trực tiếp bởi bất kỳ chuỗi nào, chẳng hạn như các mô-đun đặt cược, xác thực, gov và đúc tiền.
nguồn:
Phân hệ ngân hàng
Mô-đun ngân hàng trong Cosmos SDK chịu trách nhiệm về tất cả các chức năng liên quan đến quản lý mã thông báo, chẳng hạn như chuyển mã thông báo gốc. Việc gửi mã thông báo cần phải đáp ứng nhiều hạn chế và điều kiện, chẳng hạn như có đủ mã thông báo có sẵn trong tài khoản, ngoại trừ những mã thông báo đã được đặt cọc, bị khóa hoặc đang được hủy liên kết. Với sự hỗ trợ của các mô-đun như đặt cược và xác thực, mô-đun ngân hàng quản lý toàn bộ quá trình gửi mã thông báo. Mặc dù mô-đun ngân hàng phụ thuộc vào một số mô-đun khác, vì chúng nằm ngoài phạm vi xác minh chính thức này nên chúng tôi đưa ra một số giả định về chức năng của chúng để đơn giản hóa quy trình.
Mô-đun ngân hàng của SDK bao gồm một số mô-đun phụ, bao gồm cả trình giữ và loại, là các thành phần cốt lõi xác định hành vi và loại dữ liệu của mô-đun. Chúng tôi sẽ tập trung vào mô-đun con người giữ vì nó bao gồm các chức năng và tính năng chính của mô-đun.
Mô-đun con người giữ có hai thành phần chính: xem và gửi. Người giữ chế độ xem chịu trách nhiệm quản lý tài khoản và số dư, trong khi người giữ gửi chịu trách nhiệm thay đổi số dư tài khoản, chẳng hạn như chuyển và đặt cọc các mã thông báo bị khóa hoặc mở khóa. Luồng hoạt động của mô-đun ngân hàng được thể hiện trong hình bên dưới. Các mũi tên chỉ hướng từ các thành phần đến các chức năng hoặc Keepers.
nguồn:
Phương pháp xác thực
Như đã đề cập trước đó, phạm vi xác minh này được giới hạn ở mô-đun ngân hàng. Trước khi bắt đầu xác minh, trước tiên chúng tôi xây dựng đặc tả chính thức cho các loại dữ liệu trong mô-đun ngân hàng. Ví dụ: có một cấu trúc dữ liệu mã thông báo trong mô-đun ngân hàng, chứa tên loại chuỗi và số lượng loại big.Int, được xác định trong mã nguồn như sau:
Cấu trúc rất đơn giản và chúng tôi định nghĩa nó bằng Coq (ngôn ngữ xác minh chính thức và mô hình hóa của chúng tôi) như sau:
Dựa trên định nghĩa này, trước tiên chúng tôi chứng minh một số tính chất về hoạt động cơ bản của tiền xu để đặt nền tảng cho tính toàn vẹn chức năng của mô-đun ngân hàng, đòi hỏi phải thường xuyên sửa đổi và thao tác với loại tiền xu. Ví dụ:
Bổ đề này chứng minh một bất biến cơ bản: trừ đi hai đồng xu không làm thay đổi mệnh giá của chúng cũng như không dẫn đến số dư âm.
Tương tự như ví dụ trước, các thành phần cơ bản của mỗi lần chuyển đổi trạng thái được mô hình hóa trong Coq, bao gồm KV Store, GasMeter, Xử lý lỗi và Ngữ cảnh.
Để biết thông số kỹ thuật chi tiết của các loại dữ liệu và xác minh của chúng, vui lòng xem:
Làm mẫu thủ môn
Sau khi hoàn thành việc mô hình hóa các thành phần cơ bản, chúng ta có thể mô hình hóa người giữ lõi của module ngân hàng để mô tả các chức năng của module. Người giữ ngân hàng có hai giao diện, một giao diện để truy cập chỉ đọc vào dữ liệu mã thông báo và giao diện còn lại để chuyển mã thông báo và bảo trì nguồn cung cấp.
Người giữ chế độ xem chịu trách nhiệm xử lý quyền truy cập chỉ đọc vào số dư tài khoản và có bốn chức năng tính toán số dư tài khoản:
GetBalance: Truy vấn số dư tài khoản của một mệnh giá cụ thể thông qua địa chỉ. Nó xem xét hai trường hợp: một chuỗi các byte rỗng và một chuỗi các byte không rỗng. Xác minh chính thức đảm bảo rằng hàm GetBalance tạo ra kết quả chính xác trong cả hai trường hợp.
LockedCoins: Trả về tất cả các token không thể chi tiêu trong tài khoản tương ứng với một địa chỉ. Do hạn chế về thời gian, chúng tôi đã đưa ra giả định về một số cách triển khai từ mô-đun xác thực.
GetAllBalances: Trả về tất cả số dư tài khoản theo địa chỉ được chỉ định.
GetAccountsBalances: Trả về tất cả số dư tài khoản từ bộ lưu trữ, với các trường BAddress và BCoins làm bản ghi.
Trình quản lý gửi xử lý việc chuyển và cung cấp mã thông báo. Trong quá trình chuyển giao, nó duy trì việc cung cấp mã thông báo để không có mã thông báo mới nào được đúc.
SetBalance: Đặt số dư token cho tài khoản thông qua địa chỉ. Hàm này xem xét hai trường hợp: số dư được đặt thành 0 và số dư được đặt thành khác 0. Trong cả hai trường hợp, tính đúng đắn của SetBalance đều được chứng minh.
subUnlockedCoin: Trừ số tiền (mã thông báo) được chỉ định từ một địa chỉ. Hàm đệ quy subUnlockedCoins thực hiện tương tự đối với một tập hợp mã thông báo. Các thuộc tính liên quan của các hàm này được coi là các giả định tiên đề.
addCoin: Thêm một số tiền (mã thông báo) được chỉ định vào một địa chỉ. Hàm đệ quy addCoins thực hiện thao tác tương tự trên một bộ mã thông báo. Các thuộc tính liên quan của các hàm này được coi là các giả định tiên đề.
SendCoins: Gửi số tiền từ địa chỉ tài khoản này sang địa chỉ tài khoản khác để tiền của cả hai địa chỉ được cập nhật. Nếu người nhận không tồn tại, một tài khoản mới sẽ được tạo cho người nhận đó.
Sử dụng mô hình của các thành phần cốt lõi ở trên, chúng ta có thể bắt đầu xác minh.
Quá trình xác minh
Việc xác minh của chúng tôi được thực hiện bằng cách mô tả chính thức các thuộc tính bất biến của các hàm này và chứng minh chúng trong hệ thống chứng minh phụ trợ, tập trung chủ yếu vào chức năng cốt lõi của "View Keeper" và "Send Keeper".
Ví dụ: đặc tả và bổ đề setBalance_ok chứng minh tính đúng đắn của hàm setBalance của mô-đun BaseSendKeeper, cụ thể chứng minh các thuộc tính sau:
Khi send.setBalance trở về trạng thái "Ok", có newMultiStore. Lúc này, môi trường cập nhật uctx được lấy từ môi trường cũ ctx ban đầu bằng cách cập nhật newMultiStore.
Số dư được đặt là một token hợp lệ (nó có các thuộc tính bắt buộc của một token trong hệ thống).
Mối quan hệ của setBalance_prop được duy trì để đảm bảo rằng hàm cập nhật số dư trong newMultiStore theo cách mong đợi và tạo ra môi trường cập nhật uctx.
Sau khi cài đặt số dư hoàn tất, hãy sử dụng địa chỉ tài khoản addr và số dư mệnh giá (Denom) để gọi view.GetBalance trên môi trường được cập nhật uctx và số dư tương tự do send.setBalance đặt sẽ được trả về.
Các thuộc tính này được mô tả bằng ngôn ngữ đặc tả Coq như sau:
Đối với mã Coq có tính chất khác, hãy truy cập:
###sự nghiệp tương lai
Cơ sở của việc xác minh này được xây dựng dựa trên một số giả định và tiên đề mà chúng ta có thể xác minh sâu hơn để mở rộng phạm vi xác minh. Công việc trong tương lai tập trung vào các lĩnh vực sau:
Xác minh các giả định: Việc xác minh hiện tại dựa trên một loạt các giả định làm cơ sở cho bằng chứng. Những giả định này có thể được kiểm tra trong tương lai để đảm bảo rằng chúng phản ánh chính xác hành vi và đặc tính dự kiến của hệ thống.
Xác minh mô-đun xác thực: Mô-đun này chịu trách nhiệm quản lý dữ liệu tài khoản và cơ chế chữ ký và là thành phần cốt lõi của Cosmos SDK. Trong tương lai, nó có thể được xác minh chính thức đầy đủ để đảm bảo rằng việc triển khai và tương tác mô-đun với các mô-đun khác là chính xác.
Thêm định lý về ủy thác, đúc và bán coin: Mở rộng phạm vi xác minh và đưa thêm các định lý về ủy quyền, đúc và bán coin sẽ giúp hiểu rõ hơn về cơ chế vận hành của hệ thống một cách toàn diện hơn. Các định lý này có thể được kết hợp với việc xác minh mô-đun xác thực để đảm bảo tính nhất quán và chính xác tổng thể của hệ thống.
Mở rộng toàn bộ cơ sở hạ tầng Cosmos SDK: công việc xác minh ở giai đoạn này chủ yếu tập trung vào mô-đun ngân hàng và các thành phần liên quan của nó. Trong tương lai, quy trình xác minh chính thức có thể được mở rộng cho toàn bộ cơ sở hạ tầng Cosmos SDK, từ đó nâng cao độ chính xác, bảo mật và ổn định tổng thể của nền tảng, đồng thời cung cấp môi trường ổn định và đáng tin cậy hơn cho nhà phát triển và người dùng.
Tích hợp với các mô-đun khác: Vì Cosmos SDK bao gồm nhiều mô-đun được kết nối với nhau nên việc khám phá các tương tác và phụ thuộc giữa chúng là rất có lợi. Điều này yêu cầu xác minh tính chính xác của các tương tác giữa các mô-đun và đảm bảo rằng mọi thay đổi đối với một mô-đun không ảnh hưởng xấu đến các mô-đun khác.
Mô hình hóa và xác minh các cơ chế khuyến khích: Cosmos SDK cũng tích hợp các cơ chế khuyến khích như đặt cược và phân phối phần thưởng. Nghiên cứu trong tương lai sẽ mô hình hóa và xác nhận các cơ chế này để đảm bảo chúng chính xác và phù hợp với các khuyến khích kinh tế dự kiến.
Bài viết này trình bày trường hợp thành công đầu tiên về xác minh chính thức nâng cao của mô-đun Cosmos SDKbank, giúp hoạt động hiệu quả cho nền tảng bảo mật và độ tin cậy của hệ sinh thái blockchain. Công việc trong tương lai sẽ mở rộng thành tựu này bằng cách xác thực các giả định, xác thực các mô-đun khác và bao trùm toàn bộ cơ sở hạ tầng Cosmos SDK, cuối cùng là xây dựng một nền tảng vững chắc và đáng tin cậy hơn cho các nhà phát triển và người dùng.
Xem bản gốc
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.
Giải thích chi tiết việc xác minh chính thức các mô-đun tiêu chuẩn Cosmos SDK
/ Xác minh chính thức nâng cao ngăn xếp phần mềm hoàn chỉnh Web3/
CertiK gần đây đã phát hành báo cáo xác minh chính thức nâng cao về mô-đun Cosmos SDK Bank, theo hiểu biết của chúng tôi, đây là nỗ lực thành công đầu tiên trong việc xác minh chính thức Cosmos SDK. Xác minh chính thức là một kỹ thuật sử dụng logic toán học để đảm bảo rằng hệ thống tuân thủ các thông số kỹ thuật để nó hoạt động như mong đợi trong tất cả các điều kiện và đầu vào có thể có. Trong bài viết này, chúng tôi sẽ giới thiệu các bước cụ thể để xác minh chính thức mô-đun Cosmos SDK Bank, cũng như một số kết quả xác minh.
SDK Cosmos là gì?
Bộ công cụ phát triển phần mềm Cosmos (viết tắt là SDK) là một framework cho phép các nhà phát triển xây dựng các ứng dụng blockchain tùy chỉnh. Sử dụng SDK Cosmos, các nhà phát triển có thể dễ dàng khởi chạy chuỗi khối Lớp 1 của riêng mình mà không phải lo lắng về việc thiết kế và triển khai từ lớp đồng thuận đến lớp ứng dụng. SDK Cosmos cung cấp các mô-đun lõi tiêu chuẩn có thể được nhập và sử dụng trực tiếp bởi bất kỳ chuỗi nào, chẳng hạn như các mô-đun đặt cược, xác thực, gov và đúc tiền.
nguồn:
Phân hệ ngân hàng
Mô-đun ngân hàng trong Cosmos SDK chịu trách nhiệm về tất cả các chức năng liên quan đến quản lý mã thông báo, chẳng hạn như chuyển mã thông báo gốc. Việc gửi mã thông báo cần phải đáp ứng nhiều hạn chế và điều kiện, chẳng hạn như có đủ mã thông báo có sẵn trong tài khoản, ngoại trừ những mã thông báo đã được đặt cọc, bị khóa hoặc đang được hủy liên kết. Với sự hỗ trợ của các mô-đun như đặt cược và xác thực, mô-đun ngân hàng quản lý toàn bộ quá trình gửi mã thông báo. Mặc dù mô-đun ngân hàng phụ thuộc vào một số mô-đun khác, vì chúng nằm ngoài phạm vi xác minh chính thức này nên chúng tôi đưa ra một số giả định về chức năng của chúng để đơn giản hóa quy trình.
Mô-đun ngân hàng của SDK bao gồm một số mô-đun phụ, bao gồm cả trình giữ và loại, là các thành phần cốt lõi xác định hành vi và loại dữ liệu của mô-đun. Chúng tôi sẽ tập trung vào mô-đun con người giữ vì nó bao gồm các chức năng và tính năng chính của mô-đun.
Mô-đun con người giữ có hai thành phần chính: xem và gửi. Người giữ chế độ xem chịu trách nhiệm quản lý tài khoản và số dư, trong khi người giữ gửi chịu trách nhiệm thay đổi số dư tài khoản, chẳng hạn như chuyển và đặt cọc các mã thông báo bị khóa hoặc mở khóa. Luồng hoạt động của mô-đun ngân hàng được thể hiện trong hình bên dưới. Các mũi tên chỉ hướng từ các thành phần đến các chức năng hoặc Keepers.
nguồn:
Phương pháp xác thực
Như đã đề cập trước đó, phạm vi xác minh này được giới hạn ở mô-đun ngân hàng. Trước khi bắt đầu xác minh, trước tiên chúng tôi xây dựng đặc tả chính thức cho các loại dữ liệu trong mô-đun ngân hàng. Ví dụ: có một cấu trúc dữ liệu mã thông báo trong mô-đun ngân hàng, chứa tên loại chuỗi và số lượng loại big.Int, được xác định trong mã nguồn như sau:
Cấu trúc rất đơn giản và chúng tôi định nghĩa nó bằng Coq (ngôn ngữ xác minh chính thức và mô hình hóa của chúng tôi) như sau:
Dựa trên định nghĩa này, trước tiên chúng tôi chứng minh một số tính chất về hoạt động cơ bản của tiền xu để đặt nền tảng cho tính toàn vẹn chức năng của mô-đun ngân hàng, đòi hỏi phải thường xuyên sửa đổi và thao tác với loại tiền xu. Ví dụ:
Bổ đề này chứng minh một bất biến cơ bản: trừ đi hai đồng xu không làm thay đổi mệnh giá của chúng cũng như không dẫn đến số dư âm.
Tương tự như ví dụ trước, các thành phần cơ bản của mỗi lần chuyển đổi trạng thái được mô hình hóa trong Coq, bao gồm KV Store, GasMeter, Xử lý lỗi và Ngữ cảnh.
Để biết thông số kỹ thuật chi tiết của các loại dữ liệu và xác minh của chúng, vui lòng xem:
Làm mẫu thủ môn
Sau khi hoàn thành việc mô hình hóa các thành phần cơ bản, chúng ta có thể mô hình hóa người giữ lõi của module ngân hàng để mô tả các chức năng của module. Người giữ ngân hàng có hai giao diện, một giao diện để truy cập chỉ đọc vào dữ liệu mã thông báo và giao diện còn lại để chuyển mã thông báo và bảo trì nguồn cung cấp.
Người giữ chế độ xem chịu trách nhiệm xử lý quyền truy cập chỉ đọc vào số dư tài khoản và có bốn chức năng tính toán số dư tài khoản:
GetBalance: Truy vấn số dư tài khoản của một mệnh giá cụ thể thông qua địa chỉ. Nó xem xét hai trường hợp: một chuỗi các byte rỗng và một chuỗi các byte không rỗng. Xác minh chính thức đảm bảo rằng hàm GetBalance tạo ra kết quả chính xác trong cả hai trường hợp.
LockedCoins: Trả về tất cả các token không thể chi tiêu trong tài khoản tương ứng với một địa chỉ. Do hạn chế về thời gian, chúng tôi đã đưa ra giả định về một số cách triển khai từ mô-đun xác thực.
GetAllBalances: Trả về tất cả số dư tài khoản theo địa chỉ được chỉ định.
GetAccountsBalances: Trả về tất cả số dư tài khoản từ bộ lưu trữ, với các trường BAddress và BCoins làm bản ghi.
Trình quản lý gửi xử lý việc chuyển và cung cấp mã thông báo. Trong quá trình chuyển giao, nó duy trì việc cung cấp mã thông báo để không có mã thông báo mới nào được đúc.
SetBalance: Đặt số dư token cho tài khoản thông qua địa chỉ. Hàm này xem xét hai trường hợp: số dư được đặt thành 0 và số dư được đặt thành khác 0. Trong cả hai trường hợp, tính đúng đắn của SetBalance đều được chứng minh.
subUnlockedCoin: Trừ số tiền (mã thông báo) được chỉ định từ một địa chỉ. Hàm đệ quy subUnlockedCoins thực hiện tương tự đối với một tập hợp mã thông báo. Các thuộc tính liên quan của các hàm này được coi là các giả định tiên đề.
addCoin: Thêm một số tiền (mã thông báo) được chỉ định vào một địa chỉ. Hàm đệ quy addCoins thực hiện thao tác tương tự trên một bộ mã thông báo. Các thuộc tính liên quan của các hàm này được coi là các giả định tiên đề.
SendCoins: Gửi số tiền từ địa chỉ tài khoản này sang địa chỉ tài khoản khác để tiền của cả hai địa chỉ được cập nhật. Nếu người nhận không tồn tại, một tài khoản mới sẽ được tạo cho người nhận đó.
Sử dụng mô hình của các thành phần cốt lõi ở trên, chúng ta có thể bắt đầu xác minh.
Quá trình xác minh
Việc xác minh của chúng tôi được thực hiện bằng cách mô tả chính thức các thuộc tính bất biến của các hàm này và chứng minh chúng trong hệ thống chứng minh phụ trợ, tập trung chủ yếu vào chức năng cốt lõi của "View Keeper" và "Send Keeper".
Ví dụ: đặc tả và bổ đề setBalance_ok chứng minh tính đúng đắn của hàm setBalance của mô-đun BaseSendKeeper, cụ thể chứng minh các thuộc tính sau:
Khi send.setBalance trở về trạng thái "Ok", có newMultiStore. Lúc này, môi trường cập nhật uctx được lấy từ môi trường cũ ctx ban đầu bằng cách cập nhật newMultiStore.
Số dư được đặt là một token hợp lệ (nó có các thuộc tính bắt buộc của một token trong hệ thống).
Mối quan hệ của setBalance_prop được duy trì để đảm bảo rằng hàm cập nhật số dư trong newMultiStore theo cách mong đợi và tạo ra môi trường cập nhật uctx.
Sau khi cài đặt số dư hoàn tất, hãy sử dụng địa chỉ tài khoản addr và số dư mệnh giá (Denom) để gọi view.GetBalance trên môi trường được cập nhật uctx và số dư tương tự do send.setBalance đặt sẽ được trả về.
Các thuộc tính này được mô tả bằng ngôn ngữ đặc tả Coq như sau:
Đối với mã Coq có tính chất khác, hãy truy cập:
###sự nghiệp tương lai
Cơ sở của việc xác minh này được xây dựng dựa trên một số giả định và tiên đề mà chúng ta có thể xác minh sâu hơn để mở rộng phạm vi xác minh. Công việc trong tương lai tập trung vào các lĩnh vực sau:
Xác minh các giả định: Việc xác minh hiện tại dựa trên một loạt các giả định làm cơ sở cho bằng chứng. Những giả định này có thể được kiểm tra trong tương lai để đảm bảo rằng chúng phản ánh chính xác hành vi và đặc tính dự kiến của hệ thống.
Xác minh mô-đun xác thực: Mô-đun này chịu trách nhiệm quản lý dữ liệu tài khoản và cơ chế chữ ký và là thành phần cốt lõi của Cosmos SDK. Trong tương lai, nó có thể được xác minh chính thức đầy đủ để đảm bảo rằng việc triển khai và tương tác mô-đun với các mô-đun khác là chính xác.
Thêm định lý về ủy thác, đúc và bán coin: Mở rộng phạm vi xác minh và đưa thêm các định lý về ủy quyền, đúc và bán coin sẽ giúp hiểu rõ hơn về cơ chế vận hành của hệ thống một cách toàn diện hơn. Các định lý này có thể được kết hợp với việc xác minh mô-đun xác thực để đảm bảo tính nhất quán và chính xác tổng thể của hệ thống.
Mở rộng toàn bộ cơ sở hạ tầng Cosmos SDK: công việc xác minh ở giai đoạn này chủ yếu tập trung vào mô-đun ngân hàng và các thành phần liên quan của nó. Trong tương lai, quy trình xác minh chính thức có thể được mở rộng cho toàn bộ cơ sở hạ tầng Cosmos SDK, từ đó nâng cao độ chính xác, bảo mật và ổn định tổng thể của nền tảng, đồng thời cung cấp môi trường ổn định và đáng tin cậy hơn cho nhà phát triển và người dùng.
Tích hợp với các mô-đun khác: Vì Cosmos SDK bao gồm nhiều mô-đun được kết nối với nhau nên việc khám phá các tương tác và phụ thuộc giữa chúng là rất có lợi. Điều này yêu cầu xác minh tính chính xác của các tương tác giữa các mô-đun và đảm bảo rằng mọi thay đổi đối với một mô-đun không ảnh hưởng xấu đến các mô-đun khác.
Mô hình hóa và xác minh các cơ chế khuyến khích: Cosmos SDK cũng tích hợp các cơ chế khuyến khích như đặt cược và phân phối phần thưởng. Nghiên cứu trong tương lai sẽ mô hình hóa và xác nhận các cơ chế này để đảm bảo chúng chính xác và phù hợp với các khuyến khích kinh tế dự kiến.
Bài viết này trình bày trường hợp thành công đầu tiên về xác minh chính thức nâng cao của mô-đun Cosmos SDKbank, giúp hoạt động hiệu quả cho nền tảng bảo mật và độ tin cậy của hệ sinh thái blockchain. Công việc trong tương lai sẽ mở rộng thành tựu này bằng cách xác thực các giả định, xác thực các mô-đun khác và bao trùm toàn bộ cơ sở hạ tầng Cosmos SDK, cuối cùng là xây dựng một nền tảng vững chắc và đáng tin cậy hơn cho các nhà phát triển và người dùng.