Keamanan, pengujian & verifikasi formal

Kami adalah Runtime Verification, sebuah perusahaan penelitian dan pengembangan yang membangun alat yang ketat untuk memastikan keamanan dan kebenaran sistem kritis. Tim kami telah mengembangkan KEVM, semantik formal Ethereum Virtual Machine (EVM) yang paling lengkap dan teruji, ditulis dalam K Framework. KEVM bukan sekadar spesifikasi, ini adalah spesifikasi yang dapat dieksekusi yang dapat digunakan untuk menalar smart contract (kontrak pintar) secara simbolis, menjalankan pengujian kesesuaian, menganalisis penggunaan gas, men-debug program, dan memverifikasi properti kebenaran secara formal. Ini melewati rangkaian pengujian Ethereum secara penuh dan digunakan untuk memverifikasi kontrak bernilai tinggi, termasuk token ERC-20 di Solidity dan Vyper. Kami baru-baru ini memperbarui semantik untuk mendukung peningkatan Pectra. KEVM secara aktif dimanfaatkan oleh Kontrol - alat verifikasi formal kami untuk Solidity, yang secara aktif digunakan oleh tim terkemuka di ekosistem EVM, termasuk Optimism, Ethereum Foundation, Lido, Uniswap, serta peneliti keamanan dan auditor di seluruh komunitas Ethereum yang lebih luas. Kami secara aktif memelihara repositori ini, berkontribusi pada evolusi protokol Ethereum, dan berintegrasi dengan perkakas pengembang seperti Foundry. Melalui KEVM, kami mendorong batas-batas dari apa yang mungkin dilakukan dalam infrastruktur smart contract yang terbukti benar dan aman.

Act adalah bahasa spesifikasi kontrak pintar dan perangkat untuk verifikasi formal. Spesifikasi Act adalah deskripsi tingkat tinggi dan formal dari semua kemungkinan perilaku program EVM. Act memungkinkan banyak alat verifikasi tujuan umum yang ada untuk dimanfaatkan guna membuktikan properti tentang spesifikasi tersebut. Alat-alat tersebut termasuk SMT solvers (cvc5, z3, bitwuzla), pembukti teorema (Coq), dan perangkat analisis ekonomi (CheckMate, Open Games). Spesifikasi Act dapat secara otomatis dibuktikan setara dengan implementasi konkret di EVM. Untuk kontrak yang sangat sederhana, spesifikasi Act dapat dihasilkan secara otomatis dari bytecode EVM. Ini adalah alur kerja ujung-ke-ujung yang mendukung penalaran berprinsip tentang properti tingkat tinggi dari bytecode EVM. Ini mendukung penalaran tentang kebenaran (misalnya invarian akuntansi) dan properti ekonomi (misalnya kompatibilitas insentif). Spesifikasi Act berfungsi sebagai representasi kontrak pintar tingkat tinggi, memungkinkan integrasi yang mudah dari analisis tujuan umum yang ada dan perangkat verifikasi ke dalam konteks EVM.

Titanoboa adalah penerjemah dan kerangka kerja pengujian Vyper yang memberikan pengalaman pengembangan modern dan terintegrasi untuk smart contract (kontrak pintar) Vyper. Ini memungkinkan pengembang untuk menguji dan men-debug kontrak Vyper secara langsung di dalam Python, menawarkan fitur seperti pelacakan balik (tracebacks) yang rapi, forking, kemampuan debugging, integrasi pytest, dan fuzzing bawaan (out-of-the box). Di luar kemampuan mandirinya, Titanoboa berfungsi sebagai fondasi untuk kerangka kerja pengujian populer lainnya seperti Ape dan Moccasin, dan merupakan bagian inti dari infrastruktur untuk ekosistem Vyper.