Na minha opinião, no setor de língua russa da Internet, o tópico da verificação formal não é suficientemente abordado e faltam exemplos especialmente simples e claros.
Darei esse exemplo de uma fonte estrangeira e complementarei minha própria solução ao conhecido problema de transportar um lobo, cabra e couve para o outro lado do rio.
Mas primeiro, descreverei brevemente o que é a verificação formal e por que é necessária.
A verificação formal geralmente significa verificar um programa ou algoritmo usando outro.
Isso é necessário para garantir que o comportamento do programa seja 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 todos os buracos e bugs existentes no programa ou provar que eles não estão lá.
Vale a pena notar que em alguns casos isso é impossível, como no problema de 8 rainhas com uma largura de placa de 1000 células: tudo depende da complexidade algorítmica ou do problema de parada.
No entanto, em qualquer caso, uma das três respostas será recebida: o programa está correto, incorreto ou a resposta não pôde ser calculada.
Se não for possível encontrar uma resposta, muitas vezes é possível refazer locais obscuros do programa, reduzindo sua complexidade algorítmica para 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 dos drones Darpa, para fornecer 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 exatamente as equações e não seleciona seus valores com força bruta.
Isso significa que ele é capaz de encontrar a resposta, mesmo nos casos em que combinações de opções de entrada e 10 ^ 100.
Mas isso é apenas uma dúzia de argumentos de entrada do tipo Inteiro, e isso geralmente é encontrado na prática.
O problema das 8 rainhas (retirado do
manual 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)
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 pega as coordenadas de 8 rainhas e exibe a resposta se as rainhas se baterem.
Se resolvêssemos esse programa usando a verificação formal, em comparação com a tarefa, precisaríamos dar outro passo na forma de converter o código do programa em uma equação: seria essencialmente idêntico ao nosso (é claro, se o programa fosse escrito corretamente).
Quase o mesmo acontecerá ao procurar vulnerabilidades: definimos apenas as condições de saída necessárias, por exemplo, a senha de administrador, convertemos o código de origem ou descompilado em equações compatíveis com a verificação e obtemos a resposta de quais dados precisam ser inseridos para atingir a meta.
Na minha opinião, o problema do lobo, cabra e couve é ainda mais interessante, já que muitas (7) etapas já são necessárias para resolvê-lo.
Se o problema da rainha for comparável à opção em que você pode penetrar no servidor usando uma solicitação GET ou POST, o lobo, a cabra e o repolho demonstram um exemplo de uma categoria muito mais complexa e difundida, na qual apenas algumas solicitações podem ser alcançadas.
Isso é comparável, por exemplo, ao cenário em que você precisa encontrar a injeção de SQL, gravar um arquivo nele, aumentar seus direitos e somente obter a senha.
Condições problemáticas e sua soluçãoO agricultor precisa transportar o lobo, cabra e repolho através do rio. O fazendeiro tem um barco no qual apenas um objeto pode caber, exceto o próprio camponês. O lobo comerá a cabra, e a cabra comerá repolho se o fazendeiro os deixar sem vigilância.
A solução é que, na etapa 4, o agricultor precisará levar a cabra de volta.
Agora vamos iniciar a solução programaticamente.
Designamos o fazendeiro, o lobo, a cabra e o repolho como 4 variáveis, que assumem o valor apenas 0 ou 1. Zero significa que eles estão na margem esquerda e um 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) ] # 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 é o estado de um rio, barco e todas as entidades.
Por enquanto, escolha aleatoriamente e com uma margem, pegue 10.
Cada entidade é representada em 10 cópias - esse é o seu valor em cada uma das 10 etapas.
Agora, definimos as condições para começar e terminar.
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 repolho de cabra, como restrições na equação.
(Na presença do agricultor, a agressão não é possí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, pedimos todas as ações possíveis do agricultor quando se deslocam para lá ou para trás.
Ele pode levar um lobo, uma cabra ou um repolho com ele, ou levar ninguém, ou mesmo não ir a lugar algum.
Claro, ninguém pode atravessar sem um fazendeiro.
Isso será expresso pelo fato de que cada estado subsequente do rio, barco e entidades pode diferir do estado anterior apenas de uma maneira estritamente limitada.
Não mais que 2 bits e com muitos outros limites, 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) ]
Execute a solução.
solve(Side + Start + Finish + Safe + Travel)
E nós obtemos a resposta!
O Z3 encontrou um conjunto de condições consistente e satisfatório.
Uma espécie de elenco quadridimensional do espaço-tempo.
Vamos ver o que aconteceu.
Vimos que, no final, todos cruzaram, apenas no início nosso fazendeiro decidiu relaxar e não nada em nenhum lugar nos dois primeiros passos.
Human_2 = 0 Human_3 = 0
Isso sugere que o número de estados que escolhemos é excessivo e 8 será suficiente.
No nosso caso, o fazendeiro fez isso: começar, descansar, descansar, atravessar a cabra, atravessar para trás, atravessar repolho, retornar com a cabra, cruzar o lobo, voltar sozinho, voltar a entregar a cabra.
Mas, no final, o problema está 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, dotaremos nosso lobo de herbívoro e ele desejará comer repolho.
Isso pode ser comparado ao caso em que nosso objetivo é proteger o aplicativo 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) ]
O Z3 nos deu a seguinte resposta:
no solution
Isso significa que realmente não há soluções.
Assim, provamos programaticamente a impossibilidade de cruzar com um lobo onívoro, sem perdas para o agricultor.
Se o público achar esse tópico interessante, em artigos futuros, mostrarei como transformar um programa ou função comum em uma equação compatível com métodos formais e resolvê-lo, revelando, assim, todos os cenários e vulnerabilidades legítimos. Primeiro, na mesma tarefa, mas já apresentado na forma de um programa e, em seguida, gradualmente complicando e passando para exemplos relevantes do mundo do desenvolvimento de software.
O seguinte artigo está pronto:
Criando um sistema formal de verificação do zero: escrevemos uma VM de caractere em PHP e PythonNele, passo da verificação formal de tarefas para programas e descrevo
como convertê-los em sistemas formais de regras automaticamente.