Menurut pendapat saya, di sektor Internet berbahasa Rusia, topik verifikasi formal tidak cukup dibahas, dan khususnya contoh-contoh sederhana dan jelas masih kurang.
Saya akan memberikan contoh seperti itu dari sumber asing, dan menambahkan solusi saya sendiri untuk masalah transportasi serigala, kambing, dan kol yang terkenal ke sisi lain sungai.
Tetapi pertama-tama, saya akan menjelaskan secara singkat apa itu verifikasi formal dan mengapa diperlukan.
Verifikasi formal biasanya berarti memeriksa satu program atau algoritma menggunakan yang lain.
Ini diperlukan untuk memastikan bahwa perilaku program seperti yang diharapkan, dan juga untuk memastikan keamanannya.
Verifikasi formal adalah alat paling ampuh untuk menemukan dan menghilangkan kerentanan: memungkinkan Anda menemukan semua lubang dan bug yang ada dalam program, atau untuk membuktikan bahwa mereka tidak ada.
Perlu dicatat bahwa dalam beberapa kasus ini tidak mungkin, seperti dalam masalah 8 ratu dengan lebar papan 1000 sel: semuanya tergantung pada kompleksitas algoritmik atau masalah penghentian.
Namun, dalam hal apa pun, salah satu dari tiga jawaban akan diterima: programnya benar, salah, atau jawabannya tidak dapat dihitung.
Jika tidak mungkin menemukan jawaban, sering kali mungkin untuk memproses tempat yang tidak jelas dalam program, mengurangi kompleksitas algoritme mereka untuk mendapatkan jawaban yang spesifik, ya atau tidak.
Dan verifikasi formal digunakan, misalnya, dalam sistem operasi Windows kernel dan Darpa drone, untuk memberikan tingkat perlindungan maksimum.
Kami akan menggunakan Z3Prover, alat yang sangat kuat untuk pembuktian teorema dan penyelesaian persamaan secara otomatis.
Selain itu, Z3 memecahkan persamaan dengan tepat, dan tidak memilih nilainya dengan gaya kasar.
Ini berarti bahwa ia dapat menemukan jawabannya, bahkan dalam kasus di mana kombinasi opsi input dan 10 ^ 100.
Tapi ini hanya sekitar selusin argumen input tipe Integer, dan ini sering ditemukan dalam praktik.
Masalah 8 ratu (Diambil dari
manual Bahasa Inggris).
# We know each queen must be in a different row. # So, we represent each queen by a single integer: the column position Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ] # Each queen is in a column {1, ... 8 } val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ] # At most one queen per column col_c = [ Distinct(Q) ] # Diagonal constraint diag_c = [ If(i == j, True, And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)) for i in range(8) for j in range(i) ] solve(val_c + col_c + diag_c)
Menjalankan Z3, kami mendapatkan solusinya:
[Q_5 = 1, Q_8 = 7, Q_3 = 8, Q_2 = 2, Q_6 = 3, Q_4 = 6, Q_7 = 5, Q_1 = 4]
Masalah ratu sebanding dengan program yang mengambil dalam koordinat 8 ratu dan menampilkan jawabannya jika ratu saling mengalahkan.
Jika kita menyelesaikan program seperti itu menggunakan verifikasi formal, kemudian dibandingkan dengan tugas, kita hanya perlu mengambil langkah lain dalam bentuk mengubah kode program menjadi persamaan: itu pada dasarnya akan menjadi identik dengan kita (tentu saja, jika program itu ditulis dengan benar).
Hampir hal yang sama akan terjadi ketika mencari kerentanan: kita hanya mengatur kondisi keluaran yang kita butuhkan, misalnya, kata sandi admin, mengubah sumber atau kode yang diurai menjadi persamaan yang kompatibel dengan verifikasi, dan kemudian kita mendapatkan jawaban data apa yang perlu input untuk mencapai tujuan.
Menurut pendapat saya, masalah serigala, kambing dan kubis bahkan lebih menarik, karena banyak (7) langkah sudah diperlukan untuk menyelesaikannya.
Jika tugas ratu sebanding dengan opsi ketika Anda dapat menembus server menggunakan satu permintaan GET atau POST, maka serigala, kambing dan kubis menunjukkan contoh dari kategori yang jauh lebih kompleks dan tersebar luas di mana hanya beberapa permintaan yang dapat dicapai.
Ini sebanding, misalnya, dengan skenario di mana Anda perlu menemukan injeksi SQL, menulis file melalui itu, kemudian meningkatkan hak-hak Anda dan hanya kemudian mendapatkan kata sandi.
Kondisi masalah dan solusinyaPetani perlu mengangkut serigala, kambing, dan kubis di seberang sungai. Petani memiliki perahu di mana hanya satu benda yang bisa muat, kecuali petani sendiri. Serigala akan memakan kambing, dan kambing akan memakan kubis jika petani membiarkannya tanpa pengawasan.
Solusinya adalah pada langkah 4, peternak harus mengambil kambing kembali.
Sekarang mari kita mulai solusinya secara terprogram.
Kami menunjuk petani, serigala, kambing dan kubis sebagai 4 variabel, yang mengambil nilai hanya 0 atau 1. Nol berarti bahwa mereka berada di tepi kiri, dan satu berarti di kanan.
import json from z3 import * s = Solver() Num= 8 Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ] Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ] Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ] Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ] # Each creature can be only on left (0) or right side (1) on every state HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ] WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ] GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ] CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ] Side = HumanSide+WolfSide+GoatSide+CabbageSide
Jumlah adalah jumlah langkah yang perlu dipecahkan. Setiap langkah adalah keadaan sungai, kapal, dan semua entitas.
Untuk saat ini, pilih secara acak dan dengan margin, ambil 10.
Setiap entitas direpresentasikan dalam 10 salinan - ini nilainya pada masing-masing 10 langkah.
Sekarang kita mengatur kondisi untuk memulai dan menyelesaikan.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ] Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Kemudian kita mengatur kondisi di mana serigala makan kambing, atau kubis kambing, sebagai batasan dalam persamaan.
(Di hadapan petani, agresi tidak dimungkinkan)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Dan akhirnya, kami menanyakan semua tindakan yang mungkin dilakukan petani saat pindah ke sana atau kembali.
Dia bisa membawa serigala, kambing atau kubis bersamanya, atau tidak membawa siapa pun, atau bahkan tidak pergi ke mana pun.
Tentu saja, tidak ada yang bisa menyeberang tanpa petani.
Ini akan diekspresikan oleh fakta bahwa setiap keadaan sungai, kapal, dan entitas berikutnya dapat berbeda dari yang sebelumnya hanya dengan cara yang sangat terbatas.
Tidak lebih dari 2 bit, dan dengan banyak batasan lain, karena petani hanya dapat mengangkut satu entitas pada satu waktu dan tidak semua dapat dibiarkan bersama.
Travel = [ Or( And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]), And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]), And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
Jalankan solusinya.
solve(Side + Start + Finish + Safe + Travel)
Dan kami mendapatkan jawabannya!
Z3 menemukan serangkaian kondisi yang konsisten dan memuaskan.
Semacam pemeran ruang-waktu empat dimensi.
Mari kita lihat apa yang terjadi.
Kami melihat bahwa pada akhirnya semua orang menyeberang, hanya pada awalnya petani kami memutuskan untuk bersantai, dan tidak berenang di mana pun dalam 2 langkah pertama.
Human_2 = 0 Human_3 = 0
Ini menunjukkan bahwa jumlah negara yang telah kita pilih berlebihan, dan 8 akan cukup.
Dalam kasus kami, petani melakukan ini: mulai, istirahat, istirahat, menyeberangi kambing, menyeberang kembali, menyeberangi kubis, kembali dengan kambing, melintasi serigala, kembali sendirian, mengantarkan kembali kambing.
Namun pada akhirnya, masalahnya terpecahkan.
#. Human_1 = 0 Wolf_1 = 0 Goat_1 = 0 Cabbage_1 = 0 # . Human_2 = 0 Wolf_2 = 0 Goat_2 = 0 Cabbage_2 = 0 # . Human_3 = 0 Wolf_3 = 0 Goat_3 = 0 Cabbage_3 = 0 # . Human_4 = 1 Wolf_4 = 0 Goat_4 = 1 Cabbage_4 = 0 # . Human_5 = 0 Wolf_5 = 0 Goat_5 = 1 Cabbage_5 = 0 # . Human_6 = 1 Wolf_6 = 0 Cabbage_6 = 1 Goat_6 = 1 # : . Human_7 = 0 Wolf_7 = 0 Goat_7 = 0 Cabbage_7 = 1 # , . Human_8 = 1 Wolf_8 = 1 Goat_8 = 0 Cabbage_8 = 1 # . Human_9 = 0 Wolf_9 = 1 Goat_9 = 0 Cabbage_9 = 1 # . Human_10 = 1 Wolf_10 = 1 Goat_10 = 1 Cabbage_10 = 1
Sekarang mari kita coba untuk mengubah kondisi dan membuktikan bahwa tidak ada solusi.
Untuk melakukan ini, kita akan memberkahi serigala kita dengan herbivora, dan dia ingin memakan kol.
Ini dapat dibandingkan dengan kasus di mana tujuan kami adalah untuk melindungi aplikasi dan kami perlu memastikan bahwa tidak ada celah.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3 memberi kami jawaban berikut:
no solution
Ini berarti tidak ada solusi.
Dengan demikian, secara program kami telah membuktikan ketidakmungkinan melintasi serigala omnivora, tanpa kerugian bagi petani.
Jika audiens menemukan topik ini menarik, maka dalam artikel mendatang saya akan memberi tahu Anda cara mengubah program atau fungsi biasa menjadi persamaan yang kompatibel dengan metode formal dan menyelesaikannya, sehingga mengungkapkan semua skenario dan kerentanan yang sah. Pertama, pada tugas yang sama, tetapi sudah disajikan dalam bentuk program, dan kemudian secara bertahap menyulitkan dan beralih ke contoh yang relevan dari dunia pengembangan perangkat lunak.
Artikel berikut siap:
Membuat sistem verifikasi formal dari awal: Kami menulis karakter VM dalam PHP dan PythonDi dalamnya, saya beralih dari verifikasi formal tugas ke program, dan menjelaskan
cara mengubahnya menjadi sistem aturan formal secara otomatis.