Os Limites da Verificação

• Enunciar com precisão a consequência do Teorema de Rice para a verificação de programas e dar dois exemplos concretos de propriedades que ele impede de decidir em geral.
• Distinguir correção (soundness) de completude e explicar por que a maioria das ferramentas práticas escolhe garantir a correção ao custo da completude.
• Explicar a diferença entre superaproximação e subaproximação e que tipo de erro cada uma arrisca.
• Enumerar os modos pelos quais um programa verificado ainda pode falhar em um requisito do mundo real, apesar de uma prova totalmente correta.
• Reconstruir, a partir de primeiros princípios, por que não pode existir um verificador universal de terminação e correção, usando o Problema da Parada como a impossibilidade de fundo.

Cada técnica que esta disciplina construiu (prova em lógica de Hoare, resolução SAT e SMT, model checking, assistentes de prova) foi apresentada junto com um relato honesto de onde ela deixa de funcionar: das triplas trivialmente verdadeiras em the-hoare-triple aos fragmentos aritméticos indecidíveis em smt-solvers-and-decision-procedures, do crescimento exponencial do espaço de estados em state-space-explosion-and-symbolic-model-checking às ressalvas sobre a base de confiança dos assistentes de prova em theorem-proving-and-proof-assistants. Este conceito é onde essas limitações espalhadas são reunidas na única afirmação unificadora da disciplina sobre o que a verificação formal pode, e o que não pode, prometer em última instância; não como um final desanimador, mas como o argumento de encerramento honesto que torna confiável tudo o que já foi construído, justamente porque seu escopo foi enunciado com precisão.

O objetivo dos métodos formais nunca foi derrotar os resultados de indecidibilidade que Computabilidade e Complexidade já provou; foi, desde testing-shows-presence-proof-shows-absence, trabalhar de forma honesta e produtiva dentro das suas fronteiras. O Problema da Parada exclui um oráculo universal de terminação, e o Teorema de Rice generaliza essa impossibilidade de forma dramática: ele exclui decidir qualquer propriedade semântica não trivial da função que um programa arbitrário calcula, e não só a terminação especificamente. A boa prática de verificação, como este conceito desenvolve, responde a esses fatos não fingindo que eles não se aplicam, mas enunciando premissas explicitamente, escolhendo fragmentos decidíveis de propósito e sendo precisa sobre a diferença entre uma prova totalmente correta e uma evidência apenas limitada e parcial; a mesma distinção que testing-shows-presence-proof-shows-absence traçou entre prova e testes logo no início desta disciplina, agora generalizada para distinguir entre os diferentes tipos de evidência formal que esta disciplina construiu desde então.

O impacto do Teorema de Rice

O Teorema de Rice, provado em toda a sua generalidade em Computabilidade e Complexidade, afirma que qualquer propriedade não trivial da função calculada por um programa arbitrário é indecidível; não trivial significa que a propriedade é verdadeira para algumas funções computáveis e falsa para outras, excluindo só os casos degenerados de uma propriedade trivialmente sempre verdadeira ou sempre falsa, qualquer que seja o programa. Exemplos concretos exatamente do tipo de propriedade que isso impede de decidir automaticamente para todo programa possível: "sempre devolve zero" é não trivial (alguns programas devolvem, outros não), e "nunca vaza um valor secreto em um canal público" também é, e "ordena corretamente toda entrada" também é; cada uma dessas é uma afirmação semântica genuína e significativa, e o Teorema de Rice diz que não pode existir algoritmo que a decida corretamente para um programa arbitrário que lhe seja entregue. Isso significa que um verificador automático completo e de uso geral (um que pudesse receber literalmente qualquer programa e qualquer afirmação semântica não trivial e sempre decidir corretamente se a afirmação vale) não pode existir, ponto final, exatamente pelo mesmo motivo que não pode existir um decisor universal de parada; as duas impossibilidades compartilham sua estrutura matemática essencial.

Correção versus completude

Duas propriedades distintas que uma ferramenta de verificação pode ou não ter merecem ser separadas com cuidado, porque confundi-las é um dos mal-entendidos de maior consequência que um usuário de ferramentas formais pode cometer. Correção (soundness) significa que a ferramenta nunca aceita uma prova falsa: se ela relata que uma propriedade vale, a propriedade de fato vale, sem exceções. Completude significa que a ferramenta consegue provar toda propriedade que é de fato verdadeira dentro do seu escopo pretendido: nenhum fato verdadeiro jamais lhe escapa. Dado o Teorema de Rice, nenhuma ferramenta consegue ser ao mesmo tempo correta e completa para propriedades semânticas não triviais arbitrárias de programas arbitrários; algo precisa ceder. A grande maioria das ferramentas de verificação práticas e em uso escolhe preservar a correção e sacrificar a completude (aceitando que a ferramenta às vezes pode não conseguir provar uma propriedade que é, de fato, verdadeira, em vez de arriscar alguma vez aceitar uma falsa), porque as respostas "sim" de uma ferramenta correta, porém incompleta, continuam totalmente confiáveis, mesmo que suas respostas "não sei" não carreguem informação útil para nenhum lado, enquanto as respostas "sim" de uma ferramenta incorreta não merecem confiança nenhuma, o que mina desde a base todo o sentido da verificação formal.

Aproximações

As ferramentas que escolhem a incompletude em vez da incorreção normalmente fazem isso por uma de duas estratégias características, e reconhecer qual delas uma dada ferramenta usa é essencial para ler corretamente a saída dela. Analisadores estáticos costumam superaproximar: eles consideram um superconjunto dos comportamentos que um programa pode genuinamente exibir, para continuar corretos mesmo quando o raciocínio preciso sobre o comportamento real e exato seria caro ou indecidível demais para tentar; o custo dessa escolha são os alarmes falsos, avisos sobre comportamentos que a superaproximação admite como possíveis, mas que o programa concreto nunca conseguiria de fato produzir. Buscadores de bugs costumam subaproximar: eles exploram só uma parte limitada do comportamento real de um programa (caminhos até uma profundidade fixa, execuções dentro de um limite fixo) para continuar rápidos e concretos, ao custo de potencialmente deixar passar bugs genuínos que só se manifestam além do limite escolhido. Nenhuma das estratégias de aproximação é um defeito de que se envergonhar; as duas são escolhas de engenharia úteis e fundamentadas, desde que os usuários da ferramenta entendam qual delas está em jogo e leiam a saída "nenhum bug encontrado" ou "possível violação" da ferramenta tendo em mente o ponto cego específico daquela aproximação específica.

Limites da especificação

Mesmo uma prova totalmente correta, executada sem falhas contra uma propriedade totalmente bem especificada, ainda pode deixar de entregar a confiança que um interessado de fato queria, por motivos que não têm nada a ver com alguma falha da própria técnica de prova. Um programa verificado pode satisfazer uma especificação escolhida incorretamente; exatamente a lacuna sobre a qual specifications-preconditions-postconditions-invariants alertou, em que uma prova da propriedade errada dá uma confiança mal colocada sobre a certa. Um modelo verificado, do mesmo modo, pode simplesmente omitir algum comportamento do mundo real que o sistema de fato implantado exibe; um modelo que nunca representa falhas de hardware, descompasso de relógios ou uma rede adversarial não prova nada sobre a resiliência de um sistema justamente a essas possibilidades omitidas. E um componente verificado pode falhar depois de implantado se o seu ambiente real violar as premissas em que a verificação se apoiou; uma prova de que uma função está correta dadas certas precondições não diz nada sobre o que acontece quando quem a chama, no sistema real implantado, viola essas precondições, seja por um bug próprio, seja por circunstâncias que a especificação nunca previu.

O verificador universal impossível

Um argumento direto e autocontido de por que não pode existir um verificador universal de terminação e correção, construído inteiramente a partir do Problema da Parada: suponha, por contradição, que alguma ferramenta V conseguisse decidir, para todo programa e toda entrada, se aquele programa termina naquela entrada. Essa ferramenta suposta poderia então ser usada para resolver diretamente o Problema da Parada: dado qualquer programa M e entrada w cujo comportamento de parada está em questão, basta entregar M e w a V e relatar a resposta que V der; V, pela hipótese da contradição, decide isso corretamente para todo programa e toda entrada, incluindo M e w. Mas o Problema da Parada já foi provado indecidível em Computabilidade e Complexidade, o que significa que nenhum algoritmo consegue resolvê-lo para todo programa e toda entrada. Uma ferramenta V que o decidisse para todo caso contradiria, portanto, um resultado de impossibilidade já estabelecido, então nenhuma V assim pode existir. Não é uma técnica de prova nova inventada para esta disciplina; é exatamente o estilo de argumento por redução que Computabilidade e Complexidade já usou repetidamente, agora aplicado para mostrar que a verificação de programas não consegue escapar da mesma indecidibilidade que governa as máquinas de Turing em geral, porque um verificador poderoso o bastante seria ele mesmo um decisor de parada.

Analisador correto com alarmes falsos

Considere um analisador estático tentando provar que um acesso a array a[i] é sempre seguro, dado só que os invariantes disponíveis do programa estabelecem i ≤ n (a mesma configuração já usada no exemplo resolvido de limites de array de smt-solvers-and-decision-procedures), mas em que o programa concreto real, por alguma combinação complexa de condições que a abstração escolhida pelo analisador não consegue representar com precisão, na verdade nunca chega a esse acesso com i = n. Como o analisador é correto e, portanto, se recusa a afirmar uma segurança que não consegue de fato derivar dos invariantes disponíveis, ele relata um possível acesso fora dos limites; um aviso que, neste caso específico, não corresponde a um bug real no programa de verdade, justamente porque a segurança genuína do programa real depende de uma relação que a superaproximação do analisador não foi precisa o bastante para capturar. É o custo direto e concreto da superaproximação descrito na seção de Teoria Central: o aviso é uma limitação da precisão da abstração escolhida, e não evidência de um defeito real, e a resposta honesta de uma ferramenta correta a "não consigo provar que isto é seguro" é dizer isso, em vez de adivinhar em silêncio que provavelmente é.

Verificador limitado

Considere um model checker limitado (bounded) explorando todo rastro de um sistema até o comprimento 20 e não encontrando contraexemplo em nenhum ponto dentro desse limite. Esse resultado genuinamente prova que a propriedade vale para todo rastro de comprimento 20 ou menos; isso é um fato real, correto e útil. Mas, sem um argumento adicional estabelecendo que rastros com mais de 20 passos não podem se comportar de outro jeito (um argumento indutivo, ou um limiar de completude específico do modelo mostrando que 20 passos já cobrem todo caso comportamentalmente distinto), o resultado não diz absolutamente nada, para um lado ou para o outro, sobre um bug que só se manifesta no passo 21 ou além. É exatamente o trade-off da subaproximação da seção de Teoria Central tornado concreto: a checagem é inteiramente correta dentro do limite enunciado e inteiramente silenciosa além dele, e tratar "nenhum contraexemplo em 20 passos" como equivalente a "nenhum contraexemplo, ponto" confunde um resultado limitado e honesto com um ilimitado que ele nunca afirmou ser.

• Interpretar a indecidibilidade como "a verificação é inútil". O Teorema de Rice exclui um único verificador universal e totalmente automático para propriedades não triviais arbitrárias de programas arbitrários; ele não diz nada contra as garantias corretas, muito reais, que as técnicas específicas e mais restritas desta disciplina entregam todo dia: bounded model checking dentro de um limite enunciado, condições de verificação cumpridas por SMT dentro de uma teoria decidível, provas em lógica de Hoare com um invariante fornecido por um humano. A indecidibilidade é uma fronteira para a universalidade, e não um veredicto contra o empreendimento inteiro.
• Interpretar uma prova bem-sucedida como "o sistema inteiro está correto". Uma prova estabelece exatamente a propriedade que mirava, para exatamente o modelo contra o qual foi checada; como a discussão sobre os limites da especificação deixa claro, isso deixa inteiramente em aberto se a especificação em si era a certa, se o modelo representa fielmente o sistema implantado e se o ambiente de implantação de fato satisfaz as premissas em que a prova se apoiou.
• Esconder premissas porque parecem inconvenientes ou minam a confiança no resultado. O valor real de um resultado de verificação vem especificamente de o seu escopo enunciado ser explícito e honesto (o limite de um verificador limitado, a fonte de alarmes falsos de um analisador que superaproxima, as premissas da base de confiança de um assistente de prova de theorem-proving-and-proof-assistants), e omitir esses detalhes para fazer um resultado soar mais impressionante do que é derrota todo o propósito dos métodos formais, que é substituir uma confiança vaga por garantias enunciadas com honestidade e escopo preciso.
• Comparar ferramentas sem antes perguntar se elas são corretas, completas, limitadas ou aproximadas. Duas ferramentas que relatam "nenhum bug encontrado" no mesmo programa podem significar coisas muito diferentes: uma pode ser uma prova correta e exaustiva, outra uma busca limitada que só cobriu parte do comportamento, e outra ainda um buscador de bugs que subaproxima e nunca afirmou checar a ausência; comparar as saídas delas pelo valor de face, sem antes estabelecer qual dessas garantias muito diferentes cada uma de fato oferece, é comparar coisas incomparáveis.

Os limites da verificação formal são matemáticos, e não apenas práticos ou temporários: o Teorema de Rice, generalizando o Problema da Parada, exclui um verificador automático universal para qualquer propriedade semântica não trivial de programas arbitrários, e é por isso que cada ferramenta de verificação real que esta disciplina construiu (prova em lógica de Hoare, resolução SAT e SMT, model checking, assistentes de prova) troca deliberadamente alguma combinação de automação, generalidade ou completude pela correção dentro de um escopo restrito e explicitamente enunciado. Além dessa fronteira matemática existe uma segunda limitação, igualmente real, que não tem nada a ver com indecidibilidade: mesmo uma prova totalmente correta de uma especificação totalmente correta pode deixar de entregar garantia no mundo real se a especificação, o modelo ou as premissas do ambiente de implantação estiverem errados. A resposta honesta da disciplina às duas limitações, presente em tudo o que foi construído aqui, não é recuar, mas ser preciso: enunciar exatamente o que foi provado, sobre exatamente que modelo, sob exatamente que premissas; e é exatamente essa disciplina que o conceito de capstone aplica a seguir, acompanhando um programa pequeno por uma prova em lógica de Hoare e por uma análise de model checking para tornar totalmente concreta cada uma dessas escolhas que definem o escopo.