CertiK, zkWasm devresini biçimsel olarak doğruladı; bazı mantıklar kapsam dışında

CertiK’in 2024’te tamamladığı zkWasm çekirdek devresine ilişkin biçimsel doğrulama çalışması yeniden gündeme geldi. Ancak bu, 2026’da tamamlanan yeni bir çalışma değil, daha önce yayımlanan araştırma sonuçlarının yeniden tanıtılması niteliğinde.

CertiK, 2024’te yayımladığı teknik blog yazısında zkWasm’ın Halo2 devresinin geçerli kısıtları karşıladığında WebAssembly (Wasm) yürütme kurallarına uygun bir durumu temsil edip etmediğini doğruladığını açıkladı. Geliştirici Delphinus Lab da 2 Mayıs 2024’te kendi zkWasm uygulamasının biçimsel olarak doğrulandığını duyurdu.

zkWasm, Wasm programını çalıştırdıktan sonra tüm hesaplama sürecini yeniden yürütmeye gerek kalmadan sonucun geçerliliğini kontrol etmeyi sağlayan sıfır bilgi kanıtları üreten bir sistemdir. Program yürütme izleri, Halo2’nin çeşitli tablolarına dönüştürülür ve doğrulayıcı, her tablonun belirlenen aritmetik kısıtları karşılayıp karşılamadığını kontrol eder.

Biçimsel doğrulama, standart bir kod denetiminden farklıdır. Yalnızca bilinen güvenlik açığı kalıplarını aramakla kalmaz; programın belirli koşullarda tanımlanmış kurallara uygun çalışıp çalışmadığını makinelerin kontrol edebileceği matematiksel önermelere dönüştürür.

zkVM’lerde tek bir devre, farklı program yürütmelerini işleyebilir. Bu nedenle devrenin kısıtlarının gerçek Wasm yürütme semantiğiyle örtüşüp örtüşmediğini doğrulamak, kanıt sonuçlarının sağlamlığını değerlendirmede kritik bir aşamadır.

CertiK’in kamuya açık deposu, Coq ile yazılan biçimsel doğrulamanın zkWasm devresindeki yürütme tabloları, bellek tabloları, çağrı yığını ve bit işlemleri gibi temel bileşenleri kapsadığını belirtiyor. Amaç, tüm devre kısıtları karşılandığında yürütme izinin her satırının Wasm yürütme kurallarına uygun bir durumu temsil ettiğini kanıtlamak.

Doğrulama sürecinde devrenin bellek erişimi ile çağrı ve dönüş yapısında sorunlar tespit edilerek düzeltildiği de açıklandı. Bu durum, biçimsel doğrulamanın yalnızca mevcut kodu kontrol etmekle sınırlı kalmadığını, spesifikasyon ile uygulama arasındaki uyumsuzlukları da ortaya çıkarabildiğini gösteriyor.

Bununla birlikte bu çalışmayı 'zkWasm’ın tamamı tamamen doğrulandı' şeklinde yorumlamak doğru değil. Kamuya açık depoda Coq modeli, kanıt kodu ve derleme süreci yer alıyor ancak Rust ile yazılan algoritmanın tamamı doğrulama kapsamına alınmadı.

Şeffaflığın da sınırları bulunuyor. Depoda doğrulama kodunun yayımlanmış olmasına rağmen bazı devre bileşenleri, komut kodu çözümleme mantığı, Wasmi yorumlayıcısı ve Halo2’nin çalışma biçimi varsayıldı veya doğrulama kapsamı dışında bırakıldı.

Wasmi yorumlayıcısı, Halo2’nin kendisi ve bazı kısıt üretim kodları da doğrulama kapsamına alınmadı. Harici çağrı işlevleri ile bazı komut kodu çözümleme mantıkları ayrıca varsayımlara veya manuel incelemeye dayanıyor.

CertiK, ilgili dahili depoda toplam 33.080 satır Coq kodu bulunduğunu açıkladı. Kod hacminin kamuya açıklanması ile kanıt kapsamının tamamının kamuya açılması aynı anlama gelmiyor.

CertiK’in 2024 yıllık raporunda doğrulama kapsamındaki sistemin 144 komuttan oluşan zkWasm devresi olduğu ve bunun sıfır bilgi kanıtı ekosistemindeki ilk tam biçimsel doğrulama olarak değerlendirildiği belirtildi. Bu ifade CertiK’in kendi açıklamasına dayanıyor; bağımsız bir karşılaştırma ölçütü veya hakem değerlendirmesi sonucu doğrulanmış değil.

CertiK, söz konusu biçimsel doğrulama çerçevesinin diğer zkVM ve zkEVM sistemlerine de uygulanabileceğini belirtti. Ancak bu, diğer sistemlerde doğrulamanın tamamlandığı anlamına gelmiyor; yalnızca şirketin uygulanabilirliğe ilişkin açıklamasını yansıtıyor.

Delphinus Lab, kendi zkWasm uygulamasının biçimsel olarak doğrulandığını paylaşırken CertiK’in teknik dokümanına da bağlantı verdi. Geliştirici tarafındaki olumlu tepki doğrulanmış olsa da bu durum doğrulama kapsamının tüm yazılım yığınına genişlediği anlamına gelmiyor.

CertiK daha sonra Verus kullanarak geçmiş zkWasm kanıtlarının bir bölümünü yeniden uyguladığını ve kod hacmini 2.440 satırdan 595 satıra indirdiğini açıkladı. Bu çalışma, ilk doğrulama duyurusundan ayrı bir takip araştırması ve ilk doğrulamanın kamuya açık kapsamını genişleten bir sonuç olarak değerlendirilemez.

İlgili araştırma, ACM CCS 2026 programına 'Formal Verification of Circuit-Soundness in zkWasm, a General Purpose zkVM' başlıklı yayımlanması planlanan makale olarak kaydedildi. Makalede CertiK, Delphinus Lab, NVIDIA, Columbia University ve Yale University araştırmacıları yer alıyor. Makalenin tamamı ile hakemlik sürecinin ayrıntıları kamuya açık materyaller üzerinden doğrulanamıyor.

Bu örneğin temel önemi, zkVM altyapısında devre doğruluğunu matematiksel olarak açıklama çabasının somut bir araştırma sonucuna dönüşmesi. Bununla birlikte kamuya açıklanan doğrulama kapsamı ve yeniden üretilebilirlik, tüm yazılımın güvenliğiyle eş anlamlı kabul edilmemeli.