Миний бодлоор интернетийн орос хэл дээрх салбарт албан ёсны баталгаажуулалтын сэдэв хангалтгүй, ялангуяа энгийн бөгөөд ойлгомжтой жишээ дутагдалтай байдаг.
Чоно, ямаа, байцаа хоёрыг голын нөгөө эрэгт гатлах тухай олонд танигдсан асуудалд би гадны эх сурвалжаас жишээ татаад өөрийнхөө шийдлийг нэмье.
Гэхдээ эхлээд албан ёсны баталгаажуулалт гэж юу болох, яагаад шаардлагатай байгааг товч тайлбарлах болно.
Албан ёсны баталгаажуулалт гэдэг нь ихэвчлэн нэг програм эсвэл алгоритмыг нөгөөг ашиглан шалгахыг хэлдэг.
Энэ нь хөтөлбөр нь хүлээгдэж буй байдлаар ажиллах, аюулгүй байдлыг хангахад зайлшгүй шаардлагатай.
Албан ёсны баталгаажуулалт нь сул талыг олж илрүүлэх, арилгах хамгийн хүчирхэг хэрэгсэл юм: энэ нь програмын бүх цоорхой, алдааг олох, эсвэл байхгүй гэдгийг батлах боломжийг олгодог.
Зарим тохиолдолд энэ нь боломжгүй зүйл гэдгийг тэмдэглэх нь зүйтэй, тухайлбал 8 квадратын өргөнтэй 1000 хатан хааны асуудал: энэ бүхэн алгоритмын нарийн төвөгтэй байдал эсвэл зогсоох асуудалтай холбоотой юм.
Гэсэн хэдий ч ямар ч тохиолдолд програм зөв, буруу эсвэл хариултыг тооцоолох боломжгүй гэсэн гурван хариултын аль нэгийг хүлээн авах болно.
Хэрэв хариулт олох боломжгүй бол тодорхой тийм эсвэл үгүй гэсэн хариултыг авахын тулд програмын тодорхой бус хэсгүүдийг алгоритмын нарийн төвөгтэй байдлыг бууруулж дахин боловсруулах боломжтой байдаг.
Мөн албан ёсны баталгаажуулалтыг, жишээлбэл, Windows цөм болон Darpa drone үйлдлийн системд хамгаалалтын дээд түвшинг хангахын тулд ашигладаг.
Бид автоматжуулсан теоремыг батлах, тэгшитгэлийг шийдвэрлэх маш хүчирхэг хэрэгсэл болох Z3Prover-ийг ашиглах болно.
Түүнээс гадна Z3 нь тэгшитгэлийг шийддэг бөгөөд тэдгээрийн утгыг харгис хүчээр сонгодоггүй.
Энэ нь 10^100 оролтын сонголттой байсан ч хариултыг олох боломжтой гэсэн үг юм.
Гэхдээ энэ нь бүхэл тоо төрлийн арав орчим оролтын аргумент бөгөөд энэ нь практикт ихэвчлэн тулгардаг.
8 хатны тухай асуудал (Англи хэлнээс авсан ).
# 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-ийг ажиллуулснаар бид дараах шийдлийг олж авна.
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Хатан хааны асуудлыг 8 хатны координатыг оруулан авч, хатадууд бие биенээ ялсан эсэхийн хариултыг гаргадаг програмтай харьцуулж болно.
Хэрэв бид ийм програмыг албан ёсны баталгаажуулалтыг ашиглан шийдэх байсан бол асуудалтай харьцуулахад програмын кодыг тэгшитгэл болгон хөрвүүлэх хэлбэрээр дахин нэг алхам хийх шаардлагатай болно: энэ нь биднийхтэй үндсэндээ ижил байх болно ( Мэдээж хэрэг, хэрэв програм зөв бичсэн бол).
Сул талуудыг хайж олоход бараг ижил зүйл тохиолдох болно: бид зүгээр л шаардлагатай гаралтын нөхцлүүдийг, жишээлбэл, администраторын нууц үгийг тохируулж, эх сурвалж эсвэл задалсан кодыг баталгаажуулалтад нийцсэн тэгшитгэл болгон хувиргаж, дараа нь юу гэсэн хариултыг авна. зорилгодоо хүрэхийн тулд өгөгдлийг орц болгон өгөх шаардлагатай.
Миний бодлоор чоно, ямаа, байцаатай холбоотой асуудал бүр ч сонирхолтой, учир нь үүнийг шийдвэрлэхэд олон (7) алхам шаардлагатай.
Хэрэв хатны асуудал нь нэг GET эсвэл POST хүсэлтийг ашиглан серверт нэвтэрч болох тохиолдолтой харьцуулах боломжтой бол чоно, ямаа, байцаа нь зөвхөн зорилгодоо хүрч болох илүү төвөгтэй, өргөн тархсан ангиллын жишээг харуулж байна. хэд хэдэн хүсэлтээр.
Үүнийг жишээ нь, та SQL тарилга олж, түүгээр дамжуулан файл бичиж, эрхээ дээшлүүлж, дараа нь нууц үгээ авах шаардлагатай хувилбартай харьцуулж болно.
Асуудлын нөхцөл ба түүний шийдэлТариаланч голын дээгүүр чоно, ямаа, байцаа тээвэрлэх хэрэгтэй. Тариаланч нь тариачин өөрөөс гадна зөвхөн нэг объектыг багтаах завьтай. Тариачин тэднийг хараа хяналтгүй орхивол ямаа нь чоно, ямаа нь байцаа идэх болно.
Үүний шийдэл нь 4-р алхамд фермер ямаагаа буцааж авах шаардлагатай болно.
Одоо үүнийг программын дагуу шийдэж эхэлцгээе.
Фермер, чоно, ямаа, байцаа зэргийг зөвхөн 4 эсвэл 0 гэсэн утгыг авдаг 1 хувьсагч гэж тэмдэглэе. Тэг нь зүүн эрэгт, нэг нь баруун талд байна гэсэн үг.
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
Тоо нь шийдвэрлэхэд шаардлагатай алхамуудын тоо юм. Алхам бүр нь голын байдал, завь болон бүх байгууллагыг илэрхийлдэг.
Одоохондоо үүнийг санамсаргүй байдлаар сонгоод, зөрүүтэйгээр 10-ыг ав.
Байгууллага бүрийг 10 хувь хэлбэрээр төлөөлдөг - энэ нь 10 алхам бүрийн үнэ цэнэ юм.
Одоо эхлэх, дуусгах нөхцөлийг тогтооцгооё.
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 ]
Дараа нь бид чоно ямаа идэх, ямаа байцаа идэх нөхцөлийг тэгшитгэлд хязгаарлалт болгон тавьдаг.
(Тариаланч байгаа тохиолдолд түрэмгийлэл хийх боломжгүй)
# 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) ]
Эцэст нь бид тэнд гатлах эсвэл буцахдаа фермерийн хийх боломжтой бүх үйлдлийг тодорхойлох болно.
Тэр нэг бол чоно, ямаа, байцаа авч явах, эсвэл хэнийг ч авч явахгүй, эсвэл огтхон ч далайд гарахгүй.
Мэдээжийн хэрэг, тариачингүйгээр хэн ч гаталж чадахгүй.
Энэ нь гол мөрөн, завь, аж ахуйн нэгжийн дараагийн төлөв бүр өмнөхөөсөө зөвхөн хатуу хязгаарлагдмал байдлаар ялгаатай байж болно гэдгийг илэрхийлэх болно.
Фермер нэг удаад зөвхөн нэг аж ахуйн нэгжийг тээвэрлэх боломжтой бөгөөд бүгдийг нь хамт үлдээх боломжгүй тул 2 битээс илүүгүй, бусад олон хязгаарлалттай.
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) ]
Шийдлийг ажиллуулцгаая.
solve(Side + Start + Finish + Safe + Travel)
Тэгээд бид хариултаа авах болно!
Z3 нь бүх нөхцлийг хангасан тогтвортой байдлын багцыг олсон.
Нэг төрлийн дөрвөн хэмжээст орон зай цаг хугацаа.
Юу болсныг олж мэдье.
Эцэст нь бүгд гаталж, зөвхөн манай тариачин амрахаар шийдсэн бөгөөд эхний 2 алхамд тэр хаана ч сэлж чаддаггүйг бид харж байна.
Human_2 = 0
Human_3 = 0
Энэ нь бидний сонгосон мужуудын тоо хэт их байгаа бөгөөд 8 нь хангалттай байх болно гэдгийг харуулж байна.
Манай тохиолдолд тариачин үүнийг хийсэн: эхлэх, амрах, амрах, ямаа гатлах, буцаж гатлах, байцаа гатлах, ямаатай буцаж ирэх, чоно гатлах, ганцаараа буцаж ирэх, ямаагаа дахин хүргэх.
Гэвч эцэст нь асуудал шийдэгдсэн.
#Старт.
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
Одоо нөхцөл байдлыг өөрчилж, ямар ч шийдэл байхгүй гэдгийг батлахыг хичээцгээе.
Үүнийг хийхийн тулд бид чонондоо өвсөн тэжээл өгөх болно, тэр байцаа идэхийг хүсэх болно.
Үүнийг бидний зорилго нь програмын аюулгүй байдлыг хангах явдал бөгөөд бид ямар ч цоорхой байхгүй эсэхийг шалгах шаардлагатай байгаатай харьцуулж болно.
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 бидэнд дараах хариултыг өгсөн.
no solution
Энэ нь үнэхээр шийдэл байхгүй гэсэн үг.
Тиймээс бид тариачинд алдагдалгүй идэшт чонотой гатлах боломжгүй гэдгийг программчлан нотолсон.
Хэрэв үзэгчдэд энэ сэдвийг сонирхолтой гэж үзвэл дараагийн нийтлэлүүдэд би ердийн програм эсвэл функцийг албан ёсны аргуудтай нийцтэй тэгшитгэл болгон хувиргаж, үүнийг шийдвэрлэхийн тулд бүх хууль ёсны хувилбарууд болон сул талуудыг илчлэх талаар танд хэлэх болно. Нэгдүгээрт, ижил даалгавар дээр, гэхдээ програмын хэлбэрээр танилцуулж, дараа нь үүнийг аажмаар улам хүндрүүлж, програм хангамж хөгжүүлэх ертөнцөөс одоогийн жишээнүүд рүү шилждэг.
Дараагийн нийтлэл аль хэдийн бэлэн болсон байна:
Үүнд би асуудлын албан ёсны баталгаажуулалтаас программ руу шилжиж, тайлбарлаж байна
тэдгээрийг хэрхэн автоматаар албан ёсны дүрмийн систем болгон хувиргах вэ.
Эх сурвалж: www.habr.com