Security Engineering in IIIf, Part II -- Shadowing the IIIf

Resumo Técnico: Shadowing the Isabelle Insider and Infrastructure Framework

Problema
O Isabelle Insider and Infrastructure Framework (IIIf) fornece uma base formal para a engenharia de segurança de sistemas que envolvem atores humanos, políticas e componentes físicos/lógicos, utilizando um ciclo de Refinamento-Risco (RR). Embora o IIIf suporte o refinamento baseado em traços e a preservação de propriedades para propriedades de segurança padrão (ex: alcançabilidade), ele enfrenta uma limitação crítica em relação ao Controle de Fluxo de Informação (IFC). Especificamente, a propriedade de Não-interferência (NI) — que garante que estados de alta segurança (secretos) não influenciem observações de baixa segurança (públicas) — não é geralmente preservada sob o refinamento de especificação. Este fenômeno, conhecido como o "paradoxo do refinamento", significa que uma especificação que satisfaz NI pode resultar em uma implementação refinada que vaza informações através de fluxos implícitos. As abordagens de verificação de modelos existentes dentro do IIIf são insuficientes para verificar tais propriedades de conjunto de traços, necessitando de uma nova metodologia para caracterizar e garantir refinamentos seguros.

Metodologia
Para abordar o paradoxo do refinamento, o artigo introduz uma formalização do conceito de "Shadow" (Sombra) de Morgan para o framework IIIf. A metodologia procede através dos seguintes passos:

1. Integração de Estudo de Caso: Os autores utilizam uma especificação de sistema de radar de voo (previamente formalizada no IIIf) como um exemplo contínuo. Este sistema envolve posições de aeronaves, rotas e locais críticos. A especificação inicial demonstra como fluxos de informação implícitos ocorrem quando uma aeronave contorna um local crítico, revelando a existência dessa criticidade através de irregularidades observáveis na trajetória de voo.
2. Formalizando a Não-interferência (NI): A NI é definida dentro do IIIf como uma relação de indistinguibilidade sobre transições de estado. Dois estados são indistinguíveis para um atacante (com nível de autorização $a$) se seus componentes observáveis (aqueles com rótulos de segurança $\leq a$) forem idênticos. A NI ocorre se, para qualquer par de estados iniciais indistinguíveis, seus traços de execução subsequentes permanecerem indistinguíveis.
3. Definindo a Sombra (Shadow): Inspirado na lógica epistêmica de Morgan, uma "Sombra" é definida como o conjunto de todos os valores possíveis que um componente de estado de segurança crítica poderia assumir do ponto de vista do atacante.
   • Inicialização: Um componente de sombra é inicializado com o "universo" de seu tipo (todos os valores possíveis), representando ignorância máxima.
   • Encolhimento (Shrinking): Durante as transições de estado, a sombra "encolhe" (reduz o conjunto de valores possíveis) apenas se a transição revelar informações sobre o componente secreto ao atacante.
   • Invariante: Um sistema seguro deve satisfazer o invariante $IFC_a$, onde a sombra de um componente secreto não encolhe durante a execução. Se a sombra encolher, isso implica que o atacante obteve conhecimento sobre o segredo, indicando uma violação de NI.
4. Prova de Equivalência: O artigo estabelece formalmente (no papel, devido aos limites de quantificação de tipos em Higher Order Logic) que o invariante de sombra $IFC_a$ é equivalente à Não-interferência ($NI_a$). Especificamente, a negação da NI (existência de um fluxo de informação ilícito) é mostrada como equivalente à existência de um componente cuja sombra encolhe.
5. Caracterização de Refinamento Seguro: Os autores definem uma condição para refinamento seguro. Um refinamento de um sistema abstrato $A$ para um sistema concreto $C$ preserva a segurança se o mapa de refinamento $E$, quando restrito aos componentes de sombra de $C$, for injetivo e compatível com a sombra abstrata.

Principais Contribuições

• Formalização da Sombra no IIIf: O artigo estende o IIIf com uma definição formal de componentes de "Sombra" para estados de infraestrutura, permitindo o rastreamento da incerteza de um atacante em relação a componentes de estado secretos.
• Equivalência entre Sombra e NI: Prova que o invariante de sombra ($IFC_a$) é equivalente à propriedade de Não-interferência ($NI_a$) dentro do contexto do modelo de transição de estado do IIIf.
• Teorema de Refinamento Seguro (Teorema 2): A principal contribuição é um teorema que caracteriza o refinamento seguro. Ele afirma que, se um mapa de refinamento $E$ for injetivo nos componentes de sombra do sistema concreto e compatível com a sombra abstrata, então o invariante de sombra (e, portanto, a NI) é preservado do sistema abstrato para o sistema concreto.
• Resolução do Paradoxo do Refinamento: A metodologia fornece um mecanismo para verificar se um passo de refinamento introduz novos fluxos de informação que violariam a NI, abordando uma falha conhecida no ciclo RR padrão do IIIf.

Resultados

• Aplicação ao Sistema de Radar de Voo: Os autores aplicam a definição de sombra ao estudo de caso do sistema de radar de voo.
  • Em uma versão insegura (sem mecanismos de ocultação), a sombra do componente de localização crítica encolhe quando um avião contorna uma área crítica, provando a violação de $IFC_a$ e NI.
  • Em uma versão segura (usando um componente critpos para ocultar o desvio real), o invariante de sombra é mantido, confirmando a ausência de fluxos ilícitos.
• Análise de Refinamento: O artigo demonstra que adicionar um novo componente (ex: "velocidade") calculado com base em posições ocultas constitui um refinamento inseguro porque faz com que a sombra encolha, violando as condições de injetividade/compatibilidade do Teorema 2. Inversamente, mostra que adicionar componentes que não dependem de segredos e que são tratados corretamente pelo mapa de refinamento preserva a segurança.
• Limites Meta-Teóricos: Os autores observam que, embora a equivalência entre Sombra e NI possa ser raciocinada, a formalização completa da prova de equivalência sobre todos os tipos de infraestrutura é limitada pelo sistema de tipos do Isabelle/HOL, pois requer a quantificação sobre componentes de tipos diferentes do estado.

Significância e Alegações
O artigo alega estender as capacidades de engenharia de segurança do framework IIIf integrando o Controle de Fluxo de Informação. Sua significância reside em:

1. Abordar o Paradoxo do Refinamento: Oferece uma metodologia concreta para garantir que as propriedades de segurança (especificamente NI) sejam preservadas durante o processo de refinamento, uma capacidade anteriormente ausente no framework.
2. Unir Abstração e Implementação: Ao usar o conceito de sombra, o framework agora pode raciocinar formalmente sobre a "ignorância" de um atacante e garantir que os refinamentos não reduzam inadvertidamente essa ignorância (ou seja, vazem informações).
3. Verificação Prática: A abordagem permite a verificação de sistemas complexos e heterogêneos (combinando aspectos físicos e lógicos) onde a verificação de modelos padrão falha.

Os autores permanecem modestos quanto ao escopo, reconhecendo que as provas de equivalência são atualmente estabelecidas "no papel" devido a restrições de tipagem no Isabelle/HOL, e que a metodologia é especificamente adaptada ao modelo de infraestrutura do IIIf, em vez de uma lógica de linguagem de programação de propósito geral. O trabalho baseia-se nos conceitos fundamentais de Morgan, mas os adapta a um sistema de transição de estado com atores e políticas explícitos, evitando a necessidade de uma lógica epistêmica dedicada ao aproveitar o modelo de direitos de acesso de atores já existente no IIIf.