/ 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ün resmi olarak doğrulanmasının belirli adımlarının yanı sıra bazı doğrulama sonuçlarını da 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, stake edilmiş, kilitlenmiş veya bağı çözülmüş olanlar hariç, hesapta yeterli sayıda token bulunması gibi birçok kısıtlama ve koşulu karşılaması gerekir. 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ı dışında olduğundan, süreci basitleştirmek amacıyla işlevleri hakkında bazı varsayımlarda bulunuyoruz.
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 ve ok, bileşenden fonksiyona veya Keeper'a olan 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 kupürlerini değiştirmez ve negatif bakiyeyle sonuçlanmaz.
Önceki örneğe benzer şekilde, KV Store, GasMeter, Error Handling ve Context dahil olmak üzere her durum geçişinin temel bileşenleri Coq'da modellenmiştir.
Veri türlerinin ayrıntılı özellikleri ve bunların doğrulanması için bkz.:
Kaleciyi modelleyin
Temel bileşenlerin modellemesini tamamladıktan sonra, modülün işlevini 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:
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.
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.
GetAllBalances: Belirtilen adresteki tüm hesap bakiyelerini döndürür.
GetAccountsBalances: Kayıt olarak BAddress ve BCoins alanlarıyla birlikte depodaki tüm hesap bakiyelerini döndürür.
Gönderme yöneticisi, token transferleri ve tedarikinden sorumludur. Transferler sırasında token arzını sürdürür, böylece yeni token basılmaz.
SetBalance: Hesabın token bakiyesini adres aracılığıyla ayarlayın. Bu fonksiyon iki durumu dikkate alır: sıfıra ayarlanmış bakiyeler ve sıfırdan farklı bir değere ayarlanmış bakiyeler. Her iki durumda da SetBalance'ın doğruluğu kanıtlanmıştır.
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.
addCoin: Bir adrese belirli bir miktarı (jeton) ekleyin. Yinelemeli addCoins işlevi, aynı işlemi bir dizi jeton üzerinde gerçekleştirir. Bu fonksiyonların ilgili özellikleri aksiyomatik varsayımlar olarak ele alınır.
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:
send.setBalance "Tamam" durumuna döndüğünde, yeni birMultiStore vardır. Şu anda, güncellenmiş ortam uctx, newMultiStore'un güncellenmesiyle orijinal eski ortam ctx'inden türetilmiştir.
Ayarlanan bakiye geçerli bir jetondur (sistemdeki bir jetonun gerekli özelliklerine sahiptir).
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.
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 özelliklerin Coq kodları 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ımlar ve aksiyomlar üzerine kuruludur. Gelecekteki çalışmalar aşağıdaki alanlara odaklanmaktadır:
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.
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.
Madeni paraların emanet edilmesi, basılması ve satılmasına ilişkin daha fazla teorem: Doğrulamanın kapsamının genişletilmesi ve madeni paraların emanet edilmesi, basılması ve satılmasına ilişkin daha fazla teoremin getirilmesi, sistemin işleyiş 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.
Cosmos SDK altyapısının tamamını genişletin: Bu aşamadaki doğrulama çalışması esas olarak banka modülüne 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.
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üldeki herhangi bir değişikliğin diğer modülleri olumsuz etkilememesini sağlamayı gerektirir.
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.
View Original
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
Cosmos SDK standart modüllerinin resmi doğrulamasının ayrıntılı açıklaması
/ 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ün resmi olarak doğrulanmasının belirli adımlarının yanı sıra bazı doğrulama sonuçlarını da 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, stake edilmiş, kilitlenmiş veya bağı çözülmüş olanlar hariç, hesapta yeterli sayıda token bulunması gibi birçok kısıtlama ve koşulu karşılaması gerekir. 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ı dışında olduğundan, süreci basitleştirmek amacıyla işlevleri hakkında bazı varsayımlarda bulunuyoruz.
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 ve ok, bileşenden fonksiyona veya Keeper'a olan 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 kupürlerini değiştirmez ve negatif bakiyeyle sonuçlanmaz.
Önceki örneğe benzer şekilde, KV Store, GasMeter, Error Handling ve Context dahil olmak üzere her durum geçişinin temel bileşenleri Coq'da modellenmiştir.
Veri türlerinin ayrıntılı özellikleri ve bunların doğrulanması için bkz.:
Kaleciyi modelleyin
Temel bileşenlerin modellemesini tamamladıktan sonra, modülün işlevini 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:
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.
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.
GetAllBalances: Belirtilen adresteki tüm hesap bakiyelerini döndürür.
GetAccountsBalances: Kayıt olarak BAddress ve BCoins alanlarıyla birlikte depodaki tüm hesap bakiyelerini döndürür.
Gönderme yöneticisi, token transferleri ve tedarikinden sorumludur. Transferler sırasında token arzını sürdürür, böylece yeni token basılmaz.
SetBalance: Hesabın token bakiyesini adres aracılığıyla ayarlayın. Bu fonksiyon iki durumu dikkate alır: sıfıra ayarlanmış bakiyeler ve sıfırdan farklı bir değere ayarlanmış bakiyeler. Her iki durumda da SetBalance'ın doğruluğu kanıtlanmıştır.
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.
addCoin: Bir adrese belirli bir miktarı (jeton) ekleyin. Yinelemeli addCoins işlevi, aynı işlemi bir dizi jeton üzerinde gerçekleştirir. Bu fonksiyonların ilgili özellikleri aksiyomatik varsayımlar olarak ele alınır.
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:
send.setBalance "Tamam" durumuna döndüğünde, yeni birMultiStore vardır. Şu anda, güncellenmiş ortam uctx, newMultiStore'un güncellenmesiyle orijinal eski ortam ctx'inden türetilmiştir.
Ayarlanan bakiye geçerli bir jetondur (sistemdeki bir jetonun gerekli özelliklerine sahiptir).
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.
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 özelliklerin Coq kodları 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ımlar ve aksiyomlar üzerine kuruludur. Gelecekteki çalışmalar aşağıdaki alanlara odaklanmaktadır:
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.
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.
Madeni paraların emanet edilmesi, basılması ve satılmasına ilişkin daha fazla teorem: Doğrulamanın kapsamının genişletilmesi ve madeni paraların emanet edilmesi, basılması ve satılmasına ilişkin daha fazla teoremin getirilmesi, sistemin işleyiş 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.
Cosmos SDK altyapısının tamamını genişletin: Bu aşamadaki doğrulama çalışması esas olarak banka modülüne 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.
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üldeki herhangi bir değişikliğin diğer modülleri olumsuz etkilememesini sağlamayı gerektirir.
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.