zk-SNARKs'ın Biçimsel Doğrulaması: Bellek Kanıtı Yöntemi

Sıfır bilgi kanıtı sistemlerinin biçimsel doğrulamasını yaparken, bellek alt sistemi işlemi önemli bir zorluktur. Geleneksel sanal makinelerin aksine, zkVM bellek durumunu temsil etmek için yürütme tablosu ve yardımcı tablo kullanır, bu da özel doğrulama yöntemleri gerektirir.

zkWasm'ın bellek sistemi, yürütme tablosu ve bellek tablosundan oluşur. Yürütme tablosu, talimat yürütme sürecini kaydederken, bellek tablosu ise tüm bellek erişimlerinin tarihçesini saklar. Geliştirmeyi kolaylaştırmak için, zkWasm, bellekle etkileşimde bulunmak için alloc_memory_table_lookup_write_cell ve alloc_memory_table_lookup_read_cell adlı iki fonksiyon aracılığıyla bir soyut katman sağlar.

Doğrulama sürecinde, bellek tablosunu değişken bir veri yapısı olarak ele alıyoruz ve memory_at fonksiyonu aracılığıyla adres veri eşlemesi oluşturuyoruz. Bu, alloc fonksiyonunun ürettiği kısıtların eşlemede yapılan set ve get işlemleri ile eşdeğer olduğunu kanıtlamaya olanak tanır, böylece talimat doğrulamasını ZK benzeri bir yorumlayıcı biçimine basitleştirir.

Saldırganların bellek tablosunu manipüle etmesini önlemek için, zkWasm geçerli girişlerin sayısını izlemek için bir sayım mekanizması kullanır. Yürütme tablosu ve bellek tablosu, her biri kendi sayacını sürdürerek, ikisi arasında tutarlılığı sağlamak için kısıtlamalarla birlikte çalışır. Bu, doğrulama sırasında daha hassas olunmasını gerektirir ve her bir komutun doğru sayıda bellek tablosu girişiyle eşleştiğini kanıtlamayı gerektirir.

Doğrulama süreci üstten alta doğru bir yaklaşım kullanarak üç adım içerir:

1. Tahmin edilen komut tarafından oluşturulacak giriş sayısı
2. Kanıt tablosundaki giriş sayısı beklenenden fazla olmamalıdır.
3. cum_mops ve instructions_mops'un tabloda her zaman tutarlı olduğunu kanıtlamak için tümevarım yöntemiyle.

Bu ayrıntılı doğrulama yöntemi, atlama tablo sayım mekanizmasındaki önemli bir sorunu gibi potansiyel hataları bulmaya yardımcı olur.

Modüler doğrulama sağlamak için sistemi üç bağımsız parçaya ayırıyoruz: talimat devresi doğrulama, yürütme tablosu doğrulama ve bellek tablosu uygulaması. Bu yapı, birden fazla mühendisinin paralel çalışmasına olanak tanıyarak doğrulama verimliliğini artırır.

Genel olarak, zkVM doğrulaması dinamik durumları işlerken farklılıklar gösterse de, uygulamadaki soyutlama katmanları eşleştirilerek, geleneksel yorumlayıcı doğrulamalarına benzer modüler bir yaklaşım benimsenebilir. Bu yöntem, farklılıkların etkisini en aza indirerek, her bir komutun get-set arayüzüne dayanarak bağımsız bir şekilde doğrulanmasını sağlar.