Ethereum Gizlilik Havuzu, Sepolia Koduna Kadar Biçimsel Olarak Doğrulandı

EthSystems, Ethereum (ETH) gizlilik havuzunun tasarım belgelerinden Sepolia test ağında çalışan koda kadar biçimsel doğrulamayı tamamladı. Süreçte 6 sorun tespit edildi; bunların 3’ü doğrulama araçlarından kaynaklandı.

EthSystems sonuçları 27’sinde açıkladı. PANews bu bilgiyi aktardı. Gizlilik havuzu, işlem bilgilerini gizlerken işlemlerin belirlenen kurallara uygunluğunun doğrulanmasını sağlayacak şekilde tasarlandı. Bu doğrulamada tasarım belgelerindeki gerekliliklerin uygulamaya ve dağıtılan koda aşama aşama yansıyıp yansımadığı incelendi.

Biçimsel doğrulama, bir programın karşılaması gereken koşulların matematiksel olarak ifade edilip araçlarla sağlanıp sağlanmadığının kontrol edilmesi yöntemidir. EthSystems model, devre ve hash doğrulaması için Lean’i; akıllı sözleşme doğrulaması için Halmos ve Kontrol’ü kullandı. Cüzdanı ise Aeneas ve Verus ile inceledi.

Doğrulayıcı ve dağıtım aşamalarında kod yeniden oluşturuldu ve Sepolia test ağında çalışan bayt koduyla bayt düzeyinde karşılaştırıldı. Bayt kodu, ağın fiilen çalıştırdığı koddur. Bu yöntemle tasarım belgeleri ve insanların okuyabildiği kod üzerindeki inceleme sonuçlarının dağıtılan koda da yansıyıp yansımadığı kontrol edildi.

Temel doğrulama hedefleri çift harcamayı önlemek ve değeri korumaktı. Bunlar, aynı varlığın iki kez kullanılmasını veya işlem sırasında dayanağı olmayan bir değer artışını önlemeye yönelik koşullardır. EthSystems, her iki koşulun da Lean teorem kanıtlayıcısıyla makine tarafından doğrulandığını açıkladı.

Doğrulama sürecinde 6 sorun bulundu; bunların 3’ü doğrulama araçlarından kaynaklandı. EthSystems, açıklamasında sorunların içeriğini veya düzeltilip düzeltilmediğini belirtmedi.

Sonuçlar bazı varsayımlara dayanıyor. PANews’in aktardığına göre EthSystems, hash çakışmasının bulunmamasını, sahte kanıtların reddedilmesini ve akıllı sözleşmenin davranışıyla doğrulama modelinin uyumlu olmasını varsayımlar arasında saydı. Bu nedenle doğrulama sonuçları, söz konusu koşulların geçerli olduğu sınırlar içinde değerlendirilmelidir.

EthSystems, Ethereum’un herkese açık defterinde işlem bilgilerinin görünür olması sorununa yönelik kurumsal gizlilik teknolojileri geliştiriyor. Şirketin son açıklaması, tasarım belgelerinden test ağında çalışan koda kadar doğrulanan kapsamı ve geçerliliği için gereken varsayımları ortaya koydu.