Sıfır Bilgi Kanıtlarının Gelişmiş Resmi Doğrulaması: Sıfır Bilgi Belleği Nasıl Kanıtlanır

Blog serimizde sıfır bilgi kanıtlarının gelişmiş resmi doğrulaması , tartıştık ZK talimatları nasıl doğrulanır Ve iki ZK güvenlik açığına derinlemesine bir bakış Her zkWasm talimatını resmen doğrulayarak, her bir güvenlik açığını bulduk ve düzelttik, bu da tüm zkWasm devresinin teknik güvenliğini ve doğruluğunu tam olarak doğrulamamızı sağladı, gösterildiği gibi kamu raporu Ve kod deposu .

Bir zkWasm talimatını doğrulama sürecini göstermiş ve projenin ilk kavramlarını tanıtmış olsak da, resmi doğrulamaya aşina olan okuyucular, zkVM'nin doğrulamada diğer küçük ZK sistemlerine veya diğer bayt kodu VM'lerine kıyasla benzersizliğini anlamakla ilgilenebilirler. Bu makalede, zkWasm bellek alt sistemini doğrularken karşılaşılan bazı teknik noktaları derinlemesine ele alacağız. Bellek, zkVM'nin en benzersiz parçasıdır ve onu iyi yönetmek, diğer tüm zkVM'leri doğrulamak için kritik öneme sahiptir.

Resmi Doğrulama: Sanal Makine (VM) ve ZK Sanal Makinesi (zkVM)

Nihai hedefimiz, zkWasm'ın doğruluğunu, normal bir bayt kodu yorumlayıcısının (VM, Ethereum düğümleri tarafından kullanılan EVM yorumlayıcısı gibi) doğruluk teoremlerine benzer şekilde doğrulamaktır. Yani, yorumlayıcının her yürütme adımı, dilin operasyonel semantiğine dayalı yasal bir adıma karşılık gelir. Aşağıdaki şekilde gösterildiği gibi, bayt kodu yorumlayıcısının veri yapısının geçerli durumu SL ise ve bu durum Wasm makinesinin üst düzey spesifikasyonunda durum SH olarak işaretlenmişse, yorumlayıcı durum SL'ye geçtiğinde, karşılık gelen yasal bir üst düzey durum SH olmalıdır ve Wasm spesifikasyonu, SH'nin SH'ye geçmesi gerektiğini şart koşar.

Benzer şekilde, zkVM'nin de benzer bir doğruluk teoremi vardır: zkWasm yürütme tablosundaki her yeni satır, dilin operasyonel semantiğine dayalı yasal bir adıma karşılık gelir. Aşağıdaki şekilde gösterildiği gibi, yürütme tablosu veri yapısının bir satırının geçerli durumu SR ise ve bu durum Wasm makinesinin üst düzey spesifikasyonunda durum SH olarak temsil ediliyorsa, yürütme tablosu durumu SR'nin bir sonraki satırı üst düzey bir durum SH'ye karşılık gelmelidir ve Wasm spesifikasyonu SH'nin SH'ye adım atması gerektiğini şart koşar.

Yüksek seviyeli durum ve Wasm adımlarının özelliklerinin hem VM hem de zkVM'de tutarlı olduğu görülebilir, bu nedenle programlama dili yorumlayıcılarının veya derleyicilerinin önceki doğrulama deneyimleri referans olarak kullanılabilir. ZkVM doğrulamasının özelliği, sistemin düşük seviyeli durumunu oluşturan veri yapısının türünde yatmaktadır.

İlk olarak, daha önce açıkladığımız gibi önceki bir blog yazısı , zk kanıtlayıcıları esasen tam sayı aritmetiği modulo büyük asal sayılardır ve Wasm belirtimi ve normal yorumlayıcılar 32-bit veya 64-bit tam sayılarla ilgilenir. ZkVM uygulamasının çoğu bununla ilgilenir, bu nedenle doğrulamanın bunu da ele alması gerekir. Ancak bu yerel bir sorundur: her kod satırı aritmetik işlemleri ele alması gerektiğinden daha karmaşık hale gelir, ancak kodun ve kanıtın genel yapısı değişmez.

Bir diğer önemli fark, dinamik olarak boyutlandırılmış veri yapılarının nasıl işlendiğidir. Normal bir bayt kodu yorumlayıcısında, bellek, veri yığını ve çağrı yığını, hepsi değiştirilebilir veri yapıları olarak uygulanır. Benzer şekilde, Wasm belirtimi belleği get/set yöntemleriyle bir veri türü olarak temsil eder. Örneğin, Geths EVM yorumlayıcısı, fiziksel belleği temsil eden bir bayt dizisi olarak uygulanan ve `Set 32` ve `GetPtr` yöntemleri aracılığıyla yazılan ve okunan bir `Memory` veri türüne sahiptir. Bir hafıza depolama talimatı Geth, fiziksel belleği değiştirmek için `Set 32`yi çağırır.

func opMstore(pc *uint 64, yorumlayıcı *EVMInterpreter, kapsam *ScopeContext) ([]bayt, hata) {

// yığının pop değeri

mStart, val := kapsam.Yığın.pop(), kapsam.Yığın.pop()

kapsam.Bellek.Set 32(mStart.Uint 64(), val)

sıfır, sıfırı geri döndür

}

Yukarıdaki yorumlayıcının doğruluk ispatında, yorumlayıcıdaki somut belleğe ve spesifikasyondaki soyut belleğe değerler atandıktan sonra yüksek seviyeli durumun düşük seviyeli durumla eşleştiğini ispatlamak nispeten kolaydır.

Ancak zkVM ile işler biraz daha karmaşıklaşıyor.

zkWasms bellek tablosu ve bellek soyutlama katmanı

zkVM'de yürütme tablosu sabit boyutlu veriler için sütunlara sahiptir (bir CPU'daki kayıtlara benzer), ancak yardımcı tablolar aracılığıyla erişilen dinamik boyutlu veri yapılarını işleyemez. zkWasm yürütme tablosu 1, 2, 3 vb. değerlerine sahip bir EID sütununa ve sırasıyla bellek verilerini ve çağrı yığınını temsil eden iki yardımcı tabloya, bellek tablosuna ve atlama tablosuna sahiptir.

Aşağıda bir para çekme programının örnek bir uygulaması gösterilmektedir:

bakiye, miktar;

boş ana () {

bakiye = 100;

miktar = 10;

bakiye -= miktar; // çek

}

Yürütme tablosunun içerikleri ve yapısı oldukça basittir. 6 yürütme adımı vardır (EID'ler 1 ila 6), her biri işlem kodunu (opcode) ve talimat bir bellek okuma veya yazma ise adresini ve verilerini listeleyen bir satıra sahiptir:

Bellek tablosundaki her satır bir adres, veri, bir başlangıç EID'si ve bir bitiş EID'si içerir. Başlangıç EID'si, veriyi o adrese yazan yürütme adımının EID'sidir ve bitiş EID'si, o adrese yazacak bir sonraki yürütme adımının EID'sidir. (Ayrıca daha sonra ayrıntılı olarak tartışacağımız bir sayım da içerir.) Wasm bellek okuma talimatı devresi için, tabloda uygun bir tablo girişi olduğundan emin olmak için bir arama kısıtlaması kullanır, böylece okuma talimatının EID'si başlangıçtan bitişe kadar olan aralıkta olur. (Benzer şekilde, atlama tablosunun her satırı çağrı yığınının bir çerçevesine karşılık gelir ve her satır, onu oluşturan çağrı talimatı adımının EID'siyle etiketlenir.)

Bu bellek sistemi normal bir VM yorumlayıcısından çok farklıdır: bellek tablosu kademeli olarak güncellenen değiştirilebilir bir bellek değildir, ancak tüm yürütme izindeki tüm bellek erişimlerinin geçmişini içerir. Programcıların işini basitleştirmek için zkWasm iki kullanışlı giriş işlevi aracılığıyla uygulanan bir soyutlama katmanı sağlar. Bunlar şunlardır:

alloc_memory_table_lookup_write_cell

Ve

Alloc_memory_table_lookup_read_cell

Parametreleri şu şekildedir:

Örneğin, zkWasm'daki bellek depolama yönergesini uygulayan kod, write alloc fonksiyonuna bir çağrı içerir:

memory_table_lookup_heap_write1 = tahsis edici

.alloc_memory_table_lookup_write_cell_with_value(

mağaza yazma res 1,

kısıtlama_oluşturucusu,

bayram,

|____| constant_from!(LocationType::Heap'i u 64 olarak taşı),

taşı |meta| load_block_index.expr(meta), // adres

taşı |____| constant_from!(0), // 32-bit'tir

taşı |____| constant_from!( 1), // (her zaman) etkin

);

store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;

`alloc` fonksiyonu, tablolar arasındaki arama kısıtlamalarını ve geçerli `eid`'yi bellek tablosu girişiyle ilişkilendiren aritmetik kısıtlamaları işlemekten sorumludur. Bu nedenle, programcı bu tabloları normal bellek olarak ele alabilir ve kod yürütüldükten sonra `store_value_in_heap1` değeri `load_block_index` adresine atanmıştır.

Benzer şekilde, bellek okuma talimatları `read_alloc` fonksiyonu kullanılarak uygulanır. Yukarıdaki örnek yürütme dizisinde, her yükleme talimatının bir okuma kısıtlaması ve her depolama talimatının bir yazma kısıtlaması vardır ve her kısıtlama bellek tablosundaki bir girdi tarafından karşılanır.

mtable_lookup_write(satır 1.eid, satır 1.store_addr, satır 1.store_value)

⇐ (satır 1.eid= 1 ∧ satır 1.mağaza_adresi=bakiye ∧ satır 1.mağaza_değeri= 100 ∧ …)

mtable_lookup_write(satır 2.eid, satır 2.store_addr, satır 2.store_value)

⇐ (satır 2.eid= 2 ∧ satır 2.store_addr=miktar ∧ satır 2.store_value= 10 ∧ …)

mtable_lookup_read(satır 3.eid, satır 3.load_addr, satır 3.load_value)

⇐ ( 2

mtable_lookup_read(satır 4.eid, satır 4.load_addr, satır 4.load_value)

⇐ ( 1

mtable_lookup_write(satır 6.eid, satır 6.store_addr, satır 6.store_value)

⇐ (satır 6.eid= 6 ∧ satır 6.store_addr=bakiye ∧ satır 6.store_value= 90 ∧ …)

Resmi doğrulamanın yapısı, doğrulanan yazılımda kullanılan soyutlamalara karşılık gelmelidir, böylece kanıt kodla aynı mantığı izleyebilir. zkWasm için bu, bellek tablosu devresini ve alloc okuma/yazma hücre işlevini, değiştirilebilir bellek gibi bir arayüzle bir modül olarak doğrulamamız gerektiği anlamına gelir. Böyle bir arayüz verildiğinde, her bir talimat devresinin doğrulaması, ek ZK karmaşıklığının bellek alt sistemi modülünde kapsüllenmesiyle, normal bir yorumlayıcıya benzer şekilde yapılabilir.

Doğrulamada, bellek tablosunun aslında değiştirilebilir bir veri yapısı olarak kabul edilebileceği fikrini özellikle uyguladık. Yani, bellek tablosunu tamamen tarayan ve karşılık gelen adres veri eşlemesini oluşturan `memory_at type` adlı bir fonksiyon yazdık. (Burada, `type` değişkeninin değer aralığı üç farklı Wasm bellek verisi türüdür: yığın, veri yığını ve genel değişkenler.) Daha sonra, alloc fonksiyonu tarafından oluşturulan bellek kısıtlamalarının, set ve get fonksiyonlarını kullanarak karşılık gelen adres veri eşlemesine yapılan veri değişikliklerine eşdeğer olduğunu kanıtladık. Şunu kanıtlayabiliriz:

• Her bayram için aşağıdaki kısıtlamalar geçerliyse

memory_table_lookup_read_cell eid türü ofset değeri

Ancak

get (memory_at eid türü) ofset = Bir değer

• Ve eğer aşağıdaki kısıtlamalar geçerliyse

memory_table_lookup_write_cell eid türü ofset değeri

Ancak

memory_at (eid+ 1) type = set (memory_at eid type) ofset değeri

Bundan sonra her bir talimatın doğrulanması, ZK olmayan bir bayt kodu yorumlayıcısına benzer şekilde adres-veri eşlemesindeki get ve set işlemlerine dayalı olarak yapılabilir.

zkWasms bellek yazma sayma mekanizması

Ancak, yukarıdaki basitleştirilmiş açıklama bellek tablosunun ve atlama tablosunun tam içeriğini ortaya koymaz. zkVM çerçevesi altında, bu tablolar bir saldırgan tarafından manipüle edilebilir ve bu saldırgan, bir veri satırı ekleyerek keyfi bir değer döndürmek için bellek yükleme talimatını kolayca manipüle edebilir.

Örnek olarak para çekme programını ele alırsak, bir saldırgan para çekme işleminden önce $110'luk bir bellek yazma işlemi düzenleyerek hesap bakiyesine yanlış veri enjekte etme fırsatına sahiptir. Bu işlem, bellek tablosuna bir veri satırı eklenerek ve bellek tablosunda ve yürütme tablosunda var olan hücrelerin değerleri değiştirilerek gerçekleştirilebilir. Bu, ücretsiz bir para çekme işlemiyle sonuçlanacaktır çünkü hesap bakiyesi işlemden sonra bile $100'de kalacaktır.

Bellek tablosunun (ve atlama tablosunun) yalnızca gerçekte yürütülen bellek yazmaları (ve çağrılar ve dönüşler) tarafından oluşturulan geçerli girdileri içerdiğinden emin olmak için zkWasm, girdi sayısını izlemek için özel bir sayma mekanizması kullanır. Özellikle, bellek tablosunda toplam bellek yazma girdisi sayısını izleyen özel bir sütun bulunur. Aynı zamanda, yürütme tablosu her talimat için beklenen bellek yazma işlemlerinin sayısını sayan bir sayaç da içerir. İki sayımın tutarlı olmasını sağlamak için bir eşitlik kısıtlaması ayarlanır. Bu yaklaşımın mantığı çok sezgiseldir: her bellek yazma işlemi gerçekleştirildiğinde, bir kez sayılır ve bellek tablosunda buna karşılık gelen bir kayıt olmalıdır. Bu nedenle, bir saldırgan bellek tablosuna herhangi bir ek girdi ekleyemez.

Yukarıdaki mantıksal ifade biraz belirsizdir ve mekanik kanıt sürecinde bunu daha kesin hale getirmemiz gerekir. Öncelikle, yukarıda belirtilen bellek yazma lemmasının ifadesini düzeltmemiz gerekir. Belirli bir `eid` ve `type` ile bellek tablosu girişlerinin sayısını sayan bir `mops_at eid type` fonksiyonu tanımlarız (çoğu talimat bir eid'de 0 veya 1 giriş oluşturacaktır). Teoremin tam ifadesi, sahte bellek tablosu girişi olmadığını belirten ek bir ön koşula sahiptir:

Aşağıdaki kısıtlamalar geçerliyse

(memory_table_lookup_write_cell eid türü ofset değeri)

Ve aşağıdaki yeni kısıtlamalar geçerlidir

(mops_at bayram türü) = 1

Ancak

(memory_at(eid+ 1) türü) = (memory_at eid türü) ofset değerini ayarla

Bu, doğrulamamızın önceki durumdan daha kesin olmasını gerektirir. Eşitlik kısıtlamasından, toplam bellek tablosu girişi sayısının yürütmedeki toplam bellek yazma sayısına eşit olduğu sonucuna varmak yeterli değildir. Talimatların doğruluğunu kanıtlamak için, her talimatın doğru sayıda bellek tablosu girişine karşılık geldiğini bilmemiz gerekir. Örneğin, bir saldırganın yürütme dizisindeki bir talimat için bellek tablosu girişini atlayıp başka bir ilgisiz talimat için kötü amaçlı yeni bir bellek tablosu girişi oluşturma olasılığını ortadan kaldırmamız gerekir.

Bunu kanıtlamak için, belirli bir talimat için memtable girişlerinin sayısını kısıtlamak için üç adımdan oluşan yukarıdan aşağıya bir yaklaşım benimsiyoruz. İlk olarak, talimat türüne göre yürütme dizisindeki talimatlar için oluşturulması gereken giriş sayısını tahmin ediyoruz. i'inci adımdan yürütmenin sonuna kadar beklenen yazma sayısına `instructions_mops i` ve i'inci talimattan yürütmenin sonuna kadar karşılık gelen memtable giriş sayısına `cum_mops (eid i)` diyoruz. Her talimat için arama kısıtlamalarını analiz ederek, beklenenden daha az giriş oluşturmadığını ve dolayısıyla izlenen her segmentin [i… numRows] beklenenden daha az giriş oluşturmadığını kanıtlayabiliriz:

Lemma cum_mops_bound: her şey için,

0 ≤ ben ->

i + Z.of_nat n = etable_numRow ->

MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ instructions_mops i n.

İkincisi, eğer tablonun beklenenden daha fazla girdisi olmadığı gösterilebilirse, o zaman tam olarak doğru sayıda girdisi vardır ve bu açıktır.

Lemma cum_mops_equal : her durumda,

0 ≤ ben ->

i + Z.of_nat n = etable_numRow ->

MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≤ instructions_mops içinde ->

MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) = instructions_mops i n.

Şimdi 3. adıma geçelim. Doğruluk teoremimiz, herhangi bir n için cum_mops ve instructions_mops'un tablonun n satırından sonuna kadar olan kısmında her zaman aynı fikirde olduğunu belirtir:

Lemma cum_mops_equal : tüm n için,

0

MTable.cum_mops (etable_values eid_cell (n_nat_Z.)) (max_eid+ 1) = instructions_mops (n_nat_Z.)

Doğrulama n üzerinde tümevarımla yapılır. Tablodaki ilk satır, bellek tablosundaki toplam giriş sayısının doğru olduğunu belirten zkWasm için eşitlik kısıtlamasıdır, yani cum_mops 0 = instructions_mops 0. Aşağıdaki satırlar için tümevarım hipotezi bize şunu söyler:

cum_mops n = instructions_mops n

Ve kanıtlamayı umuyoruz

cum_mops (n+ 1) = instructions_mops (n+ 1)

Burada not alın

cum_mops n = mop_at n + cum_mops (n + 1)

Ve

talimatlar_mops n = talimat_mops n + talimatlar_mops (n + 1)

Bu nedenle, şunu elde edebiliriz:

mops_at n + cum_mops (n + 1) = talimat_mops n + talimatlar_mops (n + 1)

Daha önce, her talimatın beklenenden az giriş oluşturmayacağını gösterdik, örneğin

mops_at n ≥ instructions_mops n.

Yani şu sonuca varılabilir

cum_mops (n+ 1) ≤ instructions_mops (n+ 1)

Burada yukarıda bahsi geçen ikinci önermeyi uygulamamız gerekiyor.

(Benzer bir lemma, her çağrı talimatının tam olarak bir atlama tablosu girişi ürettiğini kanıtlamak için atlama tablolarına uygulanabilir ve bu da kanıt tekniğini genel olarak uygulanabilir hale getirir. Ancak, dönüş talimatlarının doğruluğunu kanıtlamak için daha fazla çalışmaya ihtiyaç vardır. Dönüş eid'si, çağrı çerçevesini oluşturan çağrı talimatının eid'sinden farklıdır, bu nedenle bir ek değişmez (yürütme sırasında eid değerinin tek yönlü olarak arttığını belirtir.)

Kanıtın bu kadar ayrıntılı açıklaması, resmi doğrulamanın tipik bir örneğidir ve belirli bir kod parçasını doğrulamanın genellikle onu yazmaktan daha uzun sürmesinin nedenidir. Ama buna değer mi? Bu durumda değer, çünkü kanıt sırasında atlama tablosu sayma mekanizmasında kritik bir hata keşfettik. Bu hata ayrıntılı olarak şurada açıklanmıştır: önceki bir gönderi – Özetle, kodun eski sürümü hem çağrı hem de dönüş talimatlarını sayıyordu ve bir saldırgan yürütme dizisine fazladan bir dönüş talimatı ekleyerek sahte bir atlama tablosu girişi için yer açabilirdi. Yanlış sayma mekanizması her çağrı ve dönüş talimatını sayma sezgisini tatmin etse de, bu sezgiyi daha kesin bir teorem ifadesine dönüştürmeye çalıştığımızda sorunlar belirginleşiyor.

Kanıt sürecini modüler hale getirin

Yukarıdaki tartışmadan, her talimat devresi hakkındaki kanıt ile yürütme tablosunun sayım sütunu hakkındaki kanıt arasında dairesel bir bağımlılık olduğunu görebiliriz. Talimat devresinin doğruluğunu kanıtlamak için, içindeki bellek yazmaları hakkında akıl yürütmemiz gerekir; yani, belirli bir EID'deki bellek tablosu girişlerinin sayısını bilmemiz ve yürütme tablosundaki bellek yazma işlemi sayısının doğru olduğunu kanıtlamamız gerekir; bu da sırayla her talimatın en azından minimum sayıda bellek yazma işlemi gerçekleştirdiğini kanıtlamayı gerektirir.

Ek olarak, dikkate alınması gereken başka bir faktör daha var. zkWasm projesi oldukça büyük, bu yüzden doğrulama işinin modülerleştirilmesi gerekiyor, böylece birden fazla doğrulama mühendisi işi bölebilir. Bu nedenle, sayma mekanizmasının kanıtını parçalara ayırırken, karmaşıklığına özel dikkat gösterilmesi gerekir. Örneğin, LocalGet talimatı için aşağıdaki gibi iki teorem vardır:

Teorem opcode_mops_correct_local_get : tüm i için,

0

etable_values eid_hücresi i > 0 ->

opcode_mops_correct LocalGet i.

Teorem LocalGetOp_correct : tüm i st y xs için,

0

etable_values etkin_hücre i = 1 ->

paspaslar_doğru_i ->

etable_values (ops_cell LocalGet) i = 1 ->

durum_il i st ->

wasm_stack st = xs ->

(etable_values offset_cell i) > 1 ->

nth_error xs (Z.to_nat (etable_values offset_cell i – 1)) = Bazı y ->

state_rel (i+ 1) (update_stack (incr_iid st) (y::xs)).

Birinci teorem ifadesi

opcode_mops_correct LocalGet i

Tanım genişletildikten sonra, bu, talimatın i. satırda en az bir memtable girişi oluşturduğu anlamına gelir (1 sayısı zkWasm'ın LocalGet opcode spesifikasyonunda belirtilmiştir).

İkinci teorem, bu talimat için tam doğruluk teoremidir ve şunu belirtir:

paspaslar_doğru_ben

Bir hipotez olarak bu, talimatın tam olarak bir bellek tablosu girişi oluşturduğu anlamına gelir.

Doğrulama mühendisleri bu iki teoremi bağımsız olarak kanıtlayabilir ve daha sonra bunları yürütme tablosuyla ilgili kanıtla birleştirerek tüm sistemin doğruluğunu kanıtlayabilirler. Bireysel talimatlar için tüm kanıtların, bellek tablosunun belirli uygulamasını bilmeden okuma/yazma kısıtlamaları düzeyinde yapılabileceğini belirtmekte fayda var. Bu nedenle, proje bağımsız olarak işlenebilen üç bölüme ayrılmıştır.

Özetle

ZkVM devrelerini satır satır doğrulamak, diğer ZK uygulamalarını doğrulamaktan temelde farklı değildir, çünkü hepsi aritmetik kısıtlamalar hakkında benzer akıl yürütme gerektirir. Yüksek düzeyde, zkVM doğrulaması, programlama dili yorumlayıcılarının ve derleyicilerinin resmi doğrulamasında kullanılan tekniklerin çoğunu gerektirir. Buradaki temel fark, dinamik olarak boyutlandırılmış sanal makine durumudur. Ancak, bu farklılıkların etkisi, doğrulama yapısının uygulamada kullanılan soyutlama düzeyine uyacak şekilde dikkatlice oluşturulmasıyla en aza indirilebilir, böylece her talimat, tıpkı normal bir yorumlayıcıda olduğu gibi, bir get-set arayüzüne dayalı olarak bağımsız olarak modüler olarak doğrulanabilir.

Bu makale internetten alınmıştır: Sıfır Bilgi Kanıtlarının Gelişmiş Resmi Doğrulaması: Sıfır Bilgi Belleği Nasıl Kanıtlanır