Güvenlik, test ve biçimsel doğrulama

Biz, kritik sistemlerin güvenliğini ve doğruluğunu sağlamak için titiz araçlar geliştiren bir araştırma ve geliştirme şirketi olan Runtime Verification'ız. Ekibimiz, K Framework'te yazılmış, Ethereum Sanal Makinesi'nin (EVM) en eksiksiz ve savaş testinden geçmiş resmi anlambilimi olan KEVM'yi geliştirdi. KEVM sadece bir spesifikasyon değildir; akıllı sözleşmeler hakkında sembolik olarak akıl yürütmek, uygunluk testleri çalıştırmak, gaz kullanımını analiz etmek, programlarda hata ayıklamak ve doğruluk özelliklerini resmi olarak doğrulamak için kullanılabilen yürütülebilir bir spesifikasyondur. Tüm Ethereum test paketini geçer ve hem Solidity hem de Vyper'daki ERC-20 token'ları dahil olmak üzere yüksek değerli sözleşmeleri doğrulamak için kullanılır. Yakın zamanda Pectra yükseltmesini desteklemek için anlambilimi güncelledik. KEVM, Optimism, Ethereum Foundation, Lido, Uniswap dahil olmak üzere EVM ekosistemindeki önde gelen ekiplerin yanı sıra daha geniş Ethereum topluluğundaki güvenlik araştırmacıları ve denetçileri tarafından aktif olarak kullanılan Solidity için resmi doğrulama aracımız Kontrol tarafından aktif olarak kullanılmaktadır. Bu depoyu aktif olarak koruyor, Ethereum'un protokol evrimine katkıda bulunuyor ve Foundry gibi geliştirici araçlarıyla entegre oluyoruz. KEVM aracılığıyla, kanıtlanabilir derecede doğru ve güvenli akıllı sözleşme altyapısında nelerin mümkün olduğunun sınırlarını zorluyoruz.

Act, biçimsel doğrulama (formal verification) için bir akıllı sözleşme spesifikasyon dili ve araç setidir. Act spesifikasyonları, bir EVM programının olası tüm davranışlarının biçimsel, üst düzey bir açıklamasıdır. Act, spesifikasyonla ilgili özellikleri kanıtlamak için mevcut birçok genel amaçlı doğrulama aracından yararlanılmasına olanak tanır. Bu tür araçlar arasında SMT çözücüleri (cvc5, z3, bitwuzla), teorem kanıtlayıcıları (Coq) ve ekonomik analiz araçları (CheckMate, Open Games) bulunur. Act spesifikasyonlarının EVM'deki somut uygulamalara eşdeğer olduğu otomatik olarak kanıtlanabilir. Çok basit sözleşmeler için Act spesifikasyonları doğrudan EVM bayt kodundan otomatik olarak oluşturulabilir. Bu, EVM bayt kodunun üst düzey özellikleri hakkında ilkeli akıl yürütmeyi destekleyen uçtan uca bir işlem hattıdır. Hem doğruluk (ör. muhasebe değişmezleri) hem de ekonomik özellikler (ör. teşvik uyumluluğu) hakkında akıl yürütmeyi destekler. Act spesifikasyonları, mevcut genel amaçlı analiz ve doğrulama araçlarının EVM bağlamına kolayca entegre edilmesini sağlayan üst düzey bir akıllı sözleşme temsili görevi görür.

Titanoboa, Vyper akıllı sözleşmeleri için modern, entegre bir geliştirme deneyimi sağlayan bir Vyper yorumlayıcısı ve test çerçevesidir. Geliştiricilerin Vyper sözleşmelerini doğrudan Python içinde test etmelerini ve hata ayıklamalarını sağlayarak güzel geri izlemeler (tracebacks), çatallama (forking), hata ayıklama yetenekleri, pytest entegrasyonu ve kutudan çıktığı gibi fuzzing gibi özellikler sunar. Bağımsız yeteneklerinin ötesinde Titanoboa, Ape ve Moccasin gibi diğer popüler test çerçevelerinin temelini oluşturur ve Vyper ekosistemi için altyapının temel bir parçasıdır.