Informasi Umum

Verifikasi Runtime adalah metode analisis dan eksekusi sistem komputasi yang dirancang untuk mengekstrak informasi dari sistem yang berjalan untuk mendeteksi dan mungkin menanggapi apakah perilaku yang diamati memenuhi atau melanggar atribut tertentu. Teknik ini dapat digunakan untuk berbagai tujuan, seperti pemantauan kebijakan keamanan atau keamanan, debugging, pengujian, verifikasi, validasi, analisis kinerja, failsafe, modifikasi perilaku, dan banyak lagi. Ini menghindari kompleksitas teknik verifikasi formal tradisional dengan menganalisis sejumlah kecil lintasan eksekusi dan bekerja langsung dengan sistem yang sebenarnya.

Runtime Verification Inc. adalah perusahaan yang berfokus pada audit keamanan mesin virtual dan kontrak pintar menggunakan teknik verifikasi runtime. Layanan yang mereka berikan meliputi tinjauan desain, tinjauan kode, audit, dan verifikasi formal kontrak dan protokol pintar.

Produk apa yang saat ini ditawarkan oleh Runtime Verification Inc.?

Runtime Verification Inc. saat ini sedang mengembangkan tiga produk inti: RV-Predict adalah alat analisis runtime prediktif yang berfokus pada pendeteksian kesalahan bersamaan secara otomatis dalam suatu program. RV-Monitor adalah metodologi pengembangan dan alat pembangkitan perpustakaan yang memungkinkan properti yang dipilih pengguna dipantau dan dieksekusi pada runtime. RV-Match adalah alat yang memungkinkan validasi runtime lengkap dilakukan secara simbolis pada semua jalur program yang mungkin, sehingga membuktikan bahwa properti tertentu benar untuk semua kemungkinan eksekusi program tertentu.

Kapan dan mengapa RV-Predict harus digunakan?

Kapan pun kebenaran concurrency penting untuk aplikasi multi-threaded, RV-Predict harus digunakan. RV-Predict dapat secara efisien dan mulus mendeteksi masalah konkurensi dan perselisihan data dalam suatu program, sangat mudah di jalankan, dan umumnya tidak memerlukan konfigurasi apa pun. RV-Predict juga menggunakan kemampuan prediksi unik untuk mendeteksi kemungkinan pertengkaran, bahkan jika itu tidak terjadi dalam jejak eksekusi catatan RV-Predict.

Kapan dan mengapa RV-Monitor harus digunakan?

RV-Monitor memungkinkan untuk memantau aplikasi atau sistem yang kompleks dan melakukan properti eksekusi jejak pada mereka. RV-Monitor harus digunakan selama ada spesifikasi untuk mengelola pengembangan program, dan kepatuhan terhadap spesifikasi ini adalah fitur penting dari perangkat lunak. RV-Monitor juga dapat digunakan untuk memantau kepatuhan terhadap API umum, termasuk Android dan Java API.

Kapan dan mengapa RV-Match harus digunakan?

RV-Monitor dapat memverifikasi dan menegakkan kepatuhan terhadap sifat-sifat tertentu dari eksekusi program tertentu, sementara RV-Match dapat membuktikan kebenaran suatu program pada saat runtime, sehingga menganalisis jejak eksekusi pada semua kemungkinan jalur eksekusi dan semua kemungkinan input. RV-Match memberikan jaminan kebenaran yang kuat, mensimulasikan eksekusi secara simbolis menggunakan semantik bahasa target yang ditentukan secara formal. Ketika jaminan validasi formal yang kuat diperlukan, RV-Match harus digunakan, dan juga dapat digunakan dengan RV-Monitor untuk menghilangkan pemantauan area yang dapat membuktikan bahwa properti tidak pernah dilanggar.

Lisensi mana yang dicakup oleh produk Runtime Verification Inc.?

Proyek yang dikembangkan oleh RV terbagi dalam dua kategori: produk berpemilik dan yang dilisensikan di bawah lisensi terbuka (sebagai bagian dari ekosistem sumber terbuka RV).

Produk berpemilik mencakup semua produk yang tidak dilisensikan secara tegas di bawah lisensi terbuka dan digunakan untuk evaluasi dan tujuan akademik / non-komersial saja. Karya turunan tidak boleh dibuat menggunakan produk RV berpemilik tanpa izin sebelumnya, dan RV berhak atas produk berpemilik. Produk eksklusif tidak boleh direkayasa balik dengan cara apa pun.

Blockchain Project Audit

Verifikasi Runtime telah terlibat dalam audit beberapa proyek blockchain, termasuk namun tidak terbatas padahal-hal berikut:

- Audit Keamanan Kontrak Cerdas: Mereka menyediakan audit kontrak berbiaya rendah seperti ERC-20, ERC-721, ERC-4626, dll.

- Audit Keamanan Protokol: Termasuk protokol untuk operasi terkait pinjaman.

- Verifikasi formal: Menyediakan alat verifikasi dan pengembang formal sumber terbuka untuk mengurangi biaya audit dan memungkinkan verifikasi formal berkelanjutan.

Audit mereka biasanya mencakup ulasan manual dan verifikasi formal untuk memastikan keamanan dan keandalan kode tingkat tinggi.