Ethereum istemcisinin güven tabanını azaltacak 5 doğrulama yolu

Ethereum istemcisinin güvenilirlik varsayımlarına dayanan temelini (TCB) azaltmak için biçimsel doğrulama yaklaşımı ve beş uygulama yolu açıklandı.

Ethereum Vakfı üyeleri George Kadianakis ve Kev Wedderburn, 25'inde Ethereum Araştırma Forumu'nda konuyla ilgili bir yazı yayımladı. Yazıda, biçimsel doğrulama yoluyla Ethereum istemcisinde güvenilmesi gereken kapsamın nasıl daraltılabileceği ele alındı.

TCB; doğrulanmış olmaktan ziyade güven varsayımıyla kullanılan bileşenleri, spesifikasyonları, araçları ve kabulleri ifade ediyor. Yazının temel yaklaşımına göre biçimsel doğrulama TCB'yi tamamen ortadan kaldırmasa da insanların doğrudan güvenmek zorunda olduğu alanı daraltabilir.

Araştırmacılar, soyutlanmış istemciyi birden fazla modüle ayırarak her modülün rolünü ve sağladığı güvenceleri ayrı ayrı doğrulamayı önerdi. Modül bazındaki güvenceler arayüzler aracılığıyla birleştirildiğinde istemcinin tamamına ilişkin güvenlik özelliklerinin kontrol edilebileceği belirtildi.

Temel ayrım 'saf modüller' ile 'saf olmayan modüller' arasında yapılıyor. Kriptografi, SSZ ve çatallanma seçimi kuralları gibi yan etkilerin sınırlı, matematiksel yapının açık olduğu alanlar biçimsel doğrulamaya uygun saf modüller olarak sınıflandırıldı. Girdi ve çıktıların yanı sıra dış durumu, mesaj sırasını, bağlantı kopmalarını ve gecikmeleri dikkate alması gereken ağ gibi alanlar ise saf olmayan modüller olarak değerlendirildi.

Araştırmacılar, saf olmayan modüllerin başlangıçtan itibaren güvenilmeyen bir yapıda tasarlanmasını önerdi. Örneğin ağ modülünün ilettiği imzaya doğrudan güvenmek yerine imza, saf bir imza doğrulama modülünde yeniden işlenebilir. Böylece ağ modülündeki hatalar kötü niyetli dış girdilerle benzer şekilde ele alınabilir.

Uzun vadede doğrulama sınırının ağa daha yakın bir noktaya taşınması da önerildi. Tüm ağı modellemek yerine ayrıştırıcının, dedikodu kurallarının ve senkronizasyon mantığının öncelikli olarak doğrulanmasıyla hatalı mesajların sistemi durdurması veya aşırı kaynak tüketmesine yol açması engellenebilir.

Yazıda spesifikasyon ile gerçek çalıştırılabilir dosya arasındaki bağlantı da ayrı bir çalışma alanı olarak gösterildi. Araştırmacılar, Lean4 ile biçimsel spesifikasyon yazıp özellikleri kanıtlamakla gerçek uygulamanın bu spesifikasyona uyduğunu kanıtlamayı birbirinden ayırdı. Kullanıcılar Lean4 teoremlerinden ziyade kendi bilgisayarlarında çalışan kodun güvenliğine önem verdiği için her iki aşamanın da gerekli olduğu belirtildi.

Uygulama yolları arasında △Rust gibi dillerle yazılmış kodu Lean4'e otomatik olarak dönüştürmek △Lean4 ile yazılan modülleri C koduna aktarmak △istemcinin kendisini Lean4 ile yazıp yan etkileri fazla olan modülleri başka dillere bağlamak △temel modülleri doğrudan RISC-V assembly ile yazmak △doğrulanmış bir derleyici kullanmak yer aldı.

Rust kodunun Lean4'e dönüştürülmesi halinde dönüştürücü ve nihai ikili dosyayı oluşturan Rust derleyicisi TCB içinde kalıyor. Lean4 kodunun C'ye aktarılması veya istemcinin büyük bölümünün Lean4 ile yazılması durumunda ise aktarım aracı, C derleyicisi ve harici işlev arayüzü güvenilmesi gereken bileşenler arasına giriyor.

Temel modüllerin RISC-V assembly ile yazılması, genel amaçlı derleyicinin TCB dışında bırakılmasını sağlayabilir. Ancak bu durumda RISC-V komut setinin biçimsel modeli ve assembly kodunu başka bir işlemciye yönelik koda dönüştüren araçlar yeni güven unsurları haline gelir. Doğrulanmış bir derleyici kullanıldığında ise aktarım aracı ve C derleyicisi TCB dışında bırakılabilir.

Araştırmacılar, tüm modüllere tek bir yöntemin uygulanmasının gerekmediğini belirtti. Matematiksel yapısı güçlü modüller Lean4 ile doğrulanırken veri yapıları karmaşık veya ölçeği büyük modüllerde dönüştürücülerin ya da doğrulanmış derleyicilerin kullanıldığı karma bir yaklaşım da uygulanabilir.

Yazı, Ethereum istemcisinin tamamında biçimsel doğrulamanın hâlihazırda tamamlandığına ilişkin bir duyuru değil. Çalışma, biçimsel spesifikasyon, uygulama ve derleme sürecine uzanan doğrulamanın hangi birimlere ayrılabileceği ve kapsamının ne kadar genişletilebileceği konusunda bir tasarım yönü sunuyor.