Bana göre İnternet'in Rusça sektöründe resmi doğrulama konusu yeterince ele alınmıyor ve özellikle basit ve net örneklerin eksikliği var.
Yabancı bir kaynaktan örnek verip, çok iyi bilinen bir kurdu, bir keçiyi ve bir lahanayı nehrin karşı yakasına geçirme sorununa kendi çözümümü ekleyeceğim.
Ancak önce resmi doğrulamanın ne olduğunu ve neden gerekli olduğunu kısaca anlatacağım.
Resmi doğrulama genellikle bir programı veya algoritmayı diğerini kullanarak kontrol etmek anlamına gelir.
Bu, programın beklendiği gibi davranmasını sağlamak ve aynı zamanda güvenliğini sağlamak için gereklidir.
Resmi doğrulama, güvenlik açıklarını bulmanın ve ortadan kaldırmanın en güçlü yoludur: bir programdaki mevcut tüm açıkları ve hataları bulmanıza veya bunların var olmadığını kanıtlamanıza olanak tanır.
8 kare genişliğindeki 1000 vezir probleminde olduğu gibi bazı durumlarda bunun imkansız olduğunu belirtmekte fayda var: her şey algoritmik karmaşıklığa veya durma problemine bağlı.
Ancak her durumda üç cevaptan biri alınacaktır: program doğrudur, yanlıştır veya cevabı hesaplamak mümkün değildir.
Bir cevap bulmak imkansızsa, belirli bir evet veya hayır cevabı elde etmek için programın belirsiz kısımlarını yeniden çalışmak, algoritmik karmaşıklığı azaltmak genellikle mümkündür.
Maksimum koruma düzeyini sağlamak için örneğin Windows çekirdeği ve Darpa drone işletim sistemlerinde resmi doğrulama kullanılır.
Otomatik teorem ispatı ve denklem çözümü için çok güçlü bir araç olan Z3Prover'ı kullanacağız.
Üstelik Z3 denklemleri çözer ve değerlerini kaba kuvvet kullanarak seçmez.
Bu, 10^100 giriş seçeneği kombinasyonunun olduğu durumlarda bile cevabı bulabileceği anlamına gelir.
Ancak bu yalnızca Tamsayı tipindeki bir düzine giriş argümanından ibarettir ve bununla pratikte sıklıkla karşılaşılır.
8 kraliçe ile ilgili problem (İngilizce'den alınmıştır) ).
# 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)
Z3'ü çalıştırarak çözüme ulaşıyoruz:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Kraliçe problemi, girdi olarak 8 kraliçenin koordinatlarını alan ve kraliçelerin birbirini yenip yenmediğinin cevabını veren bir programla karşılaştırılabilir.
Böyle bir programı resmi doğrulama kullanarak çözecek olsaydık, o zaman problemle karşılaştırıldığında, program kodunu bir denkleme dönüştürme biçiminde bir adım daha atmamız gerekecekti: bizimkiyle esasen aynı olduğu ortaya çıkacaktı ( tabii ki program doğru yazılmışsa).
Güvenlik açıklarının aranması durumunda da neredeyse aynı şey olacaktır: yalnızca ihtiyacımız olan çıktı koşullarını (örneğin, yönetici şifresi) belirleriz, kaynak veya derlenmemiş kodu doğrulamayla uyumlu denklemlere dönüştürürüz ve ardından ne olduğuna dair bir yanıt alırız. Hedefe ulaşmak için verilerin girdi olarak sağlanması gerekir.
Bana göre kurt, keçi ve lahana ile ilgili sorun daha da ilginç çünkü bunu çözmek zaten birçok (7) adım gerektiriyor.
Kraliçe sorunu, tek bir GET veya POST isteği kullanarak bir sunucuya girebildiğiniz durumla karşılaştırılabilirse, o zaman kurt, keçi ve lahana çok daha karmaşık ve yaygın bir kategoriden, hedefe ancak ulaşılabilen bir örnek gösterir. çeşitli isteklerle.
Bu, örneğin bir SQL enjeksiyonu bulmanız, bunun üzerinden bir dosya yazmanız, ardından haklarınızı yükseltmeniz ve ancak bundan sonra bir şifre almanız gereken bir senaryoya benzetilebilir.
Sorunun koşulları ve çözümüÇiftçinin nehrin karşısına bir kurt, bir keçi ve lahana taşıması gerekiyor. Çiftçinin, kendisi dışında yalnızca tek bir nesneyi barındırabilen bir teknesi vardır. Çiftçi onları başıboş bırakırsa kurt keçiyi, keçi de lahanayı yiyecektir.
Çözüm, 4. adımda çiftçinin keçiyi geri alması gerekmesidir.
Şimdi programlı olarak çözmeye başlayalım.
Çiftçi, kurt, keçi ve lahanayı sadece 4 veya 0 değerini alan 1 değişken olarak gösterelim. Sıfır, sol tarafta, bir ise sağ tarafta oldukları anlamına gelir.
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
Num, çözmek için gereken adım sayısıdır. Her adım nehrin, teknenin ve tüm varlıkların durumunu temsil eder.
Şimdilik rastgele seçelim ve bir farkla 10 alalım.
Her varlık 10 kopya halinde temsil edilir; bu, 10 adımın her birindeki değeridir.
Şimdi başlangıç ve bitiş koşullarını belirleyelim.
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 ]
Daha sonra denklemdeki kısıtlamalar olarak kurdun keçiyi yediği veya keçinin lahanayı yediği koşulları belirleriz.
(Bir çiftçinin varlığında saldırganlık imkansızdır)
# 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) ]
Ve son olarak çiftçinin oradan geçerken veya geri dönerken yapabileceği tüm olası eylemleri tanımlayacağız.
Ya yanına bir kurt, bir keçi ya da bir lahana alabilir, ya kimseyi götüremez ya da hiçbir yere yelken açamaz.
Elbette çiftçi olmadan kimse geçemez.
Bu, nehrin, teknenin ve varlıkların sonraki her durumunun bir öncekinden yalnızca kesin olarak sınırlı bir şekilde farklı olabileceği gerçeğiyle ifade edilecektir.
Çiftçi aynı anda yalnızca tek bir varlığı taşıyabildiğinden ve hepsi bir arada bırakılamadığından, 2 bitten fazla olamaz ve diğer birçok sınırla birlikte.
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) ]
Çözümü çalıştıralım.
solve(Side + Start + Finish + Safe + Travel)
Ve cevabı alıyoruz!
Z3, tüm koşulları karşılayan tutarlı bir durum kümesi buldu.
Bir tür dört boyutlu uzay-zaman dökümü.
Ne olduğunu çözelim.
Sonunda herkesin karşıya geçtiğini görüyoruz, ancak çiftçimiz ilk başta dinlenmeye karar verdi ve ilk 2 adımda hiçbir yerde yüzmüyor.
Human_2 = 0
Human_3 = 0
Bu da seçtiğimiz eyalet sayısının fazla olduğunu, 8'in oldukça yeterli olacağını gösteriyor.
Bizim durumumuzda çiftçi şunu yaptı: başla, dinlen, dinlen, keçiyi geç, geri geç, lahanayı geç, keçiyle dön, kurdu geç, tek başına geri dön, keçiyi yeniden teslim et.
Ama sonunda sorun çözüldü.
#Старт.
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
Şimdi koşulları değiştirmeye çalışalım ve hiçbir çözümün olmadığını kanıtlayalım.
Bunu yapmak için kurtumuza otçul vereceğiz ve o da lahana yemek isteyecek.
Bu, amacımızın uygulamayı güvence altına almak olduğu ve hiçbir boşluk olmadığından emin olmamız gereken durumla karşılaştırılabilir.
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 bize şu yanıtı verdi:
no solution
Bu aslında hiçbir çözümün olmadığı anlamına gelir.
Böylece, çiftçi için kayıpsız bir omnivor kurtla melezlemenin imkansızlığını programlı olarak kanıtladık.
Eğer izleyici bu konuyu ilginç buluyorsa, gelecek yazılarda size sıradan bir programı veya işlevi resmi yöntemlerle uyumlu bir denklem haline nasıl dönüştüreceğinizi ve çözeceğinizi, böylece hem tüm meşru senaryoları hem de güvenlik açıklarını nasıl ortaya çıkaracağınızı anlatacağım. İlk önce aynı görev üzerinde, ancak bir program biçiminde sunuluyor ve ardından yavaş yavaş karmaşıklaştırılıyor ve yazılım geliştirme dünyasından güncel örneklere geçiliyor.
Bir sonraki makale zaten hazır:
İçinde sorunların resmi olarak doğrulanmasından programlara geçiyorum ve açıklıyorum
otomatik olarak resmi kural sistemlerine nasıl dönüştürülebilirler?
Kaynak: habr.com