Cosmos SDK standart modüllerinin resmi doğrulamasının ayrıntılı açıklaması

Bu makalede Cosmos SDK Bank modülünü resmi olarak doğrulamak için belirli adımların yanı sıra bazı doğrulama sonuçlarını tanıtacağız.

/ Web3 tam yazılım yığını gelişmiş resmi doğrulama /

CertiK kısa süre önce Cosmos SDK Bank modülü hakkında gelişmiş bir resmi doğrulama raporu yayınladı; bu rapor, bildiğimiz kadarıyla Cosmos SDK'nın resmi doğrulanmasına yönelik ilk başarılı girişimdir. Biçimsel doğrulama, bir sistemin tüm olası girdiler ve koşullar altında beklendiği gibi davranacak şekilde spesifikasyonlara uygun olmasını sağlamak için matematiksel mantığı kullanan bir tekniktir. Bu makalede Cosmos SDK Bank modülünü resmi olarak doğrulamak için belirli adımların yanı sıra bazı doğrulama sonuçlarını tanıtacağız.

Cosmos SDK'sı nedir?

Cosmos Yazılım Geliştirme Kiti (kısaca SDK), geliştiricilerin özel blockchain uygulamaları oluşturmasına olanak tanıyan bir çerçevedir. Geliştiriciler, Cosmos SDK'yı kullanarak, fikir birliği katmanından uygulama katmanına kadar tasarım ve uygulama konusunda endişelenmelerine gerek kalmadan kendi Katman 1 blok zincirlerini kolayca başlatabilirler. Cosmos SDK, staking, auth, gov ve mint modülleri gibi doğrudan içe aktarılabilen ve herhangi bir zincir tarafından kullanılabilen standart çekirdek modüller sağlar.

kaynak:

Banka modülü

Cosmos SDK'daki banka modülü, yerel tokenlerin aktarımı gibi token yönetimiyle ilgili tüm işlevlerden sorumludur. Token göndermenin birçok kısıtlama ve koşulu karşılaması gerekir: Örneğin, hesapta stake edilmiş, kilitlenmiş veya ayrıştırılma sürecinde olan tokenlar hariç yeterli miktarda kullanılabilir token bulunmalıdır. Banka modülü, staking ve auth gibi modüllerin desteğiyle token gönderme sürecinin tamamını yönetir. Her ne kadar banka modülü başka modüllere bağlı olsa da, bunlar bu resmi doğrulamanın kapsamına girmediğinden, süreci basitleştirmek amacıyla işlevselliği hakkında bazı varsayımlarda bulunduk.

SDK'nın banka modülü, modül davranışını ve veri türlerini tanımlayan temel bileşenler olan kaleci ve türler de dahil olmak üzere çeşitli alt modüllerden oluşur. Modülün ana fonksiyonlarını ve özelliklerini kapsadığı için kaleci alt modülüne odaklanacağız.

Kaleci alt modülünün iki temel bileşeni vardır: görüntüleme ve gönderme. Görünüm koruyucusu, hesapları ve bakiyeleri yönetmekten sorumludur; gönderme koruyucusu ise kilitli veya kilidi açılmış tokenların aktarılması ve stake edilmesi gibi hesap bakiyelerinin değiştirilmesinden sorumludur. Bank modülünün akışı aşağıdaki şekilde gösterilmektedir.Oklar, bileşenlerden işlevlere veya Koruyuculara doğru yönü gösterir.

kaynak:

Kimlik doğrulama yöntemi

Daha önce de belirttiğimiz gibi bu doğrulamanın kapsamı banka modülü ile sınırlıdır. Doğrulama başlamadan önce ilk olarak banka modülündeki veri türleri için resmi spesifikasyonları formüle ediyoruz. Örneğin banka modülünde string tipinin değerini ve big.Int tipinin miktarını içeren, kaynak kodunda aşağıdaki gibi tanımlanan bir token veri yapısı bulunmaktadır:

Bu yapı oldukça basittir ve Coq'u (modelleme ve resmi doğrulama dilimiz) kullanarak aşağıdaki şekilde tanımlarız:

Bu tanıma dayanarak, banka modülünün işlevsel bütünlüğünün temelini oluşturmak için öncelikle madeni paranın temel işlemleriyle ilgili bazı özellikleri kanıtlıyoruz, çünkü madeni para türünün sık sık değiştirilmesini ve manipülasyonunu gerektirir. Örneğin:

Bu lemma temel bir değişmezliği kanıtlıyor: İki madeni paranın çıkarılması onların değerini değiştirmez veya negatif bakiyeye neden olmaz.

Önceki örneğe benzer şekilde, her durum geçişinin temel bileşenleri Coq'da modellenmiştir. Bu bileşenler arasında KV Mağazası, GasMeter, Hata İşleme ve Bağlam bulunur.

Veri türlerinin ayrıntılı özellikleri ve bunların doğrulanması için lütfen şu adrese bakın:

Kaleciyi modelleyin

Temel bileşenlerin modellemesini tamamladıktan sonra, modülün fonksiyonlarını açıklamak için banka modülünün çekirdek koruyucusunu modelleyebiliriz. Banka sorumlusunun iki arayüzü vardır; biri token verilerine salt okunur erişim için, diğeri ise token transferi ve tedarik bakımı için.

Görünüm koruyucusu, hesap bakiyelerine salt okunur erişimi yönetmekten sorumludur ve hesap bakiyelerini hesaplamak için dört işlev içerir:

1. GetBalance: Belirli bir kuponun hesap bakiyesini adres aracılığıyla sorgulayın. İki durumu dikkate alır: bir boş bayt dizisi ve bir boş olmayan bayt dizisi. Resmi doğrulama, GetBalance işlevinin her iki durumda da doğru sonuçlar üretmesini sağlar.

2. LockedCoins: Bir adrese karşılık gelen hesaptaki harcanamayan tüm jetonları döndürür. Zaman kısıtlamalarından dolayı auth modülünden bazı uygulamalara ilişkin varsayımlarda bulunduk.

3. GetAllBalances: Belirtilen adresteki tüm hesap bakiyelerini döndürür.

4. GetAccountsBalances: BAddress ve BCoins alanlarıyla birlikte kayıt olarak depodaki tüm hesap bakiyelerini döndürür.

Gönderme yöneticisi, jeton transferlerini ve tedarikini yönetir. Transfer işlemi sırasında token arzını sürdürür, böylece yeni token basılmaz.

1. SetBalance: Hesap için token bakiyesini adres aracılığıyla ayarlayın. Bu fonksiyon iki durumu dikkate alır: sıfıra ayarlanmış bir bakiye ve sıfırdan farklı bir bakiyeye ayarlanmış. Her iki durumda da SetBalance'ın doğruluğu kanıtlanmıştır.

2. subUnlockedCoin: Bir adresten belirtilen miktarı (jeton) düşer. Yinelemeli subUnlockedCoins işlevi, aynı işlemi bir dizi madeni para üzerinde gerçekleştirir. Bu fonksiyonların ilgili özellikleri aksiyomatik varsayımlar olarak kabul edilir.

3. addCoin: Belirtilen miktarı (jetonları) bir adrese ekleyin. Yinelemeli addCoins işlevi, aynı işlemi bir dizi madeni para üzerinde gerçekleştirir. Bu fonksiyonların ilgili özellikleri aksiyomatik varsayımlar olarak kabul edilir.

4. SendCoins: Her iki adresin fonlarının güncellenmesi için tutarı bir hesap adresinden başka bir hesap adresine gönderin. Alıcı mevcut değilse onun için yeni bir hesap oluşturulacaktır.

Yukarıdaki temel bileşen modelini kullanarak doğrulamaya başlayabiliriz.

Doğrulama süreci

Doğrulamamız, bu işlevlerin değişmez özelliklerini resmi olarak tanımlayarak ve bunları yardımcı bir kanıt sisteminde kanıtlayarak, esas olarak "Görüntüleme Koruyucusu" ve "Gönderme Koruyucusu"nun temel işlevlerine odaklanarak yapılır.

Örneğin, belirtim ve lemma setBalance_ok, BaseSendKeeper modülünün setBalance işlevinin doğruluğunu kanıtlayarak özellikle aşağıdaki özellikleri kanıtlar:

1. send.setBalance "Tamam" durumuna döndüğünde, yeni birMultiStore vardır. Şu anda, güncellenen ortam uctx, newMultiStore'un güncellenmesiyle orijinal eski ortam ctx'inden türetilmiştir.

2. Ayarlanan bakiye geçerli bir jetondur (sistemdeki bir jetonun gerekli özelliklerine sahiptir).

3. setBalance_prop ilişkisi, fonksiyonun newMultiStore'daki bakiyeyi beklenen şekilde güncellemesini ve güncellenmiş uctx ortamını oluşturmasını sağlamak için korunur.

4. Bakiye ayarı tamamlandıktan sonra, güncellenmiş ortamda uctx üzerinde view.GetBalance'ı çağırmak için hesap adresi addr ve mezhep bakiyesini (Denom) kullanın ve send.setBalance tarafından ayarlanan aynı bakiye döndürülecektir.

Bu özellikler Coq spesifikasyon dilinde şu şekilde açıklanmaktadır:

Diğer nitelikteki Coq kodu için şu adresi ziyaret edin:

gelecek kariyeri

Bu doğrulamanın temeli, doğrulamanın kapsamını genişletmek için daha derinlemesine doğrulayabileceğimiz çeşitli varsayımlara ve aksiyomlara dayanmaktadır. Gelecekteki çalışmalar aşağıdaki alanlara odaklanmaktadır:

1. Varsayımların doğrulanması: Mevcut doğrulama, kanıtın temeli olarak bir dizi varsayıma dayanır. Bu varsayımlar, sistemin amaçlanan davranışını ve özelliklerini doğru bir şekilde yansıttıklarından emin olmak için gelecekte test edilebilir.

2. Kimlik doğrulama modülü doğrulaması: Bu modül, hesap verilerinin ve imza mekanizmasının yönetilmesinden sorumludur ve Cosmos SDK'nın temel bileşenidir. Gelecekte, modül uygulamasının ve diğer modüllerle etkileşimin doğru olduğundan emin olmak için tamamen resmi olarak doğrulanabilir.

3. Yetki devri, madeni para basımı ve satışı hakkında daha fazla teorem: Doğrulama kapsamının genişletilmesi ve yetki devri, madeni para basımı ve satışı hakkında daha fazla teorem getirilmesi, sistemin çalışma mekanizmasının daha kapsamlı anlaşılmasına yardımcı olacaktır. Bu teoremler, sistemin genel tutarlılığını ve doğruluğunu sağlamak için kimlik doğrulama modülünün doğrulanmasıyla birleştirilebilir.

4. Cosmos SDK altyapısının tamamını genişletin: Mevcut doğrulama çalışması esas olarak banka modülü ve ilgili bileşenlerine odaklanmıştır. Gelecekte, resmi doğrulama süreci tüm Cosmos SDK altyapısına genişletilebilir, böylece platformun genel doğruluğu, güvenliği ve istikrarı artırılabilir ve geliştiricilere ve kullanıcılara daha istikrarlı ve güvenilir bir ortam sağlanabilir.

5. Diğer modüllerle entegre edin: Cosmos SDK, birbirine bağlı çeşitli modüller içerdiğinden, bunlar arasındaki etkileşimleri ve bağımlılıkları keşfetmek çok faydalıdır. Bu, modüller arasındaki etkileşimlerin doğruluğunun doğrulanmasını ve bir modülde yapılan değişikliklerin diğer modülleri olumsuz etkilememesini sağlamayı gerektirir.

6. Teşvik mekanizmalarının modellenmesi ve doğrulanması: Cosmos SDK ayrıca staking ve ödül dağıtımı gibi teşvik mekanizmalarını da entegre eder. Gelecekteki araştırmalar, bu mekanizmaların doğru ve beklenen ekonomik teşviklerle tutarlı olmasını sağlayacak şekilde modellenecek ve doğrulanacaktır.

Bu makale, blockchain ekosisteminin güvenlik ve güvenilirlik temelini oluşturmak için etkili bir çalışma gerçekleştiren Cosmos SDKbank modülünün gelişmiş resmi doğrulamasının ilk başarılı örneğini göstermektedir. Gelecekteki çalışmalar, varsayımları doğrulayarak, diğer modülleri doğrulayarak ve Cosmos SDK altyapısının tamamını kapsayarak bu başarıyı genişletecek ve sonuçta geliştiriciler ve kullanıcılar için daha sağlam ve güvenilir bir platform oluşturacaktır.