Jolt bytecode uzantılarının 67’sinden 60’ı doğrulandı

LayerZero Research’ün Jolt zkVM’deki 67 RISC-V bytecode uzantısından 60’ını doğruladığı bildirildi. Kalan 7 talimat, belirli uç durumlar nedeniyle doğrulama kapsamında bulunuyor.

CryptoBriefing, LayerZero Research’ün bu doğrulamayı yaklaşık iki buçuk ay boyunca Lean teorem ispatlayıcısını kullanarak yürüttüğünü bildirdi. Ancak söz konusu sayı ve doğrulama makalesi, LayerZero’nun resmi kanallarında aynı içerikle doğrulanmadı.

Biçimsel doğrulama, yazılımın belirli bir şartnameyi karşılayıp karşılamadığını testlerle değil, matematiksel kanıtlarla inceleme yöntemidir. zkVM’lerde talimatların yanlış yorumlanması veya yürütme sırasında hata oluşması, hatalı sonuçların geçerli bir kanıt olarak kabul edilmesine yol açabileceğinden bu aşama önem taşıyor.

Jolt’un bytecode uzantısı, ELF dosyasında yer alan ham RISC-V talimatlarını çözerek işlenenler, adresler, devre bayrakları ve arama bayraklarını içeren bir iç gösterime dönüştürüyor. Jolt’un resmi belgeleri, bytecode’u çalıştırılacak programın referans noktası olarak tanımlıyor.

Genişletilmiş bytecode dizini ile ELF bellek adresleri farklı işlevlere sahip. Bytecode dizini, yürütme döngüsünde talimatlara erişmek için kullanılırken ELF bellek adresi program sayacı kısıtlarını kontrol etmekte kullanılıyor.

Yürütme sırasında ayrıca okunan talimatın önceden işlenmiş bytecode ile eşleştiği de kanıtlanıyor. Bu nedenle bytecode uzantısı aşamasının doğruluğu, sonraki yürütme izlerinin ve kanıt sonuçlarının güvenilirliğini etkileyebilir.

Bu doğrulama, Jolt’un tamamı için biçimsel doğrulamanın sona erdiği anlamına gelmiyor. Andreessen Horowitz, 2024 tarihli teknik yazısında Jolt doğrulamasını; arama semantiği, polinom etkileşimli kanıt, kısıt sistemi, RISC-V şartnamesi ve gerçek Rust uygulaması arasındaki uyumun aşamalı olarak kontrol edildiği bir süreç olarak açıkladı.

Andreessen Horowitz’in doğrulama yol haritası, biçimsel model ile gerçek uygulama kodunun örtüşüp örtüşmediğinin kontrol edilmesini de ayrı bir görev olarak ortaya koyuyor. Başka bir deyişle, Lean’de biçimsel model kanıtlanmış olsa bile bu modelin gerçek uygulamayı doğru biçimde yansıtıp yansıtmadığı için ek doğrulama gerekiyor.

Önceki çalışmalarda Jolt’un RISC-V RV32I talimatlarının arama semantiği ACL2 teorem ispatlayıcısı kullanılarak doğrulandı. Araştırmacılar, talimatların küçük arama tablolarına ayrıştırılmasının RISC-V şartnamesiyle uyumlu olduğunu kontrol etti ve bazı talimatlarda gereksiz aramaları azaltan bir optimizasyon tespit etti.

İlgili çalışma, tüm RV32I talimatlarının ACL2 ile biçimsel hale getirildiğini ve doğrulandığını belirtti. Lean tabanlı mevcut çalışma, önceki doğrulama araştırmalarından farklı bir teorem ispatlayıcısı kullanarak bytecode uzantısının kapsamını inceleyen bir örnek olarak değerlendirilebilir.

LayerZero, Zero teknik belgesinde Jolt’u ağın yürütme kanıtı altyapısı olarak kullandığını açıkladı. Zero’nun yürütme mantığı kanıt oluşturma ve doğrulama süreçlerinden geçerken Jolt, program yürütme sonucunun doğru olduğunu kanıtlayan zkVM görevini üstleniyor.

Bununla birlikte yalnızca bytecode uzantısının doğrulanması, Zero ağının tamamının veya Jolt’un tümünün güvenliğinin doğrulandığı anlamına gelmiyor. Gerçek Rust uygulaması ile biçimsel model arasındaki uyum ve diğer kanıt bileşenlerinin doğrulama kapsamı ayrı başlıklar olarak varlığını sürdürüyor.

LayerZero ve Andreessen Horowitz tarafından yayımlanan Akita ve Lattice Jolt hakkındaki teknik duyuru, sıfır bilgi kanıtı altyapısının kriptografik bileşenlerini ele almıştı. Mevcut çalışma ise polinom taahhüt yöntemlerinden ziyade yürütme sürecindeki talimat yorumlama ve bytecode dönüşümüne odaklanmasıyla önceki duyurudan ayrılıyor.

Doğrulanan 60 talimatın ve doğrulanmayan 7 talimatın ayrıntılı listesi yayımlanmadı. Özellikle 7 talimatın hangi uç durumlara karşılık geldiği ve gerçek uygulama kodunun biçimsel modelle ne ölçüde örtüştüğü konusunda ek bilgilere ihtiyaç bulunuyor.

Bu duyuru, Jolt zkVM’nin belirli bir bileşeninde biçimsel doğrulama bakımından ilerleme olarak değerlendirilebilir. Ancak doğrulama kapsamı sınırlı olduğu için bunun tüm zkVM’nin veya Zero ağının güvenlik doğrulamasının tamamlandığı şeklinde yorumlanmaması gerekiyor.