Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy

Resumo Técnico: Simplificação de Provas de Segurança com Raciocínio Forward-Backward e Profecia

1. O Problema

A verificação de propriedades de segurança em sistemas complexos (especialmente protocolos distribuídos) baseia-se frequentemente na descoberta de invariantes indutivos seguros. Um invariante indutivo seguro é uma propriedade que:

1. Vale nos estados iniciais.
2. É preservada por todas as transições do sistema.
3. Implica que nenhum estado "ruim" (de falha) é alcançável.

O principal desafio identificado pelos autores é a complexidade exponencial desses invariantes à medida que os sistemas crescem. Especificamente:

• Estrutura Booleana Complexa: Os invariantes necessários frequentemente exigem combinações complexas de conjunções e disjunções (fora da Forma Normal Conjuntiva - CNF), o que aumenta drasticamente o espaço de busca para síntese automática.
• Quantificadores e Alternâncias: Em lógica de primeira ordem, os invariantes podem exigir aninhamento de quantificadores e alternâncias (ex: $\exists \forall$), tornando a validação da indução indecidível ou computacionalmente proibitiva para solvers SMT.
• Limitações das Abordagens Atuais: Métodos modulares (como assume-guarantee) dividem o sistema, mas falham quando um único componente exige provas intrinsecamente complexas. Métodos puramente forward (para frente) muitas vezes não conseguem encontrar invariantes simples o suficiente para automatizar a prova.

2. Metodologia Proposta

Os autores propõem uma abordagem de provas incrementais que decompõe uma prova complexa em uma sequência de passos mais simples, combinando três técnicas principais:

A. Raciocínio Forward-Backward (Para Frente e Para Trás)

• Em vez de apenas acumular invariantes que valem para todos os estados alcançáveis forward (a partir do estado inicial), o sistema permite acumular propriedades de estados que aparecem em traces de erro (caminhos hipotéticos de um estado inicial a um estado ruim).
• Passos Forward: Usam invariantes indutivos padrão ($\text{init} \Rightarrow \varphi$ e $\varphi \land \tau \Rightarrow \varphi'$).
• Passos Backward: Usam invariantes indutivos de um sistema com tempo reverso. Um predicado $\varphi$ é um invariante backward se vale nos estados ruins e é preservado ao reverter as transições ($\beta \Rightarrow \varphi$ e $\varphi' \land \tau \Rightarrow \varphi$).
• Sinergia: A combinação permite usar predicados auxiliares que podem não ser verdadeiros em estados alcançáveis forward nem em estados alcançáveis backward isoladamente, mas que são verdadeiros em todos os caminhos de erro. Isso frequentemente simplifica a estrutura booleana (ex: eliminando disjunções complexas).

B. Profecia (Prophecy)

• Introduzida para lidar com a complexidade dos quantificadores.
• A ideia é adicionar um símbolo de testemunha (constante fresca $w$) ao sistema que "profetiza" a existência de um elemento que satisfaz uma propriedade ao longo de toda a execução.
• Em vez de provar $\exists x. \varphi(x)$, o sistema prova $\varphi(w)$, onde $w$ é um símbolo fixo.
• Condição de Soberania (Soundness): Para garantir que a adição da profecia não introduza falsos positivos, deve-se provar que, para qualquer trace de erro do sistema original, existe uma interpretação para $w$ que satisfaz a profecia. Isso é formalizado como um problema de segurança auxiliar.
• Benefício: A profecia permite eliminar alternâncias de quantificadores e aninhamentos, transformando invariantes complexos em conjunções de cláusulas universalmente quantificadas.

C. Sistema de Prova Incremental
O sistema de prova (denotado como FBPI) permite alternar entre:

1. Adicionar invariantes forward.
2. Adicionar invariantes backward (via reversão temporal).
3. Adicionar profecias (via regra Proph).
   Cada passo fortalece o problema de segurança, permitindo que o próximo passo seja provado com predicados mais simples.

3. Contribuições Principais

1. Sistema de Prova Unificado: Definição formal de um sistema de prova incremental que combina raciocínio forward, backward e profecia de maneira sinérgica.
2. Caracterização de Soberania: Uma caracterização completa e verificável da soberania de uma profecia, reduzindo a verificação da profecia a um problema de segurança auxiliar (verificável por indução).
3. Tradução para Invariantes Únicos: Demonstração teórica de que qualquer prova incremental forward-backward com profecia pode ser convertida em um único invariante indutivo seguro para o problema original. Isso prova que o método é completo e não perde poder expressivo, apenas simplifica a busca.
4. Aumento do Poder de Prova: Prova teórica de que, sob restrições naturais no conjunto de fórmulas disponíveis, cada regra (forward, backward, profecia) aumenta estritamente o poder de prova. Existem problemas prováveis com este método que não possuem invariantes seguros dentro do mesmo conjunto de fórmulas usando apenas métodos tradicionais.
5. Estudo de Caso em Protocolos Reais: Aplicação prática em variantes do protocolo Paxos e Raft.

4. Resultados e Estudo de Caso

Os autores aplicaram sua metodologia em várias variantes do Paxos (Single-Decree, Flexible, Multi, Fast) e no Raft, utilizando a ferramenta mypyvy.

• Simplificação Booleana:
  • Provas puramente forward exigiam invariantes com estruturas booleanas complexas (mistura de $\land$ e $\lor$) e não-clausais.
  • Provas forward-backward conseguiram decompor esses invariantes em conjunções de cláusulas puramente universais (CNF), reduzindo drasticamente o espaço de busca.
• Eliminação de Quantificadores:
  • Em casos onde invariantes forward exigiam alternância de quantificadores (ex: $\exists \forall$), o uso de profecia permitiu eliminar a alternância, resultando em invariantes puramente universalmente quantificados.
  • Exemplo: No Paxos, a profecia permitiu "selecionar" um quórum específico (testemunha) no início da prova, permitindo que o passo backward verificasse propriedades apenas sobre esse quórum específico, sem necessidade de quantificadores existenciais complexos.
• Desempenho:
  • A tabela de resultados mostra que o tempo de verificação para exemplos complexos (como Fast Paxos e Raft) foi reduzido significativamente (ex: de 1.5s para 0.8s em Fast Paxos, e de 3.7s para 2.8s em Raft).
  • Para exemplos mais simples, o tempo foi mantido ou ligeiramente reduzido, demonstrando que a abordagem não impõe sobrecarga desnecessária.
• Descoberta Chave: A interação entre o passo backward e a profecia é crucial. O passo backward pode identificar qual testemunha (profecia) é necessária para simplificar o passo forward subsequente.

5. Significado e Impacto

• Automação de Verificação: Ao reduzir a complexidade booleana e a profundidade de quantificadores dos invariantes necessários, a abordagem torna viável a síntese automática de provas para protocolos que anteriormente eram intratáveis ou exigiam intervenção manual extensiva.
• Novidade Teórica: A combinação de análise forward-backward com variáveis de profecia é apresentada como uma contribuição original. Enquanto variáveis de história e profecia são conhecidas, sua interação sinérgica com a reversão temporal para simplificar a estrutura de invariantes é um avanço novo.
• Generalidade: Embora focado em protocolos de consenso, a metodologia é geral e pode ser aplicada a outros sistemas de transição com lógica de primeira ordem.
• Ferramental: O trabalho foi implementado e validado na ferramenta mypyvy, com todos os códigos e artefatos disponíveis publicamente, facilitando a adoção pela comunidade de verificação.

Em resumo, o artigo demonstra que dividir a prova em passos incrementais, alternando a direção do raciocínio e introduzindo testemunhas de profecia, permite provar a segurança de sistemas complexos usando fórmulas logicamente muito mais simples do que as exigidas por métodos tradicionais de invariante único.