Resumo Técnico: Lógica de Incorreção Suficiente (SIL) e Separação SIL

1. Definição do Problema

Os métodos formais para verificação de programas historicamente basearam-se em técnicas de sobre-aproximação (ex: Lógica de Hoare, Interpretação Abstrata) para garantir a ausência de erros. Embora consistentes (sound), esses métodos inevitavelmente produzem alarmes falsos (erros espúrios), o que pode dificultar a adoção por programadores. Por outro lado, métodos de sub-aproximação (ex: Lógica de Incorreção, Verificação de Modelo Limitada) são projetados para a busca de bugs e são livres de alarmes falsos, pois apenas relatam estados de erro alcançáveis. No entanto, as lógicas de sub-aproximação existentes, como a Lógica de Incorreção (IL), focam primariamente em provar a existência de um erro alcançável a partir de uma pré-condição. Elas não caracterizam necessariamente o conjunto de estados iniciais que levam a tais erros.

O artigo identifica uma lacuna no raciocínio sobre as fontes da incorreção. Programadores precisam saber não apenas que um bug existe, mas especificamente quais estados de entrada o causam, para escalar efetivamente a depuração e os testes. Embora as "triplas de Lisboa" (sub-aproximações retroativas) tenham sido discutidas anteriormente no contexto da Lógica de Resultado (OL), faltava um sistema de prova dedicado, minimalista e completo especificamente para inferir pré-condições suficientes para erros.

2. Metodologia

Os autores introduzem a Lógica de Incorreção Suficiente (SIL), uma nova lógica de triplas baseada em programas projetada para sub-aproximação retroativa (backward under-approximation).

2.1 Conceito Central: Triplas SIL

Uma tripla SIL é denotada como $\langle\langle P \rangle\rangle r \langle\langle Q \rangle\rangle$.

• Semântica: A tripla é válida se, e somente se, a semântica de coleta retroativa do programa $r$ aplicada ao conjunto de estados de erro $Q$ contém o conjunto de estados iniciais $P$. Formalmente: $J \leftarrow r K (Q) \supseteq P$.
• Interpretação: "Todos os estados de entrada que satisfazem $P$ possuem pelo menos uma execução de $r$ levando a um estado que satisfaz $Q$."
• Distinção da IL: Enquanto a IL ($[P] r [Q]$) garante que algum estado em $Q$ é alcançável a partir de algum estado em $P$, a SIL garante que cada estado em $P$ pode alcançar um erro em $Q$. Isso torna $P$ uma condição suficiente para a incorreção.

2.2 Sistema de Prova

O artigo define um conjunto minimal de regras de prova para a SIL (Figura 7) que são tanto consistentes (sound) quanto completas para comandos regulares (incluindo não-determinismo e loops).

• Semântica Retroativa: As regras são derivadas da semântica retroativa dos comandos (ex: atribuição usa substituição retroativa).
• Regra de Consequência: A regra $\langle\langle \text{cons} \rangle\rangle$ permite o fortalecimento da pré-condição e o enfraquecimento da pós-condição, facilitando a sub-aproximação.
• Tratamento de Loops: A lógica inclui regras para iteração ($\langle\langle \text{iter} \rangle\rangle$) e regras adicionais como $\langle\langle \text{iter0} \rangle\rangle$ (pular o loop) e $\langle\langle \text{unroll} \rangle\rangle$ (desenrolar uma vez) para suportar análise prática sem exigir invariantes de loop para terminação.
• Disjunção: Ao contrário da Lógica de Hoare, a SIL permite descartar disjuntos nas pré-condições (via $\langle\langle \text{choice} \rangle\rangle$ e $\langle\langle \text{disj} \rangle\rangle$), o que é crucial para a escalabilidade na sub-aproximação.

2.3 Separação SIL

Para lidar com ponteiros e alocação dinâmica de memória, os autores instanciam a SIL com fórmulas de Lógica de Separação, criando a Separação SIL.

• Linguagem de Asserção: Combina a Lógica de Separação padrão (separação de heap, points-to) com a asserção $x \not\mapsto$ (indicando um ponteiro desalocado), adaptada da Lógica de Separação de Incorreção (ISL).
• Regras: Inclui regras retroativas para operações de heap (alloc, free, load, store) e uma regra de quadro (frame rule) ($\langle\langle \text{frame} \rangle\rangle$) para permitir o raciocínio local sobre erros de memória.
• Completude: O sistema é provado consistente. Para programas sem loops, demonstra-se que ele é relativamente completo (assumindo um oráculo para implicação entre asserções).

3. Principais Contribuições

1. Introdução da SIL: Uma nova lógica de triplas de incorreção suficiente que identifica as fontes de erros (estados iniciais) em vez de apenas a existência de bugs.
2. Taxonomia Formal: O artigo constrói uma taxonomia de lógicas baseadas em triplas (Figura 3) baseada em dois eixos:
   • Direção da Semântica: Direta/Forward (Lógica de Hoare, IL) vs. Retroativa/Backward (SIL, Condições Necessárias).
   • Tipo de Aproximação: Sobre-aproximação (Lógica de Hoare, Condições Necessárias) vs. Sub-aproximação (IL, SIL).
   • Esta taxonomia esclarece que a SIL é a combinação única de semântica retroativa e sub-aproximação.
3. Análise Comparativa:
   • SIL vs. IL: A IL encontra que um erro é alcançável; a SIL encontra quais entradas o causam. Elas não são logicamente equivalentes.
   • SIL vs. Lógica de Hoare (HL): Para programas determinísticos e terminantes, a SIL e a HL coincidem (interpretando a pós-condição como estados de erro). Para programas não-determinísticos, elas divergem.
   • SIL vs. Condições Necessárias (NC): Os autores provam que a NC é isomorfa à HL (via dupla negação) mas não é comparável à IL ou SIL no caso geral.
   • SIL vs. Lógica de Resultado (OL): Embora a OL possa expressar triplas SIL (especificamente o padrão "Lisbon"), os autores argumentam que o sistema de prova da SIL é mais direto e natural para inferir pré-condições a partir de especificações de erro, particularmente no tratamento de disjunções e raciocínio retroativo.
4. Separação SIL: Uma instanciação consistente e relativamente completa para erros de memória, demonstrando que a sub-aproximação retroativa pode gerar pós-condições mais sucintas e garantias mais fortes do que a ISL em casos específicos (ex: fornecendo testemunhas reais para testes).

4. Resultados

• Correção e Completude: O conjunto minimal de regras da SIL é provado consistente e completo para comandos regulares.
• Completude Relativa: A Separação SIL é provada relativamente completa para programas sem loops.
• Relevância Industrial: O artigo argumenta que a SIL fornece uma justificativa formal a posteriori para as estratégias de análise retroativa usadas em ferramentas industriais na Meta (Zoncolan, Mariana Trench, Pysa), que inferem pré-condições de incorreção suficiente para detectar bugs de segurança.
• Exemplos de Derivação: O artigo fornece derivações detalhadas (ex: para um programa cliente envolvendo free e alloc) mostrando como a Separação SIL pode derivar pré-condições que garantem que um erro ocorra, ofereando um caminho mais direto para a depuração do que lógicas orientadas para frente.

5. Significância e Alegações

O artigo alega que a SIL preenche uma lacuna teórica crítica ao fornecer um framework de sub-aproximação orientado para trás. Sua significância reside em:

• Precisão para Depuração: Ao identificar o conjunto exato de estados de entrada que levam a erros, a SIL suporta o "raciocínio retroativo" que é mais natural para desenvolvedores tentando entender por que um bug ocorre, comparado a sub-aproximações diretas que apenas mostram que um bug é alcançável.
• Unificação Teórica: Esclarece o panorama das lógicas de programa, mostrando que, embora exista dualidade entre a Lógica de Hoare e as Condições Necessárias, tal dualidade simples não existe entre a Lógica de Incorreção e a Lógica de Incorreção Suficiente.
• Utilidade Prática: Os autores argumentam que a Separação SIL pode produzir pós-condições mais sucintas e garantias mais fortes do que a Lógica de Separação de Incorreção (ISL) para testes e depuração, pois garante que cada estado na pré-condição leva ao erro, fornecendo testemunhas concretas.

O artigo conclui que nenhuma lógica é "melhor"; em vez disso, cada uma (HL, IL, NC, SIL) serve a um propósito específico. A SIL é posicionada especificamente como a ferramenta de escolha quando o objetivo é localizar as fontes de incorreção para guiar os esforços de depuração e teste.