Input Output, Cardano akıllı sözleşme doğrulaması için Blaster'ı gösteriyor

Cardano Community, Cardano akıllı sözleşmelerinin belirlenen kurallara uyup uymadığını kontrol etmek için tasarlanmış otomatik bir doğrulama aracı olan Blaster'ın bir sunumunu yayımladı. Input Output mühendisleri Romain Soulat ve Jean-Frédéric Etienne, aracın bu özellikleri nasıl incelediğini ve bir ihlal bulduğunda nasıl bir karşı örnek üretebildiğini gösteriyor. Ayrıca kanıt yeniden kurma üzerindeki devam eden çalışmaları ve sonuçların incelenmesini kolaylaştırma yollarını tartışıyorlar.

Bir Cardano sözleşmesinin ne yapması gerektiğini tanımlamak

Akıllı sözleşmeler, blok zinciri işlemleri için koşullar belirler ve uygulamaların varlıkları nasıl ele alacağını belirler. Örneğin bir geliştirici, bir sözleşme tarafından tutulan fonların yalnızca yetkili bir kullanıcı tarafından kilidinin açılabileceğini belirtebilir. Biçimsel doğrulama, bir sistemin bir belirtimde yazılı özellikleri karşılayıp karşılamadığını kontrol etmek için matematiksel yöntemler kullanır. Geleneksel bir test seçilmiş durumları incelerken, biçimsel doğrulama, modelin kapsadığı durumlar genelinde belirtilen bir özelliğin geçerli olup olmadığını ortaya koymayı amaçlar.

Cardano High Assurance için teknik lider olan Soulat, Blaster'ın kanıt çalışmasının büyük bir kısmını otomatikleştirmek amacıyla geliştirildiğini açıkladı. Geliştiricilerin yine de kontrol etmek istedikleri davranışı tanımlamaları ve buna karşılık gelen belirtimi sağlamaları gerekiyor. Araç bir ihlal bulduğunda, incelenmek üzere bir karşı örnek üretebiliyor. Soulat, yetkili kullanıcıdan başka birinin bir çıktının kilidini açtığını gösterebilecek bir işlem ya da işlem dizisi tasvir etti.

Blaster sözleşme özelliklerini nasıl kontrol ediyor

Blaster, matematiksel ifadeleri dile getirmek ve kanıtlarla çalışmak için kullanılan bir sistem olan Lean 4'ü, otomatik bir çözücüyle birlikte kullanır. Önce problemi basitleştirir; özellik bu aşamada çözümlenmezse kalan problem çözücüye gönderilebilir. Kontrolleri Cardano ile ilgili kılmak için ekip, betik yürütme ve işlem kuralları dahil olmak üzere sözleşmelerin çalıştığı ortamın bazı bölümlerini biçimselleştirdi.

Bir kıdemli biçimsel yöntemler mühendisi olan Etienne, üç olası sonuç ortaya koydu: bir özellik geçerli, yanlışlanmış ya da belirlenememiş olarak raporlanabilir. Yanlışlanmış bir sonuca eşlik eden bir karşı örnek, geliştiricilerin bir sözleşme hatasını, eksik bir varsayımı ya da belirtimdeki bir hatayı belirlemesine yardımcı olabilir. Belirlenememiş sonucu, çözücünün özelliğin geçerli olup olmadığını ortaya koyamadığı anlamına gelir. Bir kontrolün kapsamı, geliştiricilerin ifade etmeyi seçtiği özelliklere bağlıdır.

[NEWSBREAK]

Kanıt yeniden kurma geliştirme aşamasında

Geliştiriciler, Plinth, Aiken ya da Plutarch gibi dillerde yazılmış sözleşmeleri, Cardano betiklerini yürütmek için kullanılan temsili olan Untyped Plutus Core'a derleyebilir. Daha sonra derlenen kodu Lean 4'e aktarabilir ve kontrol edilecek özellikleri belirtebilirler. Input Output daha önce, bu süreç için Cardano'ya özgü modeller sağlayan iki açık kaynaklı kütüphane yayımladı. Daha önceki bir gösterimde ekip, bir güvenlik zorluğundaki alıştırma amaçlı bir sözleşme üzerinde ardışık düzeni kullandı ve sözleşmenin nasıl istismar edilebileceğini gösteren bir işlem bağlamı üretti.

Etienne, kanıt yeniden kurmanın hâlâ geliştirme aşamasında olduğunu açıkladı. Amaç, geçerli bir sonucu destekleyen kanıtı Lean'in bağımsız olarak denetlemesine olanak tanımaktır; mevcut araç, çözücü bu sonucu döndürdüğünde henüz yeniden kurulmuş bir Lean kanıtı üretmiyor. Soulat ayrıca geliştiricilerin başarısız bir özelliğin arkasındaki işlem ayrıntılarını incelemesine olanak tanıyacak daha açık karşı örnek görünümleri için planları da özetledi.