Na minha opinião, na internet de língua russa, o tema da verificação formal é abordado de maneira insuficiente, e especialmente faltam exemplos simples e claros.
Vou apresentar um exemplo de uma fonte estrangeira e complementá-lo com a minha própria solução para o conhecido problema da travessia do lobo, da cabra e da couve para o outro lado do rio.
Mas antes vou descrever brevemente o que é a verificação formal e por que ela é necessária.
Verificação formal geralmente significa verificar um programa ou algoritmo usando outro programa.
Isso é necessário para garantir que o comportamento do programa corresponda ao esperado, além de garantir sua segurança.
A verificação formal é o meio mais poderoso para identificar e eliminar vulnerabilidades: ela permite descobrir todas as falhas e bugs existentes no programa, ou provar que eles não existem.
Vale ressaltar que em alguns casos isso pode ser impossível, como no caso das 8 rainhas em um tabuleiro de 1000 casas: tudo depende da complexidade algorítmica ou do problema da parada.
No entanto, em qualquer caso, será obtida uma das três respostas: o programa é correto, incorreto ou não foi possível calcular a resposta.
Caso não seja possível encontrar uma resposta, muitas vezes é possível reformular as partes obscuras do programa, reduzindo sua complexidade algorítmica, para obter uma resposta concreta de sim ou não.
A verificação formal é utilizada, por exemplo, no núcleo do Windows e nos sistemas operacionais de drones da Darpa, para garantir o máximo nível de proteção.
Usaremos o Z3Prover, uma ferramenta muito poderosa para a prova automatizada de teoremas e solução de equações.
O Z3 realmente resolve equações, e não simplesmente tenta adivinhar seus valores por força bruta.
Isso significa que ele é capaz de encontrar a resposta, mesmo em casos de combinações de entradas com 10^100.
E isso é apenas cerca de uma dúzia de argumentos de entrada do tipo Integer, algo que muitas vezes ocorre na prática.
O problema das 8 rainhas (Extraído de uma documentação em 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)
Ao executar 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 das rainhas é comparável a um programa que recebe as coordenadas de 8 rainhas e devolve a resposta se as rainhas se atacam.
Se estivéssemos resolvendo esse programa através da verificação formal, então, em comparação com a tarefa, precisaríamos apenas dar mais um passo que seria converter o código do programa em uma equação: ela seria, basicamente, idêntica à nossa (é claro, se o programa estiver escrito corretamente).
Praticamente a mesma coisa acontecerá no caso de busca por vulnerabilidades: nós simplesmente definimos as condições de saída que precisamos, como a senha do administrador, convertemos o código fonte ou decompilado em equações compatíveis com a verificação e, em seguida, obtemos a resposta sobre quais dados devem ser fornecidos como entrada para alcançar o objetivo.
Na minha opinião, a tarefa do lobo, da cabra e do repolho é ainda mais interessante, pois para sua solução são necessários muitos (7) passos.
Se a tarefa das rainhas é comparável a uma situação em que se pode invadir o servidor com 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 comum, na qual os objetivos podem ser alcançados apenas com várias solicitações.
Isso é comparável, por exemplo, a um cenário onde é necessário encontrar uma injeção SQL, gravar um arquivo através dela, depois elevar seus privilégios e só então obter a senha.
Condições da tarefa e sua soluçãoO fazendeiro precisa transportar o lobo, a cabra e o repolho através do rio. O fazendeiro tem um barco que pode acomodar, além do próprio agricultor, apenas um objeto. O lobo comerá a cabra, e a cabra comerá o repolho se o fazendeiro deixá-los sem supervisão.
A solução é que na quarta etapa o fazendeiro precisará levar a cabra de volta.
Agora vamos iniciar a solução de forma programática.
Vamos indicar o fazendeiro, o lobo, a cabra e o repolho como 4 variáveis, que podem assumir apenas o valor 0 ou 1. Zero significa que estão na margem esquerda, enquanto um significa que estão na 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) ]
# Cada criatura pode estar apenas do lado esquerdo (0) ou direito (1) em cada estado
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 passos necessários para a solução. Cada passo representa um estado do rio, do barco e de todas as entidades.
Por enquanto, vamos escolhê-lo aleatoriamente e com uma margem, pegaremos 10.
Cada entidade é representada em 10 exemplares — esse é seu valor em cada uma das 10 etapas.
Agora vamos definir as condições para o início e o fim.
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, vamos definir as condições em que o lobo come a cabra, ou a cabra come a couve, como restrições na equação.
(Na presença do 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, finalmente, vamos definir todas as possíveis ações do agricultor ao atravessar de um lado para o outro.
Ele pode levar consigo o lobo, a cabra ou a couve, ou não levar ninguém, ou nem mesmo atravessar.
Obviamente, sem o agricultor, ninguém pode atravessar.
Isso será expresso pelo fato de que cada estado subsequente do rio, do barco e das entidades pode diferir do anterior apenas de maneira estritamente limitada.
Não mais do que 2 bits, e com muitas outras limitações, pois o agricultor pode transportar apenas uma entidade por vez e nem todos podem ser deixados juntos.
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 iniciar a solução.
solve(Side + Start + Finish + Safe + Travel)
E obtemos a resposta!
O Z3 encontrou um conjunto de estados consistente e que atende a todas as condições.
Um tipo de impressão quadridimensional do espaço-tempo.
Vamos entender o que aconteceu.
Vemos que, no final, todos conseguiram atravessar, mas no início nosso agricultor decidiu descansar e não atravessou nos primeiros 2 passos.
Human_2 = 0
Human_3 = 0
Isso indica que o número de estados que escolhemos é excessivo, e 8 será mais do que suficiente.
No nosso caso, o agricultor fez o seguinte: início, descanso, descanso, atravessar a cabra, voltar, atravessar a couve, voltar com a cabra, atravessar o lobo, voltar sozinho, entregar novamente a cabra.
Mas, no final, a tarefa foi resolvida.
#Старт.
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 isso, daremos ao nosso lobo a herbivoria, e ele vai querer comer a couve.
Isso pode ser comparado a um caso em que nosso objetivo é proteger a aplicação e precisamos garantir que não haja 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:
sem solução
Isso significa que realmente não há soluções.
Assim, provamos programaticamente a impossibilidade de atravessar com o lobo onívoro, sem perdas para o fazendeiro.
Se o público achar esse tema interessante, nas próximas artigos eu falarei sobre como transformar um programa ou função comum em uma equação compatível com métodos formais e resolvê-la, descobrindo assim tanto cenários legítimos quanto vulnerabilidades. Primeiro com esta mesma tarefa, mas apresentada já na forma de um programa, e depois gradualmente complicando e passando para exemplos relevantes do mundo do desenvolvimento de software.
O próximo artigo já está pronto:
Nele, eu passo da verificação formal de tarefas para programas, e descrevo,
como pode-se convertê-los em sistemas de regras formais automaticamente.
Fonte: habr.com
