Menurut pendapat saya, di sektor Internet berbahasa Rusia, topik verifikasi formal kurang dibahas, dan contoh-contoh yang sederhana dan jelas sangat kurang.
Saya akan memberikan contoh dari sumber asing, dan menambahkan solusi saya sendiri pada masalah terkenal yaitu menyeberangi serigala, kambing, dan kubis ke seberang sungai.
Namun pertama-tama, saya akan menjelaskan secara singkat apa itu verifikasi formal dan mengapa verifikasi itu diperlukan.
Verifikasi formal biasanya berarti memeriksa satu program atau algoritma menggunakan program atau algoritma lain.
Hal ini diperlukan untuk memastikan bahwa program berperilaku seperti yang diharapkan dan juga untuk menjamin keamanannya.
Verifikasi formal adalah cara paling ampuh untuk menemukan dan menghilangkan kerentanan: verifikasi ini memungkinkan Anda menemukan semua lubang dan bug yang ada dalam suatu program, atau membuktikan bahwa mereka tidak ada.
Perlu dicatat bahwa dalam beberapa kasus hal ini tidak mungkin, seperti dalam masalah 8 ratu dengan lebar papan 1000 kotak: semuanya bergantung pada kompleksitas algoritmik atau masalah penghentian.
Namun, bagaimanapun juga, salah satu dari tiga jawaban akan diterima: programnya benar, salah, atau jawabannya tidak dapat dihitung.
Jika tidak mungkin menemukan jawaban, seringkali mungkin untuk mengerjakan ulang bagian program yang tidak jelas, mengurangi kompleksitas algoritmiknya, untuk mendapatkan jawaban ya atau tidak yang spesifik.
Dan verifikasi formal digunakan, misalnya, pada kernel Windows dan sistem operasi drone Darpa, untuk memastikan tingkat perlindungan maksimal.
Kami akan menggunakan Z3Prover, alat yang sangat ampuh untuk pembuktian teorema otomatis dan penyelesaian persamaan.
Selain itu, Z3 menyelesaikan persamaan, dan tidak memilih nilainya menggunakan kekerasan.
Artinya, ia dapat menemukan jawabannya, meskipun terdapat 10^100 kombinasi opsi masukan.
Namun ini hanya sekitar selusin argumen masukan bertipe Integer, dan ini sering dijumpai dalam praktik.
Soal tentang 8 ratu (Diambil dari 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 dapat dibandingkan dengan sebuah program yang mengambil masukan koordinat 8 ratu dan mengeluarkan jawaban apakah ratu saling mengalahkan.
Jika kita menyelesaikan program seperti itu dengan menggunakan verifikasi formal, maka dibandingkan dengan masalahnya, kita hanya perlu mengambil satu langkah lagi dalam bentuk mengubah kode program menjadi sebuah persamaan: kode tersebut pada dasarnya akan sama dengan kita ( tentu saja, jika programnya ditulis dengan benar).
Hal yang hampir sama akan terjadi ketika mencari kerentanan: kita cukup mengatur kondisi keluaran yang kita perlukan, misalnya kata sandi admin, mengubah kode sumber atau kode yang didekompilasi menjadi persamaan yang kompatibel dengan verifikasi, dan kemudian mendapatkan jawaban tentang apa data perlu diberikan sebagai masukan untuk mencapai tujuan.
Menurut saya, masalah serigala, kambing, dan kubis ini lebih menarik lagi, karena penyelesaiannya sudah membutuhkan banyak (7) langkah.
Jika masalah ratu sebanding dengan kasus di mana Anda dapat menembus server menggunakan satu permintaan GET atau POST, maka serigala, kambing, dan kubis menunjukkan contoh dari kategori yang jauh lebih kompleks dan luas, di mana tujuannya hanya dapat dicapai oleh beberapa permintaan.
Ini sebanding, misalnya, dengan skenario di mana Anda perlu menemukan injeksi SQL, menulis file melaluinya, lalu meningkatkan hak Anda dan baru kemudian mendapatkan kata sandi.
Kondisi masalah dan solusinyaPetani perlu mengangkut serigala, kambing, dan kubis menyeberangi sungai. Petani mempunyai perahu yang hanya mampu menampung satu benda saja, selain petani itu sendiri. Serigala akan memakan kambing dan kambing akan memakan kubis jika petani meninggalkannya tanpa pengawasan.
Solusinya adalah pada langkah 4 peternak harus mengambil kembali kambingnya.
Sekarang mari kita mulai menyelesaikannya secara terprogram.
Mari kita nyatakan petani, serigala, kambing, dan kubis sebagai 4 variabel yang hanya bernilai 0 atau 1. Nol berarti berada di tepi kiri, dan satu berarti berada di tepi 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
Bil adalah jumlah langkah yang diperlukan untuk menyelesaikannya. Setiap langkah mewakili keadaan sungai, perahu, dan seluruh entitas.
Untuk saat ini, mari kita pilih secara acak dan dengan margin, ambil 10.
Setiap entitas diwakili dalam 10 salinan - ini adalah nilainya pada masing-masing 10 langkah.
Sekarang mari kita atur kondisi untuk awal dan akhir.
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 ]
Lalu kami menetapkan kondisi di mana serigala memakan kambing, atau kambing memakan kubis, sebagai batasan dalam persamaan tersebut.
(Di hadapan seorang petani, agresi tidak mungkin dilakukan)
# 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 terakhir, kami akan mendefinisikan semua tindakan yang mungkin dilakukan petani saat menyeberang bolak-balik.
Dia bisa membawa serigala, kambing, atau kubis, atau tidak membawa siapa pun, atau tidak berlayar ke mana pun sama sekali.
Tentu saja tidak ada seorang pun yang bisa menyeberang tanpa seorang petani.
Hal ini akan diungkapkan oleh fakta bahwa setiap keadaan sungai, perahu, dan entitas selanjutnya dapat berbeda dari keadaan sebelumnya hanya dalam cara yang sangat terbatas.
Tidak lebih dari 2 bit, dan dengan banyak batasan lainnya, karena petani hanya dapat mengangkut satu entitas dalam satu waktu dan tidak semuanya 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) ]
Mari kita jalankan solusinya.
solve(Side + Start + Finish + Safe + Travel)
Dan kami mendapatkan jawabannya!
Z3 menemukan serangkaian keadaan konsisten yang memenuhi semua kondisi.
Semacam pemeran ruang-waktu empat dimensi.
Mari kita cari tahu apa yang terjadi.
Kami melihat bahwa pada akhirnya semua orang menyeberang, hanya saja pada awalnya petani kami memutuskan untuk beristirahat, dan pada 2 langkah pertama dia tidak berenang kemana-mana.
Human_2 = 0
Human_3 = 0
Hal ini menunjukkan bahwa jumlah negara bagian yang kita pilih berlebihan, dan 8 negara bagian sudah cukup.
Dalam kasus kami, petani melakukan ini: memulai, istirahat, istirahat, menyilangkan kambing, menyilangkan punggung, menyilangkan kubis, kembali dengan kambing, menyilangkan serigala, kembali sendirian, mengantarkan kembali kambing tersebut.
Namun pada akhirnya masalah tersebut terselesaikan.
#Π‘ΡΠ°ΡΡ.
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 mengubah kondisi dan membuktikan bahwa tidak ada solusi.
Untuk melakukan ini, kami akan memberikan serigala kami herbivora, dan dia ingin makan kubis.
Hal ini dapat dibandingkan dengan kasus di mana tujuan kita adalah mengamankan aplikasi dan kita perlu memastikan 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 respons berikut:
no solution
Artinya sebenarnya tidak ada solusi.
Jadi, kami secara terprogram membuktikan ketidakmungkinan persilangan dengan serigala omnivora tanpa kerugian bagi petani.
Jika audiens menganggap topik ini menarik, maka di artikel mendatang saya akan memberi tahu Anda cara mengubah program atau fungsi biasa menjadi persamaan yang kompatibel dengan metode formal, dan menyelesaikannya, sehingga mengungkap semua skenario dan kerentanan yang sah. Pertama, pada tugas yang sama, tetapi disajikan dalam bentuk program, kemudian secara bertahap memperumitnya dan beralih ke contoh-contoh terkini dari dunia pengembangan perangkat lunak.
Artikel selanjutnya sudah siap:
Di dalamnya saya beralih dari verifikasi formal masalah ke program, dan menjelaskannya
bagaimana mereka dapat diubah menjadi sistem aturan formal secara otomatis.
Sumber: www.habr.com