Giriş

Kripto ekonomide farklı kullanım senaryolarını başlatan birkaç proje ile blok zincirindeki varlıkların değeri hızla artarken, olası açıklar ve tehditlerin önünde olmak daha da önemlidir.

Bitcoin, bankaları değiştirmek için icat edildi, ancak temel teknoloji olan blok zinciri, neredeyse herhangi bir aracıyı değiştirebileceğini kanıtladı. İlerleyen süreçte, kağıt para asla yapamadığı dijital paranın sahip olduğu muazzam potansiyeli görerek durmadı ve bunun programlanabilir para yeteneğini içerir. Birdenbire, avukatlar ve sözleşmeler finansal işlemlerde yerine geçebilirdi. Bu dijital para birimi, tam şeffaflık ve insan müdahalesi olmaksızın sözleşmelerin otomatik olarak yürütülmesini sağlayarak merkeziyetsizleşmeyi ilerletti. Ancak, akıllı sözleşmeler tam olarak nasıl çalışır? Güvenin eksik olduğu bu sistemlere gerçekten güvenilir mi?

Bu makalede, Ethereum üzerindeki akıllı sözleşmelerin biçimsel doğrulaması hakkında kapsamlı soruları keşfedeceğiz, avantajları, dezavantajları, kripto ekosisteme etkisi ve daha fazlasını vurgulayarak tartışacağız.

Akıllı Sözleşmelerin Kısa Tarihi

Kaynak: CryptoSlate

Nick Szabo, Amerikalı bir bilgisayar bilimcisi ve şifre uzmanı olan ve genellikle Satoshi Nakamoto olmasıyla spekülasyonlara konu olan, akıllı sözleşmelerin öncüsüdür ve 1994 yılında bu kavramı ilk kez tanıtmıştır. Szabo, akıllı sözleşmeleri, bir anlaşmanın koşullarını otomatik olarak uygulamak için tasarlanmış dijital işlem protokolleri olarak tanımladı. Amacı, satış noktası sistemleri gibi elektronik işlem yöntemlerini geliştirmek ve yeteneklerini dijital dünyaya genişletmektir.

Szabo, anlaşmaların otomatik, güvenilir ve müdahale edilemez şekilde çalışabileceği bir gelecek hayal etti. Zamanının teknolojisi tam anlamıyla vizyonunu gerçekleştirmek için yeterince ileri değildi, ancak Szabo'nun fikirleri daha sonra blok zinciri endüstrisini devrimlendirmek için temel oluşturdu.Ethereum başlatıldı2015 yılında, akıllı sözleşmeleri pratik kullanıma getirerek, Szabo'nun teorik kavramlarını merkezi olmayan uygulamaların temel bileşenlerine dönüştürdü.

Onun vizyonu, insan müdahalesi ve denetimin ihtiyacını azaltarak, hassas, otomatik koşullarla ilişkileri yönetebilecek sözleşmeler içindi. Bu yaklaşım, anlaşmaları ele almanın daha güvenli ve verimli bir yolunu oluşturmayı amaçladı ve bu da akıllı sözleşmelerin blockchain ekosisteminde güçlü araçlara dönüşmesinin yolunu açtı. Szabo'nun erken içgörüleri, dijital işlemlerin peyzajını ve akıllı sözleşme gelişimini bugün de şekillendirmeye devam ediyor.

Biçimsel Doğrulama nedir?

Kaynak: Orta

Biçimsel doğrulama, bir akıllı sözleşme gibi bir sistemın belirlenmiş bir kural veya özellik kümesine göre çalışıp çalışmadığını sıkı bir şekilde değerlendirme sürecidir. Temelde, sistemin beklenildiği gibi davranıp davranmadığını kontrol eder, gereken koşulları karşıladığından ve hatalar olmadan amaçlanan işlevleri gerçekleştirdiğinden emin olur.

Bunu başarmak için, sistemin beklenen davranışları biçimsel modeller kullanılarak ana hatlarıyla belirtilirken, sözleşmenin karşılaması gereken özellikleri tam olarak tanımlamak için spesifikasyon dilleri kullanılır ve makale ilerledikçe daha pratik senaryolar göreceğiz. Resmi doğrulama teknikleri daha sonra sözleşmenin uygulanmasını spesifikasyonlarıyla eşleştirerek doğruluğunun matematiksel kanıtını sağlar. Bir sözleşme bu özellikleri karşıladığında, "işlevsel olarak doğru" veya "tasarım gereği doğru" olarak kabul edilir ve blok zinciri ortamındaki güvenilirliğini ve güvenliğini teyit eder.

Akıllı Sözleşmeler için Biçimsel Özelliklerin Türleri

Kaynak: Her Zaman Ölçek

Formal spesifikasyonlar, bir programın yürütmesinin doğruluğunu doğrulamak için matematiksel akıl yürütme kullanma yöntemi sağlar. Bu spesifikasyonlar, genel davranışa odaklanan yüksek seviye özellikleri veya bir sözleşmenin iç işleyişine ilişkin düşük seviye ayrıntıları tanımlayabilir. Bu davranışları matematiksel olarak tanımlayarak, formal spesifikasyonlar sözleşmenin amaçlandığı gibi çalıştığından emin olur.

Yüksek seviye specifikasyonları

Yüksek düzeydeki özellikler, aynı zamanda model odaklı özellikler olarak da bilinir, akıllı bir sözleşmenin genel davranışını tanımlar; onu belirli işlemler aracılığıyla farklı durumlar arasında geçiş yapan bir sonlu durum makinesi (FSM) olarak ele alır. Zaman mantığı genellikle bu geçişleri yöneten biçimsel kuralları tanımlamak için kullanılır, sözleşmenin zaman içinde durumlar arasında nasıl hareket ettiğini ve bunu doğru bir şekilde yapmak için karşılaması gereken koşulları detaylandırır.

Bu özellikler iki temel özelliği ele alır: güvenlik ve canlılık. Güvenlik, gönderenin bakiyesinin bir işlem için gereken miktardan daha az düşmesi gibi istenmeyen olayların meydana gelmemesini sağlar. Tersine, canlılık, kullanıcılar talep edildiğinde fon çekebilsinler diye likiditeyi koruyarak sözleşmenin devam etmesini ve ilerlemesini sağlar. Her iki özellik de akıllı sözleşmelerin güvenli ve güvenilir bir şekilde çalışmasını sağlar, kullanıcı etkileşimlerini ve varlıklarını korur.

Düşük seviye özellikleri

Düşük seviye özellikleri, aynı zamanda özellik odaklı özellikler olarak da bilinir ve akıllı sözleşmelerin içsel yürütme süreçlerini analiz ederek doğru davranışlarını tanımlamaya odaklanır. Sözleşmeleri sonlu durum makineleri olarak modelleyen yüksek seviye özelliklerin aksine, düşük seviye özellikler akıllı sözleşmeleri matematiksel fonksiyon sistemleri olarak görür ve sözleşmenin durumunu değiştiren, iz olarak bilinen fonksiyon yürütme dizilerini incelemektedir.

Akıllı Sözleşmelerin Biçimsel Doğrulama Teknikleri

Kaynak: Her Zaman Ölçek

Model Kontrolü

Model kontrolü, akıllı sözleşmenin modelinin belirtildiği gibi olup olmadığını değerlendirmek için algoritmalar kullanan bir biçimsel doğrulama yöntemidir. Akıllı sözleşmeler genellikle durum geçiş sistemleri olarak temsil edilir ve özellikleri zamansal kullanılarak tanımlanır.mantıkBu süreç, sözleşmenin matematiksel bir modelinin oluşturulmasını ve mantıksal formüller aracılığıyla özelliklerinin ifade edilmesini içerir, bu da algoritmanın modelin bu özellikleri karşılayıp karşılamadığını doğrulamasına olanak tanır.

Teorem Kanıtlama

Model kontrolüne karşı, teorem kanıtlama, akıllı sözleşmeler de dahil olmak üzere programların doğruluğunu sağlamak için kullanılan matematiksel bir yaklaşımdır. Bu yöntem, bir sözleşmenin modelini ve özelliklerini mantıksal formüllere dönüştürerek bunların mantıksal eşdeğerliğini doğrulamayı içerir, yani diğer ifadenin doğruysa bir ifade doğrudur. Bu ilişkiyi bir teorem olarak formüle ederek, otomatik teorem kanıtlayıcı, sözleşme modelinin doğruluğunu özelliklerine karşı doğrulayabilir.

Model kontrolü ile keskin bir tezat oluşturan teorem kanıtlama, sonlu durumlu sistemlerle sınırlı olsa da sonsuz durumlu sistemleri analiz edebilir, ancak genellikle karmaşık mantık problemlerini yönlendirmek için insan rehberliği gerektirir. Sonuç olarak, teorem kanıtlama, tamamen otomatik model kontrol sürecinden daha fazla kaynak yoğun olma eğilimindedir.

Sembolik Yürütme

Sembolik yürütme, belirli girişler yerine sembolik değerlerle fonksiyonları yürütmeyi içeren akıllı sözleşmeler için güçlü bir analiz yöntemidir. Bu biçimsel doğrulama tekniği, yürütme yollarını matematiksel formüller olarak temsil ederek bir sözleşmenin kodundaki iz seviyesi özellikleri hakkında akıl yürütme yapmayı sağlar. Bu formüllerin tatmin edilebilir olup olmadığını belirlemek için bir SMT çözücü kullanılır, yani koşulları karşılayan bir giriş mevcuttur.

Örneğin, bir sözleşme işlevi 5 ile 10 arasında bir değer olduğunda geri dönerse, sembolik yürütme koşulu X > 5 ∧ X < 10 olarak değerlendirerek böyle tetikleyici değerleri verimli bir şekilde belirleyebilir. Bu yöntem, geleneksel testlerden daha etkili olabilir ve daha az yanlış pozitif üretebilir, herhangi bir SMT çözücüsü tarafından bulunan hataları doğrudan üretebilen somut değerler oluşturur. Bu nedenle, akıllı sözleşme güvenilirliğinin sağlanmasında değerli bir araç haline gelir.

Akıllı sözleşmeler nedir?

Kaynak: Nazikçe

Akıllı sözleşmeler, belirli koşullar karşılandığında işlemleri gerçekleştiren bir blok zincirinde çalışan otomatik bilgisayar programlarıdır. Basit anlaşmalardan çok karmaşık süreçlere kadar değişebilirler ve milyonlarca veya hatta milyarlarca dolar değerinde varlıkları yönetebilirler.

Akıllı sözleşmeler, siyasi oylama, tedarik zinciri yönetimi, sağlık hizmetleri ve gayrimenkul gibi çeşitli sektörleri devrim yapma potansiyeline sahipken, bu makale hala kripto para birimi alanındaki etkilerine odaklanmaktadır. Tasarımları, manipülasyon riski olmadan çoklu tarafların işbirliği yapmasına izin vererek, verimlilik ve yenilikçiliği artıran şeffaf ve güvenli bir çerçeve sunar. Bununla birlikte, akıllı sözleşmelerin de güvenlik açıkları ve zorlukları olduğunu kabul etmek önemlidir.

Akıllı Sözleşmeler ile İlgili Zayıf Noktalar

Güvenlik açıklarıAkıllı sözleşme kodunda bir hata, son zamanlardaki olaylar tarafından gösterildiği gibi, sözleşme içinde depolanan varlıkların tamamen kaybına yol açabilir ve felaketle sonuçlanabilir.

• 2021 yılında otomatik piyasa yapıcısı Uranium Finance 50 milyon dolarlık bir hırsızlık yaşandıakıllı sözleşmesindeki basit bir yazım hatası nedeniyle.
• Ayrıca 2021'de, Compound Finance yanlışlıkla 80 milyon dolar dağıttıtek bir karakter hatası nedeniyle kazanılmamış ödüllerde yine
• Daha önemli bir ihlal 2022'de meydana geldi Wormhole Köprüsünden 320 milyon dolar çalındığındaakıllı sözleşmelerinden birindeki bir hatadan dolayı.

Bu örnekler verildiğinde, akıllı sözleşmelerin baştan doğru bir şekilde kodlanmasının son derece önemli olduğunu sağlamak önemlidir. Dağıtıldıktan sonra, akıllı sözleşmeler açık kaynaklıdır, yani kodları genel olarak erişilebilir olduğundan, keşfedilen herhangi bir zayıflıktan faydalanmak için hacker'ların kolayca kullanabileceği anlamına gelir. Ek olarak, akıllı sözleşmelerin değiştirilemez doğası, bir kez başlatıldıklarında, genellikle güvenlik açıklarını yamalamak için kodlarının değiştirilemeyeceği anlamına gelir, bu da en üst düzeyde hassasiyetle geliştirilmediyse, sürekli bir risk altında bırakır.

Akıllı Sözleşme Doğrulaması Nasıl Çalışır?

Kaynak: Certik

İşlem şunları içerir:

• Formal dil kullanarak sözleşmenin özelliklerini ve istenen özelliklerini tanımlama.
• Sözleşmenin kodunu matematik modelleri veya mantıksal ifadeler gibi biçimsel bir temsile çevirmek.
• Otomatik teorem kanıtlayıcıları veya model denetleyiciler, sözleşmenin özellik ve özelliklerinin geçerliliğini onaylamak için kullanılır.
• Doğrulama sürecini tekrarlayarak hataları veya amaçlanan özelliklerden sapmaları belirlemek ve düzeltmek için tekrarlayın.

Akıllı Sözleşmelerin Temel Özellikleri

Kaynak: Certik

Akıllı sözleşmeleri bir kere oluşturulduktan sonra değiştirilemez anlaşmalar olarak düşünün. Zincirin değiştirilemeyen defteri üzerinde çalışan bu sözleşmeler, aracılar olmadan koşulları otomatik olarak uygular ve işlemleri hızlandırır ve maliyetleri düşürür. Bu sabit özellik güvenliği artırır ve kontrolü merkezsizleştirir, dolandırıcılık ve yolsuzluğun olasılığını önemli ölçüde azaltır.

Neden Akıllı Sözleşme Doğrulamanın Önemli Olduğu

Matematiksel akıl yürütme, biçimsel olarak doğrulanan akıllı sözleşmelerin hatalardan, güvenlik açıklarından ve beklenmedik davranışlardan uzak olduğunu sağlamak için önemli bir rol oynar. Bu titiz süreç, özellikleri tamamen doğrulanmış olduğu için sözleşmeye olan güveni ve güveni artırır.

Başarılı akıllı sözleşme doğrulama örnekleri, önemini önemli finansal kayıpları önlemede vurgulamaktadır.

Uniswap

Örneğin, Uniswap, iyi bilinen bir otomatik piyasa yapıcısı (AMM), V1 akıllı sözleşmesinin geliştirilme sürecinde biçimsel doğrulamadan geçti ve bu süreçte yuvarlama hatalarını tespit edip düzeltti fonları boşaltmış olabilirdi.

Dengeleyici

Benzer şekilde, formal doğrulama keşfeden Balancer V2 gibi başka bir AMM'den faydalandı.yanlış bir ücret hesaplamaflash kredileriyle ilgili olarak, potansiyel hırsızlığı önleyerek.

SafeMoon

SafeMoon V1'in hafif bir hatası vardıDağıtımdan sonra biçimsel doğrulama ile belirlendi. Bu hata, sahibin belirli koşullar altında sahipliği reddetmesine ve tekrar kazanmasına izin verdi, çoğu manuel denetim tarafından karmaşıklığından dolayı gözden kaçırılan bir ayrıntı. Biçimsel doğrulamanın değişken değerlerinin belirli kombinasyonlarını analiz etme yeteneği, insan denetçilerin gözden kaçırabileceği sorunları yakalamak için etkili bir araç yapar.

Biçimsel Doğrulama ve Manuel Denetimin Nasıl Birlikte Çalıştığı

Biçimsel doğrulama, akıllı sözleşmenin mantığını ve davranışını amaçlanan özelliklerine karşı kontrol etmek için sistemli ve otomatik bir yöntem sunar. Bu yaklaşım, özellikle manuel incelemelerin gözden kaçırabileceği potansiyel hataları veya hataları belirlemeyi ve düzeltmeyi basitleştirir.

Öte yandan, manuel denetim, bir uzmanın sözleşmenin kodunu, tasarımını ve dağıtımını kapsamlı bir şekilde incelemesini içerir. Denetçi, güvenlik risklerini belirlemek ve sözleşmenin genel güvenlik duruşunu değerlendirmek için deneyimlerinden yararlanır. Ayrıca resmi doğrulama sürecinin doğruluğunu onaylayabilir ve otomatik araçların gözden kaçırabileceği sorunları belirleyebilirler. Resmi doğrulamayı manuel denetimle birleştirmek, kapsamlı bir güvenlik değerlendirmesi oluşturarak güvenlik açıklarını ortaya çıkarma ve çözme olasılığını artırır ve hem insan uzmanlığının hem de otomatik analizin güçlü yönlerinden yararlanan sağlam bir savunma stratejisi oluşturur.

Akıllı Sözleşmelerin Artıları ve Eksileri

Kaynak: Blockonomi

Akıllı sözleşmeler mükemmel değiller, ancak avantajları dezavantajlarından önemli ölçüde ağır basmaktadır. Karmaşık işlemleri basitleştirerek zaman ve para tasarrufu sağlar, şeffaflığı teşvik eder ve anlaşmazlıkları azaltır. Kod üzerinde çalıştıkları için insan hatalarını en aza indirirler. Kriptografik korumalar sayesinde güvenlikleri sağlamdır. Bununla birlikte, akıllı sözleşmeler esnek olmayabilir ve beklenmedik durumlara adapte olmakta zorlanabilirler. Ayrıca, kurulumları bazıları için bir engel olabilecek özel kodlama becerilerini gerektirir. Bu zorluklara rağmen, akıllı sözleşmeler endüstrileri dönüştürüyor.

Akıllı Sözleşmelerin Avantajları

• Görevleri otomatikleştirerek verimliliği artırın, zaman ve para tasarrufu sağlayın.
• Aynı bilgiye tüm tarafların erişimini sağlayarak şeffaflığı artırın ve anlaşmazlıkları azaltın.
• Kodlara güvenerek insan hatalarını ortadan kaldırarak hataları azaltın.
• Kriptografik korumalarla güvenliği güçlendirerek, müdahalenin zorlaşmasını sağlayın.

Akıllı Sözleşmelerin Dezavantajları

• Katı doğaları nedeniyle beklenmedik durumlara uyum sağlama esnekliği eksikliği.
• Yaygın benimsenmeyi sınırlayan özel kodlama bilgisi gerektirir.

Ethereum Akıllı Sözleşmeler için Biçimsel Doğrulama Araçları

Kaynak: Calibraint

Formal şartnameler oluşturmak için specifikasyon dilleri

• Act: Act, kullanıcıların depolama güncellemelerini, ön ve son koşulları ve sözleşme değişmezliklerini tanımlamalarını sağlar. Aracı seti, Coq, SMT çözücüleri veya hevm kullanarak çeşitli özellikleri doğrulayabilen kanıt arka uçlarını içerir.

GitHub

Belgeleme

• Scribble: Scribble, özellik dilinde yazılmış kod açıklamalarını belirli bir doğrulama yapacak ifadelere dönüştürür.

Belgeleme

• Dafny: Dafny, kodun doğruluğunu düşünmeye ve onaylamaya yardımcı olmak için yüksek düzeyli açıklamalar kullanarak doğrulama için tasarlanmış bir programlama dilidir.

GitHub (İngilizce)

Doğruluğu kontrol etmek için program doğrulayıcıları

• Certora Prover: Certora Prover, akıllı sözleşme kodlarının doğruluğunu kontrol eden otomatik bir biçimsel doğrulama aracıdır. Sınırlamaların tespiti, Certora Doğrulama Dili (CVL) kullanılarak oluşturulan özellikler aracılığıyla statik analiz ve kısıtlama çözme tekniklerinin bir karışımıyla gerçekleştirilir.

Web sitesi

Belgeleme

• Solidity SMTChecker: Solidity’nin SMTChecker’ı, Tatmin Edilebilirlik Modülü Teorileri (SMT) ve Horn çözümleme kullanan entegre bir model doğrulayıcıdır. Derleme sırasında bir sözleşmenin kaynak kodunun belirtilerle uyumlu olup olmadığını doğrular ve güvenlik özelliği ihlallerini kontrol eder.

GitHub

• Solc-verify: Solc-verify, Solidity derleyicisinin geliştirilmiş bir sürümüdür ve Solidity kodunun otomatik biçimsel doğrulamasını, açıklamalar ve modüler program doğrulaması aracılığıyla mümkün kılar.

GitHub

• KEVM: KEVM, Ethereum Sanal Makinesi'ni resmi olarak temsil eder(EVM)K çerçevesi kullanılarak oluşturulmuştur. Yürütülebilir ve ulaşılabilirlik mantığı aracılığıyla belirli özellikle ilgili iddiaları doğrulayabilir.

GitHub

Belgeleme

Teorem kanıtlama için mantıksal çerçeveler

• Isabelle: Isabelle/HOL, kullanıcıların matematiksel formülleri formel bir dilde ifade etmelerine ve bunları kanıtlamak için araçlar sağlayan bir kanıt asistanıdır. Temel kullanımı, özellikle bilgisayar donanımı ve yazılımının doğruluğunu ve programlama dillerinin ve protokollerinin özelliklerini doğrulamak için matematiksel kanıtları biçimlendirmektir.

GitHub

Belge

• Coq - Coq, teoremleri tanımlamanıza ve etkileşimli bir süreç aracılığıyla doğruluklarının makine tarafından kontrol edilen kanıtlarını oluşturmanıza olanak tanıyan etkileşimli bir teorem kanıtlayıcıdır.

GitHub

Belgeleme

Akıllı sözleşmelerde zayıf desenleri tespit etmek için sembolik yürütme tabanlı araçlar

• Manticore - Sembolik yürütme kullanarak EVM bytecode'ı analiz eden bir araç.

GitHub

Belgeleme

• Hevm - hevm, EVM bytecode'nin eşdeğerliğini kontrol eden sembolik bir yürütme motorudur.

GitHub

• Mythril - Ethereum akıllı sözleşmelerindeki güvenlik açıklarını bulmak için kullanılan bir sembolik yürütme aracı.

GitHub

Belgeleme

Sonuç

Akıllı sözleşmeleri korumak için, biçimsel doğrulamayı manuel denetimle birleştirmek, güvenliklerinin kapsamlı bir değerlendirmesi için önemlidir. Biçimsel doğrulama kaynak yoğun olabilir, ancak yüksek bahis veya önemli risk içeren sözleşmeler için değerli bir yatırımdır. Akıllı sözleşmeler sadece trend bir kavramdan daha fazlasıdır; küresel işletme operasyonlarını dönüştürüyorlar ve zorluklarla birlikte geliyor olsalar da, verimliliği artırmak, hataları minimize etmek ve güvenliği güçlendirmek için eşsiz yetenekleri göz ardı edilemez. Akıllı sözleşmeler, işlemleri basitleştirmek ve dijital işlemlerde güveni artırmak için büyük potansiyele sahiptir. Bu amaçla, bugün bu teknolojiyi benimseyen organizasyonlar, şeffaflığı ve güvenilirliği önceliklendiren bir gelecekte başarılı olacaklar.