Na minha opinião, no sector da Internet de língua russa, o tema da verificação formal não é suficientemente coberto e faltam especialmente exemplos simples e claros.
Darei um exemplo de fonte estrangeira e acrescentarei minha própria solução ao conhecido problema de cruzar um lobo, uma cabra e um repolho para o outro lado do rio.
Mas primeiro, descreverei brevemente o que é a verificação formal e por que ela é necessária.
A verificação formal geralmente significa verificar um programa ou algoritmo usando outro.
Isso é necessário para garantir que o programa se comporte conforme o esperado e também para garantir sua segurança.
A verificação formal é o meio mais poderoso de encontrar e eliminar vulnerabilidades: permite encontrar todas as falhas e bugs existentes em um programa ou provar que eles não existem.
É importante notar que em alguns casos isso é impossível, como no problema de 8 rainhas com tabuleiro de 1000 quadrados de largura: tudo se resume à complexidade algorítmica ou ao problema de parada.
Porém, em qualquer caso, será recebida uma de três respostas: o programa está correto, incorreto ou não foi possível calcular a resposta.
Se for impossível encontrar uma resposta, muitas vezes é possível retrabalhar partes pouco claras do programa, reduzindo a sua complexidade algorítmica, a fim de obter uma resposta específica sim ou não.
E a verificação formal é usada, por exemplo, no kernel do Windows e nos sistemas operacionais de drones Darpa, para garantir o nível máximo de proteção.
Usaremos o Z3Prover, uma ferramenta muito poderosa para prova automatizada de teoremas e resolução de equações.
Além disso, Z3 resolve equações e não seleciona seus valores por meio de força bruta.
Isso significa que ele é capaz de encontrar a resposta, mesmo nos casos em que existem 10^100 combinações de opções de entrada.
Mas isso é apenas cerca de uma dúzia de argumentos de entrada do tipo Integer, e isso é frequentemente encontrado na prática.
Problema sobre 8 rainhas (retirado do inglês ).
# 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)
Executando o Z3, obtemos a solução:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
O problema da rainha é comparável a um programa que recebe como entrada as coordenadas de 8 rainhas e produz a resposta se as rainhas vencem umas às outras.
Se resolvêssemos tal programa usando verificação formal, então, em comparação com o problema, precisaríamos simplesmente dar mais um passo na forma de converter o código do programa em uma equação: ele acabaria sendo essencialmente idêntico ao nosso ( claro, se o programa foi escrito corretamente).
Quase a mesma coisa acontecerá no caso de busca por vulnerabilidades: apenas definimos as condições de saída que precisamos, por exemplo, a senha do administrador, transformamos o código fonte ou descompilado em equações compatíveis com a verificação e então obtemos uma resposta sobre o que os dados precisam ser fornecidos como entrada para atingir a meta.
Na minha opinião, o problema do lobo, da cabra e do repolho é ainda mais interessante, pois resolvê-lo já requer muitos (7) passos.
Se o problema da rainha for comparável ao caso em que você pode penetrar em um servidor usando uma única solicitação GET ou POST, então o lobo, a cabra e o repolho demonstram um exemplo de uma categoria muito mais complexa e difundida, na qual o objetivo só pode ser alcançado por vários pedidos.
Isso é comparável, por exemplo, a um cenário onde você precisa encontrar uma injeção de SQL, escrever um arquivo através dela, depois elevar seus direitos e só então obter uma senha.
Condições do problema e sua soluçãoO fazendeiro precisa transportar um lobo, uma cabra e um repolho para o outro lado do rio. O agricultor possui um barco que só acomoda um objeto, além do próprio agricultor. O lobo comerá a cabra e a cabra comerá o repolho se o fazendeiro os deixar sozinhos.
A solução é que no passo 4 o agricultor terá de levar a cabra de volta.
Agora vamos começar a resolvê-lo programaticamente.
Vamos denotar o agricultor, o lobo, a cabra e o repolho como 4 variáveis que assumem o valor apenas 0 ou 1. Zero significa que estão na margem esquerda e um significa que estão na margem direita.
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 é o número de etapas necessárias para resolver. Cada etapa representa o estado do rio, do barco e de todas as entidades.
Por enquanto, vamos escolher aleatoriamente e com margem, pegue 10.
Cada entidade é representada em 10 cópias – este é o seu valor em cada uma das 10 etapas.
Agora vamos definir as condições de largada e chegada.
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 ]
Em seguida, definimos as condições em que o lobo come a cabra, ou a cabra come o repolho, como restrições na equação.
(Na presença de um agricultor a agressão é impossível)
# 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) ]
E por fim, definiremos todas as ações possíveis do agricultor ao cruzar de ida ou volta.
Ele pode levar consigo um lobo, uma cabra ou um repolho, ou não levar ninguém, ou não navegar para lugar nenhum.
Claro, ninguém pode atravessar sem um agricultor.
Isto será expresso pelo fato de que cada estado subsequente do rio, barco e entidades pode diferir do anterior apenas de forma estritamente limitada.
Não mais que 2 bits, e com muitos outros limites, já que o agricultor só pode transportar uma entidade por vez e nem todas podem ficar juntas.
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) ]
Vamos executar a solução.
solve(Side + Start + Finish + Safe + Travel)
E nós obtemos a resposta!
Z3 encontrou um conjunto consistente de estados que satisfaz todas as condições.
Uma espécie de elenco quadridimensional do espaço-tempo.
Vamos descobrir o que aconteceu.
Vemos que no final todos atravessaram, só que no início o nosso agricultor decidiu descansar, e nos primeiros 2 passos não nada para lado nenhum.
Human_2 = 0
Human_3 = 0
Isto sugere que o número de estados que escolhemos é excessivo e 8 serão suficientes.
No nosso caso, o fazendeiro fez isso: começar, descansar, descansar, cruzar o bode, cruzar de volta, cruzar o repolho, voltar com o bode, cruzar o lobo, voltar sozinho, reentregar o bode.
Mas no final o problema foi resolvido.
#Старт.
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
Agora vamos tentar mudar as condições e provar que não há soluções.
Para fazer isso, daremos herbivoria ao nosso lobo, e ele vai querer comer repolho.
Isso pode ser comparado ao caso em que nosso objetivo é proteger o aplicativo e precisamos ter certeza de que não há brechas.
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 nos deu a seguinte resposta:
no solution
Isso significa que realmente não há soluções.
Assim, comprovamos programaticamente a impossibilidade de cruzamento com um lobo onívoro sem perdas para o agricultor.
Se o público achar este tópico interessante, em artigos futuros direi como transformar um programa ou função comum em uma equação compatível com métodos formais e resolvê-la, revelando assim todos os cenários e vulnerabilidades legítimos. Primeiro, na mesma tarefa, mas apresentada em forma de programa, e depois complicando-a gradativamente e passando para exemplos atuais do mundo do desenvolvimento de software.
O próximo artigo já está pronto:
Nele passo da verificação formal de problemas para programas e descrevo
como eles podem ser convertidos automaticamente em sistemas de regras formais.
Fonte: habr.com