Vitalik: Ethereum'un bir sonraki aşamasının anahtarı nedir?

Yazar: Vitalik Buterin

Çeviren: Jiahua, ChainCatcher

Geri bildirimleri ve değerlendirmeleri için Yoichi Hirai, Justin Drake, Nadim Kobeissi ve Alex Hicks'e özel teşekkürler.

Son birkaç ayda, Ethereum geliştirme çevrelerinde ve bilişimin birçok diğer alanında yeni bir programlama paradigması hızla rağbet görmeye başladı: kodu doğrudan çok düşük seviyeli dillerde (EVM bayt kodu, assembly dili gibi) veya Lean'de yazmak ve doğruluğunu doğrulamak için Lean'de yazılmış otomatik olarak doğrulanabilir matematiksel kanıtlar kullanmak.

Doğru yapıldığında, bu yöntem yalnızca son derece verimli kod üretme potansiyeline sahip olmakla kalmaz, aynı zamanda önceki programlama yöntemlerine göre çok daha güvenlidir. Yoichi Hirai buna "yazılım geliştirmenin nihai biçimi" diyor.

Bu makale, temel prensipleri ortaya çıkarmayı, yazılımın biçimsel doğrulanmasının neler başarabileceğini araştırmayı ve Ethereum ve diğer alanlardaki zayıf yönlerini ve sınırlamalarını belirlemeyi amaçlamaktadır.

Biçimsel Doğrulama Nedir?

Biçimsel doğrulama, matematiksel teoremlerin kanıtlarını otomatik olarak kontrol edilebilecek şekilde yazma sürecini ifade eder. Nispeten basit ama ilginç bir örnek vermek gerekirse, Fibonacci dizisiyle ilgili temel bir teoremi ele alalım: her üçüncü sayı çift, diğerleri ise tektir.

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

Bunu kanıtlamanın basit bir yolu, matematiksel indüksiyon yöntemiyle, her seferinde üç adım ilerleyerek yapılabilir.

İlk olarak temel durumu ele alalım. F1 = F2 = 1, F3 = 2 olsun. Gözlem yoluyla, ("i, 3'ün katı olduğunda F1 çifttir, aksi halde tektir") ifadesinin x = 3'ten önce doğru olduğunu görüyoruz.

Sırada tümevarımsal durum var. İfadenin 3k+3'ten önce doğru olduğunu varsayalım, yani F3k+1, F3k+2 ve F3k+3'ün sırasıyla tek, tek ve çift olduğunu zaten biliyoruz. Sonraki üç sayı grubunun çiftliğini hesaplayabiliriz:

F3k+4 = F3k+2 + F3k+3 = tek + çift = tek

F3k+5 = F3k+3 + F3k+4 = çift + tek = tek

F3k+6 = F3k+4 + F3k+5 = tek + tek = çift

Dolayısıyla, ifadenin 3k+3'ten önce doğru olduğunu bildiğimizden, ifadenin 3k+6'dan önce de doğru olduğunu çıkarabiliriz. Bu akıl yürütmeyi tekrar tekrar uygulayarak, bu kuralın tüm tamsayılar için geçerli olduğundan emin olabiliriz.

Bu argüman insanları ikna etmek için yeterlidir. Ancak, yüz kat daha karmaşık bir şeyi kanıtlamak ve kesinlikle hata yapmadığınızdan emin olmak istiyorsanız ne yapmalısınız? İşte o zaman bir bilgisayarın da ikna olabileceği bir kanıt sunabilirsiniz.

Sunum şekli şöyledir:

-- Fibonacci dizisi, fib 0 = 0, fib 1 = 1, fib 2 = 1 (indeksler 1'er kaydırılmış)

def fib : Nat → Nat

| 0 => 0

| 1 => 1

| n + 2 => fib (n + 1) + fib n

-- İddia: fib (3k+1) tek sayıdır, fib (3k+2) tek sayıdır, fib (3k+3) çift sayıdır.

-- Eşdeğer olarak: Fibonacci 3'ten başlayarak her üçüncü Fibonacci sayısı çifttir.

-- Her üçünü de k üzerinden tümevarım yöntemiyle aynı anda kanıtlıyoruz, çünkü her durum

-- Bir sonraki blok, bir önceki bloktan oluşturulur.

teorem fib_triple (k : Nat) :

fib (3 * k + 1) % 2 = 1 ∧

fib (3 * k + 2) % 2 = 1 ∧

fib (3 * k + 3) % 2 = 0 := by

indüksiyon k ile

| sıfır => karar ver

| succ k ih =>

-- Yeni indeksleri (bir şey) + 2 şeklinde yeniden yazın ki Fibonacci açılımı gerçekleşsin.

rafine et ⟨?_, ?_, ?_⟩

· (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1'i göster

omega

· (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1'i göster

omega

· (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3) göster

+ (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0

omega

Bu, aynı mantık yürütme biçimidir, ancak Lean dilinde ifade edilmiştir. Lean, matematiksel ispatların yazılması ve doğrulanmasında yaygın olarak kullanılan bir programlama dilidir.

Bu, yukarıda verilen "insan" kanıtından farklı görünüyor ve bunun geçerli bir sebebi var: Bir bilgisayar için (geleneksel anlamda "bilgisayar", yani büyük dil modelleri yerine if/then ifadelerinden oluşan "deterministik" bir program) sezgisel olan şey, insanlar için sezgisel olan şeyden temelde farklıdır.

Yukarıdaki ispatta, fib(3k+4) = fib(3k+3) + fib(3k+2) gerçeğini vurgulamak yerine, fib(3k+3) + fib(3k+2)'nin tek sayı olduğunu vurguladınız; oysa Lean'deki omega adı verilen bir strateji bunu fib(3k+4)'ün tanımına dair bilgisiyle otomatik olarak birleştirir.

Daha karmaşık ispatlarda, bazen hangi matematiksel yasanın mevcut adımı atmanıza olanak sağladığını açıkça belirtmeniz gerekir ve bazen de Prod.mk.inj gibi anlaşılması güç isimler kullanmanız gerekebilir.

Öte yandan, devasa polinom ifadelerini tek bir adımda açabilir ve geçerliliklerini "omega" veya "halka" gibi tek satırlık bir ifadeyle kanıtlayabilirsiniz.

Bu sezgisel olmayan ve zahmetli yapı, makine tarafından doğrulanabilir kanıtların neredeyse 60 yıldır var olmasına rağmen, alanın neden niş bir alan olarak kaldığını büyük ölçüde açıklıyor. Bununla birlikte, diğer yandan, yapay zekanın hızlı gelişimi sayesinde, daha önce imkansız olan birçok şey artık hızla mümkün hale geliyor.

Matematiksel Kanıtlar Kodu Korumaya Başladığında

Şimdiye kadar şöyle düşünüyor olabilirsiniz: Bilgisayarlar matematiksel teoremlerin ispatlarını doğrulayabiliyor, bu yüzden asal sayılarla ilgili hangi çılgın yeni sonuçların doğru olduğunu ve hangilerinin yüzlerce sayfalık PDF makalelerindeki hatalar olduğunu nihayet belirleyebiliriz.

Belki Shinichi Mochizuki'nin ABC varsayımı hakkındaki görüşlerinin doğru olup olmadığını bile anlayabiliriz!

Ama merakı bir kenara bırakırsak, ne olmuş yani?

Pek çok olası cevap var. Ancak benim için çok önemli olan bir cevap, özellikle kriptografik veya güvenlik ile ilgili görevleri yerine getiren bilgisayar programlarının doğruluğunu doğrulamaktır.

Sonuçta, bilgisayar programları matematiksel nesnelerdir; dolayısıyla bir bilgisayar programının belirli bir şekilde çalıştığını kanıtlamak da başlı başına bir matematiksel teoremdir.

Örneğin, Signal gibi şifreli bir iletişim yazılımının gerçekten güvenli olup olmadığını kanıtlamak istediğinizi varsayalım. Bu bağlamda "güvenli" kelimesinin matematiksel olarak ne anlama geldiğini yazabilirsiniz.

Genel olarak, belirli kriptografik varsayımların geçerli olduğunu kabul edersek, mesajın içeriği hakkında herhangi bir bilgiye yalnızca özel anahtara sahip olanların sahip olabileceğini kanıtlıyorsunuz. Gerçekte ise, çok sayıda farklı ve kritik güvenlik özelliği bulunmaktadır.

Meğerse tam da bu sorunu çözmeye çalışan bir ekip varmış! Güvenlik teoremlerinden biri şöyle:

teorem pasif_gizlilik_le_ddh

(g : G)

(adv : PassiveAdversary G SK) :

passiveSecrecyAdvantage (F := F) g adv ≤

ProbComp.boolDistAdvantage

(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))

(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

İşte Leanstral'dan anlamının özeti:

Passivesecrecyle_ddh teoremi, X3DH'nin pasif mesaj gizliliğinin, rastgele oracle modelindeki DDH varsayımı kadar zor olduğunu gösteren kompakt bir indirgemedir. Eğer bir düşman X3DH'nin pasif mesaj gizliliğini kırabilirse, DDH'yi de kırabilir.

DDH'nin kırılmasının zor olduğunu varsaydığımızdan, X3DH pasif saldırılara karşı da güvenlidir. Bu teorem, bir düşmanın Signal'in anahtar değişim mesajlarını pasif olarak gözlemleyebilmesi durumunda, ürettiği oturum anahtarını rastgele bir anahtardan ihmal edilebilir olasılıktan daha iyi bir olasılıkla ayırt edemeyeceğini kanıtlar.

Bunu AES şifrelemesinin doğru bir şekilde uygulandığına dair bir kanıtla birleştirirseniz, Signal protokolünün şifrelemesinin pasif saldırganlara karşı güvenli olduğuna dair bir kanıt elde edersiniz.

Benzer projeler, TLS ve tarayıcı içi şifrelemenin diğer unsurlarının uygulamalarının güvenli olduğunu da kanıtlamıştır.

Uçtan uca eksiksiz biçimsel doğrulama gerçekleştirirseniz, yalnızca protokolün teorik bir tanımının güvenli olduğunu değil, aynı zamanda kullanıcılar tarafından çalıştırılan belirli kodun da pratikte güvenli olduğunu kanıtlamış olursunuz.

Kullanıcı açısından bakıldığında, bu güvenilmezliği büyük ölçüde artırır: koda tamamen güvenmek için tüm kod tabanını kontrol etmenize gerek yoktur; yalnızca kod hakkında kanıtlanmış ifadeleri kontrol etmeniz yeterlidir.

Şimdi, özellikle son derece önemli olan "güvenli" kelimesinin gerçek anlamıyla ilgili olarak akılda tutulması gereken bazı önemli uyarılar var.

Gerçekten önemli olan ifadeleri kanıtlamayı unutmak kolaydır. Bazen kanıtlanması gereken ifadelerin, kodun kendisinden daha basit bir şekilde açıklanamadığını görmek de kolaydır.

İspat sürecine istemeden de olsa geçerli olmayan varsayımlar eklemek kolaydır. Ayrıca, sistemin yalnızca bir bölümünün gerçekten resmi olarak kanıtlanması gerektiğine karar vermek de kolaydır; bu durumda sistemin diğer bölümlerinde (hatta donanımda bile) ciddi güvenlik açıklarıyla karşılaşılabilir.

Lean uygulamasının kendisinde bile hatalar olabilir. Ancak tüm bu can sıkıcı ayrıntıları tartışmadan önce, biçimsel doğrulamayı doğru ve ideal bir şekilde tamamlamanın doğurabileceği ütopyaya bir göz atalım.

Güvenlik İçin Tasarlanmış Biçimsel Doğrulama

Bilgisayar kodlarındaki hatalar korkunçtur.

Kripto para birimlerini değiştirilemez zincirleme akıllı sözleşmelere koyduğunuzda ve Kuzey Kore, kodda bir hata ortaya çıktığında tüm fonlarınızı otomatik olarak çekebildiğinde ve sizin hiçbir çareniz olmadığında, kod hataları daha da korkutucu hale gelir.

Tüm bunlar sıfır bilgi ispatlarıyla sarmalandığında, hatalar daha da korkunç hale gelir çünkü birisi sıfır bilgi ispat sistemine sızmayı başarırsa, tüm parayı çekebilir ve biz neyin yanlış gittiğini bilemeyiz (daha da kötüsü, ne zaman yanlış gittiğini bile bilemeyiz).

İki yıl sonra Claude Mythos gibi bu hataları otomatik olarak keşfedebilen güçlü yapay zeka modellerine sahip olduğumuzda, kodlardaki hatalar daha da korkutucu hale gelecek.

Bazı insanların bu gerçeğe tepkisi, akıllı sözleşmelerin temel fikrinden vazgeçmeyi savunmak, hatta internetin, savunucuların saldırganlara karşı asimetrik bir avantaja sahip olabileceği bir alan olamayacağına inanmaktır.

İşte bazı alıntılar:

Bir sistemi güçlendirmek için, saldırganın güvenlik açıklarından yararlanmak için kullandığı token sayısından daha fazla token harcamanız gerekir.

Ve:

Sektörümüz, belirleyici kod üzerine kuruludur. Yazmak, test etmek, dağıtmak, çalıştığından emin olmak... Ancak benim deneyimime göre, bu sözleşme bozuluyor.

Gerçekten yapay zekâ odaklı şirketlerin önde gelen yöneticileri arasında, kod tabanı artık "güvenebileceğiniz" bir şey haline geldi ve başarı olasılığını kesin olarak belirleyemezsiniz.

Daha da kötüsü, bazı insanlar tek çözümün açık kaynak yazılımı terk etmek olduğuna inanıyor.

Siber güvenlik açısından bu, kasvetli bir gelecek olurdu. Özellikle internetin merkeziyetsizleşmesine ve özgürlüğüne önem veren bizler için bu son derece karamsar bir bakış açısı.

Siberpunk ruhunun tamamı, internette savunmacıların avantajlı olduğu ve dijital bir "kale" inşa etmenin (şifreleme, imza veya ispat yoluyla olsun) onu yok etmekten çok daha kolay olduğu fikrine dayanmaktadır.

Eğer bunu kaybedersek, internet güvenliği ancak ölçek ekonomilerinden, dünya çapında potansiyel saldırganları avlamaktan sağlanabilir ve daha geniş anlamda, ancak egemenlik ve yıkım arasında bir seçim olabilir.

Katılmıyorum; siber güvenliğin geleceği konusunda daha iyimser bir vizyonum var.

Güçlü yapay zekâ destekli güvenlik açığı tespit yeteneklerinin yarattığı zorlukların ciddi olduğuna inanıyorum, ancak bunlar geçici bir zorluk. Ortam sakinleşip yeni bir dengeye ulaştığımızda, geçmişe kıyasla savunmacılar için daha elverişli bir ortam oluşacak.

Mozilla da benim görüşüme katılıyor. Onların sözlerini aktaracak olursam:

Diğer her şeyin önceliğini yeniden ayarlamanız ve bu göreve sürekli ve odaklanmış bir enerji ayırmanız gerekebilir, ancak tünelin sonunda ışık var.

Ekibimizin bu zorluğun üstesinden gelme biçiminden çok gurur duyuyoruz ve diğerleri de duyacaktır. İşimiz henüz bitmedi, ancak fırtınayı atlattık ve sadece mevcut durumu korumakla kalmayıp çok daha iyi bir geleceğin ipuçlarını görebiliyoruz.

Savunmacılar nihayet kesin bir zafer kazanma fırsatına sahipler. … Kusurlar sınırlı ve nihayet hepsini bulabileceğimiz bir dünyaya giriyoruz.

Şimdi, Mozilla'nın gönderisinde Ctrl+F kullanarak "resmi" ve "doğrulama" kelimelerini ararsanız, hiçbir sonuç bulamazsınız. Siber güvenliğin olumlu geleceği tamamen resmi doğrulamaya veya başka herhangi bir tek teknolojiye bağlı değildir.

Neye bağlı? Esasen şu tabloya:

Zaman içinde CVE güvenlik açıklarının eğilimi

On yıllardır birçok teknoloji, güvenlik açıklarının sayısındaki azalmaya katkıda bulunmuştur:

Tip sistemleri

Hafızaya güvenli diller

Yazılım mimarisindeki iyileştirmeler (kum havuzu oluşturma, izin kontrolü ve daha genel olarak "güvenilir bilgi işlem tabanı"nı "diğer kodlardan" ayırma dahil)

Daha iyi test yöntemleri

Güvenli ve güvensiz kodlama kalıpları hakkında sürekli genişleyen bir bilgi tabanı.

Giderek artan sayıda önceden yazılmış ve denetlenmiş yazılım kütüphanesi

Yapay zekâ destekli biçimsel doğrulama, yepyeni bir paradigma olarak değil, halihazırda ilerlemekte olan eğilimlerin ve paradigmaların güçlü bir hızlandırıcısı olarak görülmelidir.

Biçimsel doğrulama her derde deva değildir. Ancak, hedefin uygulamadan çok daha basit olduğu durumlar için özellikle uygundur. Bu, Ethereum'un bir sonraki büyük sürümünde kullanmamız gerekecek son derece karmaşık ve zorlu bazı teknolojiler için özellikle geçerlidir: kuantum dirençli imzalar, STARK'lar, konsensüs algoritmaları ve ZK-EVM'ler.

STARK çok karmaşık bir yazılımdır. Ancak uyguladığı temel güvenlik özellikleri anlaşılması ve formüle edilmesi kolaydır: eğer bir H karma değerinin P programına, x girdisine ve y çıktısına işaret ettiğini görürseniz, o zaman ya (i) STARK'ta kullanılan karma algoritması kırılmıştır ya da (ii) P(x) = y'dir.

Dolayısıyla, tamamen biçimsel olarak doğrulanmış bir STARK uygulaması oluşturmaya çalışan Arklib projesine sahibiz (VCV-io'ya bakın; bu, STARK'ın bağımlılıkları olan birçok diğer kriptografik protokole biçimsel doğrulama için temel oracle hesaplama altyapısını sağlar).

Daha iddialı bir yaklaşım olarak, tamamen biçimsel olarak doğrulanmış eksiksiz bir EVM uygulamasını oluşturmayı amaçlayan evm-asm projesi bulunmaktadır.

Buradaki güvenlik özellikleri o kadar basit değil: Temelde amaç, sezgiselliği ve okunabilirliği en üst düzeye çıkarmak için belirli çalışma zamanı verimliliğini dikkate almadan yazılabilecek başka bir Lean ile yazılmış EVM uygulamasına eşdeğerliğini kanıtlamaktır.

Muhtemelen, hepsi kanıtlanabilir şekilde birbirine eşdeğer olan on adet EVM uygulaması elde edeceğiz ve bunların hepsinde, bir saldırganın erişim yetkisi olmayan adreslerden tüm ETH'yi çekmesine olanak tanıyan aynı ölümcül güvenlik açığı bulunacak.

Ancak bu, mevcut bazı EVM uygulamalarında bu tür kusurların bulunma olasılığından çok daha düşüktür. Acı verici derslerden sonra önemini fark ettiğimiz bir diğer güvenlik özelliği olan DoS saldırılarına karşı direnç de kolayca formüle edilebilir.

Diğer iki önemli alan ise şunlardır:

Bizans hata toleranslı konsensüsü. Burada, beklenen tüm güvenlik özelliklerini resmileştirmek de aynı derecede zordur, ancak hataların ne kadar yaygın olduğu göz önüne alındığında, denemeye değer. Bu nedenle, Lean'de devam eden uygulamalar ve konsensüs protokollerinin ispatları mevcuttur.

Akıllı sözleşme programlama dilleri: Vyper ve Verity'deki biçimsel doğrulama örneklerine bakın.

Tüm bu durumlarda, biçimsel doğrulamanın sağladığı en büyük katma değerlerden biri, bu kanıtların gerçekten uçtan uca olmasıdır. Tipik olarak, en can sıkıcı hatalar, bağımsız olarak ele alınan iki alt sistemin arayüzünde gizlenen etkileşim hatalarıdır.

İnsanlar için tüm sistemi baştan sona anlamak çok zordur. Ancak otomatik kural kontrol sistemleri bunu yapabilir.

Biçimsel Doğrulama, Verimlilik İçin Doğmuştur

Evm-asm'ye bir kez daha bakalım. Bu bir EVM uygulamasıdır. Ancak doğrudan RISC-V assembly dilinde yazılmış bir EVM uygulamasıdır.

Eşsiz.

İşte ADD işlem kodu:

EvmAsm.Rv64.Program'ı içe aktarın.

ad alanı EvmAsm.Evm64

EvmAsm.Rv64 dosyasını açın

/-- 256-bit EVM ADD: ikili, 2 eleman çıkarır, 1 eleman ekler.

Uzuv 0: LD, LD, ADD, SLTU (taşıma), SD (5 talimat).

Uzuvlar 1-3: LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OR (carryOut), SD (her biri 8).

Sonra ADDI sp, sp, 32.

Kaydediciler: x12=sp, x7=acc, x6=işlenen, x5=elde, x11=elde1. -/

def evm_add : Program :=

-- Uzuv 0 (5 talimat)

LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;

ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

-- 1. Uzuv (8 talimat)

LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;

ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

VEYA' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

-- 2. Uzuv (8 talimat)

LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;

ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

VEYA' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

-- 3. Uzuv (8 talimat)

LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;

ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

VEYA' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

-- sp ayarı

.x12 .x12 32 EKLE

EvmAsm.Evm64'ü sonlandır

RISC-V'nin seçilmesinin nedeni, oluşturulan ZK-EVM ispatlayıcılarının tipik olarak RISC-V'yi ispatlayarak ve Ethereum istemcilerini RISC-V'ye derleyerek çalışmasıdır. Bu nedenle, doğrudan RISC-V ile yazılmış bir EVM uygulamanız varsa, bu elde edebileceğiniz en hızlı uygulama olmalıdır.

RISC-V, sıradan bilgisayarlarda da oldukça verimli bir şekilde simüle edilebilir (ve piyasada RISC-V işlemcili dizüstü bilgisayarlar mevcuttur).

Elbette, uçtan uca doğrulamayı gerçekten başarmak için, RISC-V'nin kendisinin (veya ispatlayıcının aritmetiğinin) uygulamasını resmi olarak doğrulamanız gerekir, ancak endişelenmeyin, bu alanda zaten çalışmalar mevcut.

Elli yıl öncesine kadar doğrudan assembly dilinde kod yazardık. O zamandan beri, bu uygulamayı terk ederek üst düzey dillerde kod yazmaya başladık.

Üst düzey programlama dilleri verimlilikten ödün verir, ancak karşılığında çok daha hızlı kod yazmaya ve daha da önemlisi, güvenlik açısından hayati önem taşıyan başkalarının kodunu çok daha hızlı anlamaya olanak tanır.

Biçimsel doğrulama ve yapay zekanın birleşimiyle, "geleceğe geri dönme" fırsatına sahibiz.

Özellikle, yapay zekanın assembly kodu yazmasını sağlayabilir ve ardından assembly kodunun istenen özelliklere sahip olduğunu doğrulamak için resmi bir ispat yazabiliriz.

En azından, istenen özellikler, okunabilirliği optimize edilmiş ve insan dostu üst düzey bir dilde yazılmış bir uygulamanın mükemmel eşdeğerliği olabilir.

Okunabilirlik ve verimlilik arasında denge kurmak için artık tek bir kod nesnesine ihtiyacımız yok; bunun yerine, iki bağımsız nesnemiz var: biri (montaj uygulaması), belirli yürütme ortamının gereksinimlerini dikkate alarak yalnızca verimlilik için optimize edilmiş; diğeri (güvenlik bildirimi veya üst düzey dil uygulaması), yalnızca okunabilirlik için optimize edilmiş ve daha sonra ikisi arasındaki eşdeğerliği matematiksel bir ispatla kanıtlıyoruz.

Kullanıcılar bu kanıtı bir kez (otomatik olarak) doğrulayabilirler ve bundan sonra yalnızca hızlı sürümü çalıştırmaları gerekir.

Bu yaklaşım inanılmaz derecede güçlü ve Yoichi Hirai'nin buna "yazılım geliştirmenin nihai biçimi" demesinin bir nedeni var.

Resmi Doğrulama Her Derde Değmez

Kriptografi ve bilgisayar bilimi alanlarında, biçimsel yöntemlerin tarihi kadar eski bir gelenek vardır: biçimsel yöntemleri (veya daha geniş anlamda, "kanıtlar"a olan bağımlılığı) eleştirme geleneği.

Bu yazılar pratik örneklerle dolu. 2004'te Menezes ve Koblitz'in eleştirilerine atıfta bulunarak, erken dönem basit kriptografi çağından kalma el yazısıyla yazılmış ispatlarla başlayalım:

1979'da Rabin, bir anlamda "kanıtlanabilir" şekilde güvenli olan, yani indirgemeci bir güvenlik özelliğine sahip bir kriptografik fonksiyon önerdi.

İndirgemeci güvenlik açıklaması, şifreli metin y'den m mesajını bulabilen herkesin n'yi de çarpanlarına ayırabilmesi gerektiğini belirtir. ... Rabin şifreleme şemasını önerdikten kısa bir süre sonra Rivest, ironik bir şekilde, ona ek güvenlik sağlayan bu özelliğin, "seçilmiş şifreli metin" olarak bilinen bir saldırganla karşılaşıldığında tamamen çökmeye yol açacağını belirtti.

Yani, eğer saldırgan bir şekilde Alice'i kandırıp seçtiği şifreli metni çözmesini sağlayabilirse, saldırgan önceki paragrafta Sam'in n'yi çarpanlarına ayırmak için kullandığı adımların aynısını izleyebilir.

Menezes ve Koblitz daha sonra başka örnekler verdiler. Ortak örüntü, şifreleme protokollerini daha "kanıtlanabilir" hale getirmeyi amaçlayan tasarımların, onları genellikle daha az "doğal" hale getirmesi ve tasarımcıların hiç düşünmediği şekillerde başarısız olma olasılığını artırmasıdır.

Şimdi, makine tarafından doğrulanabilir ispatlara ve koda geri dönelim. İşte, biçimsel olarak doğrulanmış bir C derleyicisinde güvenlik açıkları keşfeden 2011 tarihli bir makale: makale:

Bulduğumuz ikinci CompCert sorunu, büyük bir PowerPC yığın çerçevesinin tahsis edildiği stwu r1, -44432(r1) kodunun oluşturulmasına yol açan iki hatada kendini gösteriyor.

Sorun şu ki, 16 bitlik yer değiştirme alanı taşma hatası verdi. CompCert'in PPC semantiği, bu anlık değerin genişliğine bir sınır koymamıştı; derleyicinin aralık dışı değerleri yakalayacağını varsaymıştı.

Ayrıca 2022 tarihli bir makale de var:

CompCert-KVX'te, e2618b31 commit'i bir hatayı düzeltti: "nand" komutu "and" olarak yazdırılıyordu; "nand" yalnızca nadir kullanılan ~ (a & b) kalıbında kullanılıyordu. Bu hata, rastgele oluşturulmuş programlar derlenirken keşfedildi.

Ve bugün, 2026'da, Nadim Kobeissi, Cryspen'de resmi olarak doğrulanmış yazılımlardaki güvenlik açıklarını şöyle tanımlıyor:

Kasım 2025'te Filippo Valsorda, libcrux-ml-dsa v0.0.3'ün aynı deterministik girdi verildiğinde farklı platformlarda farklı açık anahtarlar ve imzalar ürettiğini bağımsız olarak bildirdi.

Hata, SHA-3'ün Keccak-f permütasyonunda kullanılan XAR işlemini uygulayan dahili sarmalama fonksiyonu vxarqu64'te mevcuttu. Geri dönüş mekanizması, kaydırma işlemine yanlış parametreler ileterek, donanım SHA-3 desteği olmayan ARM64 platformlarında SHA-3 özetini bozuyordu.

Bu, tip I hatası kapsamına giriyor: dahili işlev işaretlendi, ancak NEON arka ucunun tamamı çalışma zamanı güvenliği veya doğruluğunun kanıtını tamamlayamadı.

Ve:

libcrux-psq kütüphanesi, kuantum sonrası önceden paylaşılan anahtar protokolünü uygular. decrypt_out yönteminde, AES-GCM 128 şifre çözme yolu, hataları yaymak yerine şifre çözme sonucunda .unwrap() yöntemini çağırır. Hatalı bir şifreli metin, işlemin çökmesine neden olabilir.

Bu dört sorunun tamamı aşağıdaki iki kategoriden birine giriyor:

Kodun yalnızca bir kısmının doğrulandığı (çünkü geri kalanının doğrulanması çok zordu) ve bunun sonucunda doğrulanmamış kodun yazarların hayal ettiğinden daha fazla (ve daha ölümcül) güvenlik açığına sahip olduğunun keşfedildiği durumlar.

Yazarların ispatlanması gereken temel özellikleri belirtmeyi unuttuğu durumlar.

Nadim'in makalesi, biçimsel doğrulamada başarısızlık modlarının bir sınıflandırmasını içeriyor; ayrıca diğer başarısızlık modlarını da sunuyor (örneğin, bir diğer önemli durum "biçimsel şartnamenin kendisinin yanlış olması veya ispatın, oluşturulan sistem tarafından sessizce kabul edilen yanlış ifadeler içermesi"dir).

Son olarak, yazılım ve donanım sınırında biçimsel doğrulamanın başarısızlıklarına bakabiliriz. Burada sık karşılaşılan bir sorun, yan kanal saldırılarına karşı direncin doğrulanmasıdır.

Mesajlarınızı korumak için mükemmel derecede güvenli şifreleme yöntemleriniz olsa bile, birkaç metre ötedeki biri elektrik sinyallerindeki dalgalanmaları yakalayıp yüz binlerce şifrelemeden sonra özel anahtarınızı ele geçirebiliyorsa, yine de güvende değilsiniz.

Bu, söz konusu tekniklerin iyi bilinen bir örneği olan "diferansiyel güç analizi" hakkında bir makaledir: makale.

Diferansiyel güç analizi, yaygın bir yan kanal saldırısı türüdür. Kaynak: Vikipedi

Bu tür saldırganlara karşı güvenlik sağlamaya yönelik girişimler her zaman olmuştur. Ancak, bu tür bir kanıt, saldırgana karşı güvenliği kanıtlamanıza olanak tanıyan bir matematiksel model gerektirir.

Bazen "d-sorgulama modeli" kullanılır: Saldırganın devrede sorgulayabileceği konum sayısının bilinen bir sınırı olduğunu varsayıyoruz. Ancak, bazı sızıntı biçimleri bu model tarafından yakalanmaz.

Bu makalede gözlemlendiği gibi, yaygın bir sorun geçici sızıntıdır: Eğer bir sinyalin yalnızca belirli bir konumdaki değere değil, aynı zamanda bu değerin nasıl değiştiğine de bağlı olduğunu gözlemleyebiliyorsanız, bu genellikle ihtiyacınız olan bilgiyi yalnızca bir değerden değil, iki değerden (eski ve yeni değerler) kurtarmak için yeterlidir.

Bu makale, diğer sızıntı türlerinin sınıflandırmasını sunmaktadır.

On yıllardır, biçimsel doğrulamaya yönelik bu eleştiriler, biçimsel doğrulamanın geliştirilmesine yardımcı oldu. Geçmişe kıyasla, bu tür sorunlara karşı korunmada artık daha iyiyiz. Ancak bugün bile mükemmel değil.

Genel tabloya baktığımızda, burada ortak bir tema var. Biçimsel doğrulama çok güçlü bir yöntemdir.

Ancak pazarlama terimleri ne kadar "kanıtlanabilir doğruluk" sağlıyormuş gibi gösterse de, sözde "kanıtlanabilir doğruluk" temelde yazılımın (veya donanımın) "doğru" olduğunu kanıtlamaz.

Çoğu insanın anlayışına göre, "doğru" demek, "nesnelerin davranışı, kullanıcının geliştiricinin niyetini anlamasıyla örtüşür" anlamına gelir.

"Güvenli" olmak ise şu anlama gelir: "Nesnelerin davranışı kullanıcının beklentilerini ihlal etmez ve kullanıcının çıkarlarına zarar verecek şeyler yapmaz."

Her iki durumda da doğruluk ve güvenlik, matematiksel nesneler ile insan niyetleri veya beklentileri arasındaki bir karşılaştırmaya indirgenir.

İnsan niyetleri ve beklentileri, kendi başlarına matematiksel olarak karmaşık nesnelerdir; sonuçta, insan beyni evrenin bir parçasıdır ve yeterli işlem gücüne sahipseniz simüle edilebilen fiziksel yasalara tabidir.

Ancak bunlar, ne bilgisayarların ne de bizim anlayabileceğimiz, hatta okuyabileceğimiz inanılmaz derecede karmaşık matematiksel nesnelerdir.

Pratik açıdan bakıldığında, bunlar kara kutulardır; niyetlerimiz ve beklentilerimiz hakkında bir fikrimiz ancak her birimizin yıllarca kendi düşüncelerimizi gözlemleme ve başkalarının düşüncelerini çıkarım yapma deneyimine sahip olmamız sayesinde vardır.

Ve insan niyetlerini olduğu gibi bilgisayara aktaramadığımız için, biçimsel doğrulama insan niyetleriyle karşılaştırmayı kanıtlayamaz.

Dolayısıyla, "kanıtlanabilir doğruluk" ve "kanıtlanabilir güvenlik", aslında biz insanların anladığı "doğruluk" ve "güvenlik" kavramlarını kanıtlamaz. İnsan beynini tam olarak simüle edemediğimiz sürece hiçbir şey bunu yapamaz.

Peki ne işe yarıyor?

Test paketlerini, tip sistemlerini ve biçimsel doğrulamayı, programlama dili güvenliğine yönelik aynı temel yaklaşımın farklı uygulamaları olarak görme eğilimindeyim (ki bu aynı zamanda tek mantıklı yaklaşım da olabilir).

Bunların hepsi, niyetlerimizi farklı şekillerde gereksiz yere belirtmek ve ardından bu farklı belirtmelerin birbiriyle uyumlu olup olmadığını otomatik olarak kontrol etmekle ilgili.

Örnek olarak şu Python kodunu ele alalım:

def fib(n: int) -> int:

eğer n < 0 ise:

Hata fırlat ("Negatif değerler desteklenmiyor")

elif 0 <= n < 2:

n'yi döndür

başka:

fib(n-1) + fib(n-2) döndür

Eğer __name__ == '__main__' ise:

[fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

assert fib(15) == 610

Burada niyetinizi üç farklı şekilde ifade edebilirsiniz:

Açıkça, Fibonacci formülünü kodda uygulayarak

Dolaylı olarak, tip sistemi aracılığıyla (girişlerin, çıkışların ve özyinelemedeki ara adımların tümünün tamsayı olduğunu belirterek)

"Örnek paket" yöntemi aracılığıyla: test senaryoları

Dosyayı çalıştırmak, formülü örneklerle karşılaştıracaktır. Tür denetleyicisi, türlerin uyumlu olup olmadığını doğrulayabilir: iki tamsayıyı toplamak uyumlu bir işlemdir ve başka bir tamsayı üretecektir.

Fizikte hesaplamaları kontrol etmenin iyi bir yolu genellikle tip sistemleridir: ivmeyi hesaplarken metre/saniye² yerine metre/saniye cinsinden bir cevap elde ederseniz, hata yaptığınızı anlarsınız.

Test senaryoları ise "örnek paket" tanımının bir örneğidir ve bu, insanların kavramları doğrudan ve açık tanımlamalardan daha doğal bir şekilde ele almalarının bir yoludur.

Niyetinizi ne kadar farklı şekilde ifade ederseniz, ideal olarak soruna farklı bir bakış açısıyla yaklaşmanızı gerektiren şekillerde, tüm bu ifadelerin birbiriyle uyumlu olduğu kanıtlandıktan sonra gerçekten ne istediğinizi ifade etme olasılığınız o kadar artar.

Güvenli programlama, niyetlerinizi birden fazla farklı şekilde ifade etmek ve ardından tüm bu ifadelerin birbiriyle uyumlu olup olmadığını otomatik olarak doğrulamakla ilgilidir.

Biçimsel doğrulama, bu yaklaşımı daha da genişletmenizi sağlar. Biçimsel doğrulama sayesinde, niyetlerinizi neredeyse sonsuz sayıda farklı ve gereksiz şekilde belirtebilirsiniz ve program ancak bunların tümü uyumluysa doğrulanabilir.

Son derece optimize edilmiş bir uygulama ve çok verimsiz ama insan tarafından okunabilir bir uygulama belirtebilir ve bunların eşleşip eşleşmediğini doğrulayabilirsiniz. On arkadaşınızdan programınızın sahip olması gerektiğini düşündükleri matematiksel özelliklerin bir listesini vermelerini isteyebilir ve ardından programın tüm bu özelliklere sahip olup olmadığını kontrol edebilirsiniz.

Eğer test başarısız olursa, programın hatalı olup olmadığını veya matematiksel özelliklerin yanlış belirtilip belirtilmediğini öğrenin. Ve tüm bu işlemleri son derece verimli bir şekilde gerçekleştirmek için yapay zekayı kullanabilirsiniz.

Peki nasıl başlayabilirim?

Gerçekçi olmak gerekirse, ispatları kendiniz yazmayacaksınız. Biçimsel yöntemlerin hiçbir zaman popülerlik kazanmamasının nedeni, çoğu insanın bu karmaşık şeyleri nasıl yazacağını çözememesidir. Bana aşağıdaki kodun ne anlama geldiğini söyleyebilir misiniz?

/-- Yardımcı: Foldl seviyesinde, bir biriktirici ile noktasal ≤ işlemi. -/

özel teorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (ab : Nat) (hAcc : a ≤ b)

(hLE : Forall₂ (· ≤ ·) ds1 ds2):

List.foldl (λ acc d => acc * w + d) a ds1 ≤

List.foldl (λ acc d => acc * w + d) b ds2 := by

ds1, ds2, hLE ile eşleştirin

| [], [], .nil => exact hAcc

| d1::ds1', d2::ds2', .cons hd htl =>

basit [List.foldl]

refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl

tam Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

(Merak ediyorsanız, bu, SPHINCS imzalarının bir varyantı için belirli bir güvenlik ifadesinin ispatındaki birçok alt önermeden biridir.)

Özellikle, ifade şu şekildedir: bir karma çakışması meydana gelmedikçe, bir karma özeti (dig1) kullanılarak oluşturulan bir mesajın imzası, diğer herhangi bir mesajın imzasından en azından bir yerde daha yüksek bir değere ihtiyaç duyacaktır; dolayısıyla bu, diğer imzadan hesaplanamayan bilgileri içerecektir.

Kod ve ispatları elle yazmanıza gerek yok; yapay zekanın sizin için programlar yazmasına (ister doğrudan Lean dilinde ister hız için assembly dilinde) ve bu süreçte istediğiniz özellikleri ispatlamasına izin vermeniz yeterli.

Bu görevin avantajı, kendi kendini doğrulayabilmesidir; bu nedenle denetlemenize gerek yoktur, yapay zekanın birkaç saat boyunca sürekli çalışmasına izin vermeniz yeterlidir.

En kötü sonuç, ilerleme kaydetmeden yerinde saymasıdır (ya da benim leanstral'ımın bir zamanlar yaptığı gibi, iş yükünü hafifletmek için kanıtlaması istenen ifadeyi değiştirmesidir).

Sonuç olarak kontrol etmeniz gereken tek şey, ortaya koyduğu iddiaların gereksinimlerinizi karşılayıp karşılamadığıdır.

SPHINCS imza varyantı söz konusu olduğunda, nihai açıklama şu şekildedir:

teorem wots_fullDigits_incomparable

{dig1 dig2 : List Nat} {w l1 l2 : Nat}

(hw : 0 < w)

(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)

(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)

(hL2suff : l1 * (w - 1) < w ^ l2)

(hNeq : dig1 ≠ dig2) :

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

Bu, neredeyse okunamaz durumda:

Bir karma özetinden (dig1) elde edilen sayılar, diğer bir karma özetinden (dig2) elde edilen sayılara eşit değilse

O halde aşağıdaki iki koşuldan hiçbiri geçerli değildir:

Tüm sayılar için, dig1'deki sayılar <= dig2'deki sayılardır.

Tüm sayılar için, dig2'deki sayılar dig1'deki sayılara eşittir (<= ).

Sağlama toplamlarının eklenmesiyle oluşturulan "genişletilmiş sayılarda" (wotsFullDigits). Yani, dig1'in genişletilmiş halinde, sayıların daha yüksek olduğu yerler kaçınılmaz olarak olacaktır, diğer yerlerde ise dig2'nin genişletilmiş halindeki sayılar daha yüksek olacaktır.

Kanıt yazmak için büyük dil modelleri kullanma açısından, hem Claude hem de Deepseek 4 Pro'nun yeterli olduğunu düşünüyorum. Leanstral, özellikle Lean yazmak için ince ayarlanmış daha küçük bir açık kaynaklı ağırlık modelidir ve umut vadeden bir alternatiftir.

119 milyar parametreye sahip olup, her token başına 6 milyar parametreyi etkinleştirir ve yerel olarak çalıştırabilirsiniz, ancak daha yavaştır (dizüstü bilgisayarımda yaklaşık 15 tok/sn). Karşılaştırmalı testlere göre, Leanstral çok daha büyük genel modellerden daha iyi performans gösteriyor:

Şu anki kişisel deneyimime dayanarak, Deepseek 4 Pro'dan biraz daha az etkili olduğunu ancak yine de oldukça etkili olduğunu söyleyebilirim.

Biçimsel doğrulama tüm sorunlarımızı çözemez.

Ancak, internet güvenliği modelinin artık birkaç güçlü kuruluşa güvenmeye dayanmamasını istiyorsak, kodlara güvenmeye yönelmeliyiz; bu da güçlü yapay zeka düşmanlarıyla karşı karşıya kaldığında bile kodlara güvenmeyi içerir.

Yapay zeka destekli biçimsel doğrulama, bu hedefe ulaşma yolunda bizi sağlam bir adım ileriye taşıdı.

Blockchain ve ZK-SNARK'lar gibi, yapay zeka ve biçimsel doğrulama da birbirini büyük ölçüde tamamlayan teknolojilerdir.

Blockchain, gizlilik ve ölçeklenebilirlik pahasına size açık doğrulanabilirlik ve sansür direnci sağlarken, ZK-SNARK'lar size gizlilik ve ölçeklenebilirliği (hatta daha önce sahip olduğunuzdan daha fazlasını) geri kazandırır.

Yapay zeka, doğruluktan ödün vererek çok miktarda kod yazma olanağı sağlarken, biçimsel doğrulama size doğruluk kazandırır (hatta daha önce sahip olduğunuzdan bile daha fazla).

Varsayılan olarak, yapay zeka son derece aceleyle yazılmış çok sayıda kod üretecek ve hata sayısı artacaktır.

Aslında, bazı durumlarda hata sayısındaki artışı hoş görmek doğru bir uzlaşmadır: eğer hatalar küçükse, hatalı yazılım bile hiç yazılım olmamasından daha iyidir.

Ancak burada siber güvenlik iyimser bir geleceğe sahip: yazılım, "güvenli bir çekirdek" etrafında "güvenli olmayan uç parçalara" (bölünmeye) devam edecek.

Güvenli olmayan uç noktalar, görevlerini tamamlamak için gerekli olan minimum izinler verilerek sanal ortamlarda çalışacaktır.

Güvenli çekirdek her şeyi yönetecek. Güvenli çekirdek çökerse, kişisel verileriniz, paranız ve benzeri her şey çöker. Ancak güvenli olmayan bir uç nokta çökerse, güvenli çekirdek sizi yine de koruyabilir.

Güvenli çekirdek söz konusu olduğunda, hatalı kodun yayılmasına izin veremeyiz. Güvenli çekirdeği küçük tutmak ve hatta daha da küçültmek için radikal önlemler alacağız.

Bunun yerine, yapay zekanın getirdiği tüm ekstra performansı, güvenli çekirdeği daha güvenli hale getirmek için kullanacağız ve böylece dijitalleşmiş bir toplumda ona yüklediğimiz son derece yüksek güven yüklerini taşıyabilmesini sağlayacağız.

Bir işletim sisteminin çekirdeği (veya en azından bir kısmı) böyle bir güvenli çekirdek haline gelecektir.

Ethereum da bir diğeri olacak.

Umarım, en azından performans gerektirmeyen tüm hesaplamalar için, kullandığınız donanım üçüncü bir bileşen haline gelir.

Nesnelerin İnterneti ile ilgili sistemler dördüncü sırada yer alacak.

En azından bu güvenli çekirdekler arasında, "hatalar kaçınılmazdır; saldırgan bulmadan önce siz ancak onları bulmaya çalışabilirsiniz" şeklindeki eski atasözü çürütülecek ve yerini gerçek güvenliğe ulaşacağınız daha umutlu bir dünyaya bırakacaktır.

Ama eğer varlıklarınızı ve verilerinizi kötü yazılmış ve yanlışlıkla kara deliğe çekebilecek bir yazılıma teslim etmeye razıysanız, elbette bu özgürlüğe de sahipsiniz.