Certora Baş Bilim İnsanı Mooly Sagiv: Blockchain Güvenliği Koddan Daha Fazlasıdır

2025 bize bir şey öğrettiyse, o da Solana'nın patlama hızına ulaşması ve kendisini “perakende zinciri “olarak kurmasıydı. Her gün binlerce kullanıcı, potansiyel riskleri umursamadan akıl almaz derecede karmaşık akıllı sözleşmelerle etkileşime girerek para taşıyor ve işlem imzalıyor.

Tabii ki hizmetin altında hala riskler var. Ancak kripto hack'leri ve istismarları hala istediğimizden çok daha yaygın olsa da, insanlar genellikle en büyük risklerin belirsiz mantık ve teknik kod tabanlarının derinliklerine gömülü olduğunu varsayıyor."

Mooly Sagiv o kadar da emin değil.

190 milyar doların üzerinde DeFi TVL'nin güvenliğini sağlayan bir blok zinciri güvenlik firması olan Certora'nın Baş Bilim Adamına göre, kayıpların çoğu kod mantığındaki hatalardan veya programlama hatalarından değil, çok daha basit suçlulardan kaynaklanıyor:  Anahtarlar, saklama ve insan hatası. 

“Anahtarınıza… ve telefonunuza göz kulak olun.”

Bu basit bir uyarıdır, ancak kripto güvenliğine yönelik kritik derecede önemli ve genellikle gözden kaçan bir yaklaşımı yakalar. Güvenlik hataları nadiren “sadece bir hata”dır ve mobil kripto uygulamalarının çoğalması yalnızca daha fazla değişken ve potansiyel güvenlik açığı ekler. 

Sagiv bu durumu ortaya koymak için benzersiz bir konuma sahip. Akademik meslektaşları arasında Shmuel (Mooly) Sagiv olarak tanınan Certora Baş Bilim İnsanı, aynı zamanda yaklaşık 28 yıldır Tel Aviv Üniversitesi Yazılım Sistemleri Kürsüsü Başkanı olarak görev yapmaktadır. Program analizi ve doğrulama alanında onlarca yıldır araştırma yapan Sagiv, Certora’nın biçimsel doğrulamayı niş bir disiplinin ötesine taşıyarak geliştiricilerin sürekli olarak çalıştırabileceği bir şeye dönüştürme çabasında öncü bir rol oynamaktadır.

SolanaFloor ile Breakpoint 2025'te konuşan Mooly Sagiv, blockchain güvenliğinin karanlık ormanına aydınlatıcı bir ışık tuttu. DeFi'deki en büyük isimlerden bazılarının denetiminden sorumlu olan Certora’nın Baş Bilim İnsanı, kripto kullanıcılarının güvenlik, resmi doğrulamanın önemi ve yapay zeka ve kuantum hesaplama risklerinin abartılıp abartılmadığı konusunda sahip oldukları en büyük yanılgılardan bazılarını açıkladı.

Kripto Güvenliği’nin En Büyük Yanılgısı: “Tüm Hatalar Kodda”

Blockchain güvenliğiyle ilgili yanlış anlamalar söz konusu olduğunda Sagiv, kripto kültürünün çok gevşek olduğunu savunuyor. En tehlikeli yanlış anlama, güvenlik açıklarının yalnızca kodda bulunduğu ve kod denetlenirse kullanıcıların sağduyuyu ortadan kaldırabileceği inancıdır.

“Herkes tüm hataların kodda olduğunu düşünür. Ve bu her zaman böyle olmayabilir… belki kodunuz mükemmeldir, ancak dağıtılma şeklinin dışında… bir şeyler olacaktır…”

Kripto uzmanları ‘kod kanundur’ gibi temel felsefi ilkeleri savunurlar. Ancak bu doğru olsa da, hala dikkate alınması gereken düzinelerce değişken vardır. Bir protokol “doğru” olabilir ve yine de güvensiz olabilir çünkü anahtarlar zayıf bir şekilde kontrol edilir, entegrasyonlar gözeneklidir veya operasyonel ortam tehlikeye atılmıştır. Bir uygulama ancak onu yöneten kişilerin sistemleri ve davranışları kadar güvenlidir.

Sagiv’in ikinci yanılgısı çoğu kullanıcının inanmak istediği yanılgıdır: “denetlenmiş” güvenlik anlamına gelir.

“Asla tamamen güvenli değildir. Daha güvenli hale getirebiliriz… ama asla tamamen güvenli değildir.”

Denetimler şüphesiz kripto güvenliğinin ayrılmaz bir parçasıdır, ancak hiçbir şekilde bir garanti değildir. İnsanlar bir uygulamanın denetlendiğini gördüklerinde yanlış bir güvenlik duygusu geliştirirler, ancak DeFi kullanıcıları kesinlikle temel güvenlik uygulamalarını unutmamalıdır.

Certora’nın Güvenliğe Hibrit Yaklaşımı

Sagiv denetimleri reddetmiyor. Aslında, resmi doğrulamanın insan incelemesinin yerini alması fikrine açıkça karşı çıkmaktadır. Bunun yerine, resmi doğrulama ve insan denetimleri mümkün olduğunca fazla kapsam sağlamak için ideal olarak birlikte kullanılmalıdır.

SolanaFloor ile konuşan Sagiv, denetimlerin tipik olarak bilinen saldırı modellerine karşı nasıl korunduğunu, resmi doğrulamanın ise “bilinmeyen bilinmeyenlere ”

maruz kalmayı nasıl azaltabileceğini özetledi.

“Denetim yaptığınızda, kodunuzu bilinen saldırılara karşı en iyi kişinizle gözden geçiriyorsunuz. Biçimsel doğrulama yapabildiğinizde… bilinmeyen bilinmeyenlere karşı bir tür [önlem] almış olursunuz.”

Bu fark önemlidir çünkü kripto bir silahlanma yarışıdır. Saldırı teknikleri gelişiyor ve bilgisayar korsanları ve siber suçlular her gün kullandığımız milyar dolarlık uygulamaları kırmak için her zaman yeni yöntemler ve teknikler buluyorlar.

Yeni hata sınıfları keşfediliyor çünkü birileri, bir yerlerde, endüstrinin yaptığının farkında bile olmadığı varsayımları kırmanın akıllıca bir yolunu buldu. Biçimsel doğrulama, bu “bilinmeyen bilinmeyenlere” karşı başka bir savunma hattı sağlamayı amaçlamaktadır.

Sagiv, Certora'nın defalarca gördüğü bir modeli anlatıyor. Ekipler her şeyi “doğru” yapabilir, güvenlik için muazzam iç kaynaklar ayırabilir, seçkin denetçiler tutabilir ve ardından resmi doğrulama yine de ek yüksek ciddiyetli sorunları ortaya çıkarır.

“En iyi güvenlik [araştırmacısının]… 10 kritik bulmasına izin verdiniz. Çok mutlu olursunuz. Ve sonra resmi doğrulamayı çalıştırırsınız. İki tane daha bulur.”

Bu tez, FV'nin önemini ve etkisini göstermek için Solana Breakpoint'te sahne alan Certora’Formal Verification Team Lead Pamina Georgiev tarafından daha da güçlendirildi.

Biçimsel doğrulamanın sunduğu tüm vaatlere ve korumaya rağmen, hala mükemmel bir sistem olmaktan uzaktır. Biçimsel doğrulama, kripto Twitter'ın bazı kesimlerinin sizi inandırmak istediklerinin aksine, bilgisayar korsanlarını izlerinde durduran aşılmaz bir güç alanı değildir.

.

Sagiv, bu çerçevelemenin neden tehlikeli olduğu konusunda açık sözlüdür.

.

“Biçimsel doğrulamadaki en büyük sorun, hangi özelliğin [belirtileceğini]” anlamaktır.

Formal doğrulama, kodun mutlak anlamda güvenli olduğunu kanıtlamaz. Kodun bir dizi özelliği karşıladığını kanıtlar; kanıtlamasını istediğiniz özellikler. Yanlış özellikleri seçerseniz, son derece güvenilir görünen ancak su geçirmezlikten uzak bir şey elde edersiniz.

CI, Otomasyon ve “Döngüde İnsan Yok”

Sagiv’in Breakpoint'teki en açık noktalarından biri, güvenliğin tek seferlik bir olay olmadığıdır. Bir uygulama birkaç yıl önce bir denetimden geçtiği için bugün hala güvenli olacak diye bir şey yok. Bu durum özellikle protokollerin ve saldırı yöntemlerinin sürekli olarak yinelendiği ve tek bir kod satırında yapılan değişikliklerin yığının başka yerlerinde de yankı bulabildiği kriptoda geçerlidir.

.

“Tamamen değişir, bir satırdaki değişiklik tüm kodu bozabilir.”

Certora'nın doğrulamayı geliştirici iş akışına dahil etmesinin nedeni budur. Sagiv, Certora'nın CI boru hatlarına entegre olduğunu, böylece her yeni işlemin doğrulama kontrollerini otomatik olarak tetiklediğini ve tek seferlik bir kilometre taşı yerine sürekli bir korkuluk oluşturduğunu söylüyor.

“Her değişiklik yaptıklarında, kodda bir taahhütte bulunurlar, resmi doğrulamayı çalıştırırız. Aslında aracımızın güzelliği de bu. Aracımız otomatiktir; insan döngünün içinde değildir.”

Certora, Rust dilinde yazılmış Solana akıllı sözleşmelerini doğrulamak için tasarlanmış “Certora Solana Prover” ile Solana programlarının resmi doğrulaması için özel belgeler bulundurmaktadır.

Cypherpunks & Academia

Genellikle cypherpunk, düzen karşıtı bir ethos'a dayanan birçok kripto kökenli hikayenin aksine Sagiv, sektöre çok ihtiyaç duyulan akademik bir sınıf getiriyor. Akademiden geçişini entelektüel meydan okuma ve gerçek dünya riskleri arasında bir çarpışma olarak tanımlıyor

.

“Kripto, çok fazla değer taşıyan küçük kodlara sahip olduğunuz tek alandır”

Geleneksel güvenlik açısından kritik yazılımlarda, kod çok büyük olabilir, ancak genellikle eski, kararlı ve kripto’nun hızlı yinelemesinin tam bir antitezidir. Bu, Certora’nın favori sloganlarından birinin temelini oluşturmuş olabilir: “Hızlı hareket et ve hiçbir şeyi kırma”

Sagiv, kriptoyu biçimsel yöntemlere mükemmel bir uyum olarak çerçeveliyor çünkü çoğu doğası gereği matematiksel: dengeler, değişmezler, koruma kısıtlamaları, erişim kontrol kuralları ve kesin olarak ifade edilebilen durum geçişleri.

“Hala akademik dersler veriyorum. Bazı insanlar kriptoyu sevmiyor. Onları teknik açıdan motive etmeye çalışıyorum. Tekniğe geri dönüyorum ve onlara neyin zor olduğunu anlatıyorum.”

Akademik meslektaşları kriptoya şüpheyle yaklaşsa da Sagiv, kriptonun yeni geliştiriciler için bilgisayar bilimlerinin en teşvik edici ve motive edici alanlarından biri olduğunu vurguluyor

.

Solana’s “Can-Do Attitude”

Certora hiçbir şekilde Solana'ya özel bir güvenlik firması değildir, ancak bu şirketin DeFi zinciriyle derinden iç içe olmadığı anlamına gelmez. Solana’nın en büyük ve en etkili uygulamalarından bazılarıyla çalışmış olan Sagiv, ekosisteme yalnızca üst düzey ekiplerle omuz omuza olmanın getirdiği bir operasyonel saygı düzeyi sağlıyor.

Certora’nın Solana ile ilk ilişkisi, Sagiv“in “inanılmaz&rdquo dediği Squads ile oldu; Certora oradan Solana Vakfı ile çalıştı ve SPL programlarının özelliklerini doğruladı ve işbirliğini alışılmadık derecede açık olarak tanımladı.

En çok dikkat çeken şey ise diğer ortamlarla yaptığı karşılaştırma. Solidity Developers ile yaşadığı deneyime değinen Sagic, ekiplerin değişikliklere karşı dirençli olabildiğini belirtti.

“İnsanlarla konuştuğumuzda, bazen Solidity'de, onlardan kodu değiştirmelerini istediğimizde çok isteksiz davranıyorlar. Sınırlı bir zamanımız olduğunu söylüyorlar… Burada [Solana] insanlar daha çok ‘yapabilirim’ tavrına sahipler. Onlardan kodu değiştirmelerini istiyorsunuz, çok açık sözlüler.”

2026'da Güvenlik Tehditleri

2026 yılında insanların farkında olması gereken en büyük tehditler sorulduğunda Sagiv, insanların kod güvenlik açıklarına aşırı endekslenmemesi gerektiğini bir kez daha vurguladı. İyi bir operasyonel güvenlik çok yönlüdür ve ortalama bir kripto sahibinin kendisini sosyal mühendislik veya saklama hatası kurbanı olarak bulması, bir DeFi istismarında fon kaybetmesinden çok daha olasıdır

.

“Her türlü şeyin gerçekleştiğini görüyoruz, bu sadece kod değil.”

O’haksız değil. Chainalysis’ 2025 Kripto Suç Raporuna göre, dolandırıcılar 2025 yılı boyunca 14 milyar doların üzerinde para çaldı.

Sagiv ayrıca yapay zeka tehdidinin gereğinden fazla büyütüldüğüne inanıyor. Bir güvenlik uzmanından bekleyebileceğiniz gibi, Certora’nın Baş Bilim İnsanı yapay zekayı kötü niyetli bir tehdit olarak değil, bir araç olarak görüyor. Kabul etmek gerekir ki, yapay zeka saldırganlar için bir çarpan görevi görebilir, ancak savunucular ve güvenlik firmaları tarafından da kullanılabilir. 

“Kötü adamlar yapay zeka kullanabilir. İyi adamlar yapay zekayı kullanabilir,”

YZ, güvenlik açıklarının bulunmasına yardımcı olursa, özelliklerin kanıtlanmasına, daha güçlü spesifikasyonların oluşturulmasına ve doğrulama sorunlarının çözülmesine de yardımcı olabilir.

.

Kripto asla “tamamen güvenli ” olmayacaktır ve Solana ’bir sonraki saldırgan dalgasının icat ettiği her şeye karşı bağışık olmayacaktır. Ancak ileriye dönük yol Kripto Güvenliği 101'e sadık kalmaktadır: Anahtar yönetimini sıkılaştırın, sağduyulu davranın ve güvenliği bir kez ilan edip unuttuğunuz bir şey olarak değil, sürekli kanıtladığınız bir şey olarak ele alın.

SolanaFloor hakkında daha fazlasını okuyun

Tek kesinlik belirsizliktir.

Çin-Kanada Ticaret Görüşmeleri, Yen Enflasyonu ve Bir Başka Hükümet Kapanması Kripto Piyasalarını Korkuttu

SolanaFloor Certora’dan Mooly Sagiv ile Görüştü