Model checking of hyperproperties for high-level relational models

Resumo Técnico: Verificação de Modelos de Hiperpropriedades para Modelos Relacionais de Alto Nível

Enunciação do Problema
Muitas propriedades críticas de sistemas, particularmente aquelas relacionadas à segurança (por exemplo, não-interferência, não-interferência generalizada) e concorrência (por exemplo, linearizabilidade), são hiperpropriedades. Diferentemente das propriedades de traço tradicionais que raciocinam sobre uma única execução, as hiperpropriedades exigem raciocínio sobre relações entre múltiplos traços de execução. Embora avanços recentes tenham produzido verificadores de modelos para hiperlógicas como HyperLTL, essas ferramentas tipicamente operam em formatos de baixo nível, legíveis por máquina (por exemplo, fragmentos SMV, autômatos). Isso cria uma lacuna significativa para profissionais de engenharia de software: há uma falta de linguagens de especificação de alto nível que permitam a modelagem natural de designs de sistemas, ao mesmo tempo em que suportam a verificação automática de hiperpropriedades. Ferramentas existentes frequentemente exigem que os usuários traduzam manualmente conceitos de alto nível em máquinas de estado de baixo nível ou fornecem contraexemplos em formatos (por exemplo, saídas brutas de QBF) que são difíceis de interpretar.

Metodologia
Os autores propõem HyperPardinus, um procedimento de descoberta de modelos que estende Pardinus (o backend de lógica temporal da linguagem Alloy) para suportar a verificação automática de hiperpropriedades sobre modelos relacionais. A abordagem envolve um pipeline de duas fases:

1. Modelagem de Alto Nível e Tradução (HyperPardinus):

   • Os autores introduzem uma extensão mínima à linguagem Alloy 6, adicionando uma palavra-chave trace a assinaturas. Isso permite que assinaturas representem traços de execução, habilitando a quantificação sobre múltiplos traços dentro de uma única especificação.
   • O HyperPardinus formaliza o problema da Descoberta de Modelo Relacional Hiper. Ele recebe uma especificação Alloy de alto nível e a traduz em um conjunto de máquinas de estado SMV (Symbolic Model Verifier) de baixo nível e uma fórmula HyperLTL.
   • O algoritmo de tradução converte as restrições de lógica temporal relacional em uma forma normal prenex, separando quantificadores de traço do fragmento não-hiper. Ele gera modelos SMV para cada traço quantificado e codifica a hiperpropriedade como uma fórmula HyperLTL sobre esses modelos.
   • Otimizações chave são aplicadas durante a tradução, incluindo composição de quantificadores (mesclando quantificadores sequenciais do mesmo tipo para reduzir o número de traços), exploração de restrições de multiplicidade (usando variáveis inteiras em vez de codificações booleanas para reduzir o espaço de estados) e quebra de simetria.

2. Verificação de Baixo Nível (HyperSMV):

   • Os modelos SMV gerados e as fórmulas HyperLTL são processados pelo HyperSMV, uma nova ferramenta de verificação de modelos projetada para lidar com os desafios específicos das traduções Alloy de alto nível.
   • O HyperSMV suporta dois backends:
     • Estado Explícito (Exp): Converte modelos SMV em sistemas de estado explícito (Autômatos de Büchi Não-Determinísticos) e utiliza solucionadores baseados em autômatos (por exemplo, AutoHyper, forklift, ROLL). Inclui otimizações para compressão de fórmulas e redução por bisimulação.
     • Simbólico (Sym): Converte modelos e fórmulas em Fórmulas Booleanas Quantificadas (QBF) usando técnicas de desenrolamento, aproveitando solucionadores QBF prontos (por exemplo, Quabs, qute).
   • Uma característica crítica do HyperSMV é sua capacidade de rastrear testemunhas. Ele traduz saídas do solucionador (que são frequentemente traços de baixo nível ou atribuições QBF) de volta para traços SMV legíveis e, finalmente, para instâncias relacionais de alto nível visualizadas pelo Alloy Analyzer.

Principais Contribuições

• HyperPardinus: A primeira ferramenta de verificação de modelos para uma hiperlógica de primeira ordem. Estende o ecossistema Alloy para suportar a especificação e verificação automática de hiperpropriedades com alternâncias flexíveis de quantificadores de traço.
• HyperSMV: Um verificador de modelos SMV robusto que integra solucionadores de última geração de estado explícito e simbólico. Melhora significativamente a expressividade dos modelos SMV suportados (lidando com estilos declarativos e variáveis inteiras) e a escalabilidade do processo de verificação.
• Extensão do Alloy: Uma extensão mínima e compatível com versões anteriores ao Alloy 6 que permite aos usuários especificar hiperpropriedades de forma declarativa e visualizar contraexemplos em um alto nível de abstração.
• Avaliação: Uma avaliação abrangente usando benchmarks diversos, incluindo sistemas de gerenciamento de conferências (CMS), síntese de caminhos robóticos, testes de mutação e linearizabilidade de estruturas de dados concorrentes (SNARK).

Resultados
A avaliação aborda quatro perguntas de pesquisa sobre viabilidade, usabilidade, eficácia de otimização e desempenho:

• Expressividade e Usabilidade: A abordagem modela com sucesso hiperpropriedades complexas (por exemplo, linearizabilidade, não-interferência) em Alloy de alto nível. Os autores demonstram que os modelos Alloy são significativamente mais legíveis e mantíveis do que suas contrapartes SMV de baixo nível, que frequentemente exigem scripts extensos para geração.
• Visualização de Contraexemplos: Diferentemente de ferramentas existentes que fornecem saídas brutas de QBF ou traços SMV de baixo nível, o HyperPardinus fornece contraexemplos relacionais de alto nível, mínimos e visualizados no Alloy Analyzer. Por exemplo, no benchmark SNARK, a ferramenta identificou um erro e forneceu uma instância gráfica de 9 estados, enquanto ferramentas de última geração produziram traços extensos e ilegíveis.
• Impacto das Otimizações: As otimizações no HyperPardinus (composição de quantificadores, quebra de simetria, restrições de multiplicidade) foram cruciais para a viabilidade do backend de estado explícito. Sem elas, muitos modelos (por exemplo, variantes de CMS, exemplos de Robô) excederam o tempo limite ou falharam ao gerar máquinas de estado.
• Desempenho:
  • Modelos de Alto Nível: O HyperSMV superou ferramentas de última geração (AutoHyper, HyperQB) em modelos Alloy de alto nível, frequentemente resolvendo-os em segundos onde outras ferramentas excederam o tempo limite.
  • Modelos de Baixo Nível: Quando aplicado a benchmarks SMV padrão (traduzidos para Alloy e de volta), o HyperSMV mostrou desempenho competitivo, replicando resultados esperados com eficiência comparável ou superior.
  • Simbólico vs. Explícito: O backend simbólico (Sym) performou bem na descoberta de erros (encontrando contraexemplos), mas frequentemente produziu resultados inconclusivos para propriedades universais devido às limitações da semântica de verificação de modelos limitada (BMC). O backend explícito (Exp) foi mais eficaz para verificação exaustiva de escopos menores.

Significado e Afirmações
O artigo afirma que o HyperPardinus preenche a lacuna entre o design de software de alto nível e a verificação de hiperpropriedades. Ao permitir que profissionais especifiquem e verifiquem hiperpropriedades diretamente em uma linguagem relacional de alto nível (Alloy), a abordagem elimina a necessidade de tradução manual para formatos de baixo nível. Os autores afirmam que isso torna a verificação de hiperpropriedades acessível a uma comunidade mais ampla de engenharia de software.

O trabalho é modesto quanto ao seu escopo: não afirma resolver todas as questões de decidibilidade em hiperlógicas, mas sim demonstra um pipeline prático para analisar modelos complexos de alto nível que anteriormente eram intratáveis ou inutilizáveis com ferramentas existentes. O significado reside na usabilidade (especificação e visualização de alto nível) e na viabilidade de verificar cenários complexos (como linearizabilidade com quantificadores alternados) que anteriormente estavam restritos a abordagens de baixo nível, manuais ou dedutivas. Os autores observam que a abordagem depende de formatos padrão, garantindo que se beneficiará de melhorias futuras em verificadores de modelos de baixo nível.