늑대, 염소, 양배추 문제의 예를 이용한 형식적 검증

제 생각에는 인터넷의 러시아어 부문에서는 공식 검증 주제가 충분히 다루어지지 않았고 특히 간단하고 명확한 예가 부족합니다.

나는 외국 자료의 예를 제시하고 늑대, 염소, 양배추를 강 반대편으로 건너는 잘 알려진 문제에 대한 나만의 해결책을 추가하겠습니다.

하지만 먼저 공식 검증이 무엇인지, 왜 필요한지에 대해 간략하게 설명하겠습니다.

공식 검증은 일반적으로 다른 프로그램이나 알고리즘을 사용하여 하나의 프로그램이나 알고리즘을 확인하는 것을 의미합니다.

이는 프로그램이 예상대로 작동하는지 확인하고 보안을 보장하는 데 필요합니다.

공식 검증은 취약점을 찾고 제거하는 가장 강력한 수단입니다. 이를 통해 프로그램의 기존 허점과 버그를 모두 찾거나 존재하지 않음을 증명할 수 있습니다.
보드 너비가 8제곱인 1000개의 퀸 문제와 같이 어떤 경우에는 이것이 불가능하다는 점은 주목할 가치가 있습니다. 모든 것은 알고리즘의 복잡성이나 중지 문제로 귀결됩니다.

그러나 어떤 경우에도 프로그램이 정확하거나, 틀리거나, 답을 계산할 수 없다는 세 가지 답변 중 하나가 수신됩니다.

답을 찾는 것이 불가능한 경우 구체적인 예 또는 아니요 답을 얻기 위해 프로그램의 명확하지 않은 부분을 재작업하여 알고리즘의 복잡성을 줄이는 것이 가능한 경우가 많습니다.

예를 들어 Windows 커널 및 Darpa 드론 운영 체제에서는 최대 수준의 보호를 보장하기 위해 공식 검증이 사용됩니다.

우리는 자동화된 정리 증명과 방정식 풀이를 위한 매우 강력한 도구인 Z3Prover를 사용할 것입니다.

또한 Z3은 방정식을 풀고 무차별 대입을 사용하여 해당 값을 선택하지 않습니다.
이는 10^100개의 입력 옵션 조합이 있는 경우에도 답을 찾을 수 있음을 의미합니다.

그러나 이는 Integer 유형의 입력 인수가 12개 정도에 불과하며 실제로는 자주 접하게 됩니다.

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개의 변수로 표시해보자. XNUMX은 왼쪽 둑에 있다는 뜻이고, XNUMX은 오른쪽 둑에 있다는 뜻이다.

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은 문제를 해결하는 데 필요한 단계 수입니다. 각 단계는 강, 보트 및 모든 개체의 상태를 나타냅니다.

지금은 무작위로 선택하고 여유를 두고 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은 모든 조건을 만족하는 일관된 상태 집합을 찾았습니다.
일종의 4차원 시공간 캐스트입니다.

무슨 일이 일어났는지 알아봅시다.

우리는 결국 모두가 건넜고 처음에는 농부가 휴식을 취하기로 결정했고 처음 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

정말 해결책이 없다는 뜻이다.

따라서 우리는 농부의 손실 없이 잡식성 늑대와 교배하는 것이 불가능하다는 것을 프로그래밍 방식으로 증명했습니다.

청중이 이 주제에 흥미를 느낀다면 향후 기사에서는 일반적인 프로그램이나 함수를 형식적 방법과 호환되는 방정식으로 변환하고 해결하여 모든 합법적인 시나리오와 취약점을 모두 드러내는 방법을 알려 드리겠습니다. 첫째, 동일한 작업에 대해 프로그램 형태로 제시된 다음 점차 복잡해지고 소프트웨어 개발 세계의 현재 사례로 이동합니다.

다음 기사는 이미 준비되어 있습니다.
처음부터 공식 검증 시스템 만들기: PHP 및 Python에서 기호형 VM 작성

여기서 나는 문제의 공식 검증에서 프로그램으로 이동하고 설명합니다.
어떻게 자동으로 공식 규칙 시스템으로 변환할 수 있습니까?

출처 : habr.com