Renaming or Tightness: Enforcing Disjunctive Information Flow Policies

Resumo Técnico: Renomeação ou Estreiteza: Impondo Políticas de Fluxo de Informação Disjuntiva

Problema
Políticas de fluxo de informação disjuntiva restringem um valor a depender de, no máximo, um de dois segredos, proibindo a combinação de liberações que seriam permitidas de outra forma (por exemplo, uma barreira ética impedindo que um relatório dependa tanto dos arquivos do Cliente A quanto do Cliente B, ou um esquema de compartilhamento de segredos liberando apenas uma parte). Diferente das políticas padrão baseadas em reticulados (lattices), onde o junção de duas dependências admissíveis é admissível, as políticas disjuntivas não possuem forma de reticulado. Hunt e Sands forneceram anteriormente uma semântica para essas políticas usando o "quantale da informação", onde a conjunção é um tensor não idempotente ($\otimes$) em vez de um junção (join). No entanto, a camada de imposição — especificamente, o que um sistema de tipos sensível ao fluxo pode certificar sobre essas políticas — permanecia um problema em aberto.

O desafio central é que os sistemas de tipos existentes sensíveis ao fluxo, que dependem de um objeto universal para permitir uma análise independente da política (via renomeação monótona), falham em preservar a precisão sob políticas disjuntivas. Especificamente, quando uma fonte é lida duas vezes (por exemplo, um resumo usado tanto em um cabeçalho quanto em uma tabela), os mecanismos padrão perdem a correlação de que ambas as leituras respeitam o mesmo disjunto. Consequentemente, eles superestimam o fluxo de informação, certificando que a saída revela ambos os segredos ($\top$) mesmo quando a política é satisfeita.

Metodologia
Os autores constroem uma família de sistemas de tipos sensíveis ao fluxo ($F_1$) sobre um quantale comutativo afim $M$ arbitrário. A análise procede investigando o "objeto universal" do qual todos os sistemas específicos de política se especializam. Na era dos reticulados, o conjunto das partes das variáveis servia como um único objeto universal. O artigo demonstra que, sobre um quantale, este objeto se divide em três candidatos distintos, cada um com propriedades diferentes em relação à precisão e à capacidade de suportar renomeação monótona:

1. O Objeto Multiset ($U_N$): O monoide comutativo livre sobre as variáveis (os elementos são multiset/multiconjuntos). Ele suporta renomeação monótona completa e tipagens principais, mas perde a "correlação de mesma fonte". Ele trata duas leituras de uma fonte como dois usos independentes, levando à superestimação ($\sigma(v) \otimes \sigma(v)$).
2. O Objeto Set ($U$): O monoide comutativo idempotente livre (elementos são conjuntos de variáveis, representados como downsets do conjunto das partes). Ele preserva a correlação de mesma fonte (duas leituras de uma fonte contam como uma) mas quebra a propriedade homomórfica necessária para a renomeação monótona. A especialização aqui é uma seção oplaxa, não um homomorfismo.
3. O Locale Livre ($L$): O objeto da era dos reticulados (conjuntos de variáveis com união como a combinação). É estreito para leituras únicas, mas confunde a disjunção de ramos com a combinação por tensor, apagando a distinção entre "a execução A usou X e a execução B usou Y" e "alguma execução usou X e Y".

O artigo analisa as trocas (trade-offs) entre esses objetos, provando que nenhum mecanismo da forma de "atributo independente" (onde os ambientes mapeiam variáveis para elementos únicos do quantale) pode simultaneamente suportar renomeação monótona e alcançar limites estreitos para políticas disjuntivas.

Contribuições Principais e Resultados

1. Família de Sistemas de Tipos ($F_1$): Uma família de sistemas de tipos sonora ancorada nos lemas de composição de Hunt e Sands. Ela lida com loops usando o fechamento idempotente do fator de guarda, um ajuste necessário para quantales que é invisível em reticulados.
2. A Divisão do Objeto Universal: O artigo estabelece uma tricotomia:
   • Sobre $U_N$, todo o mecanismo de tipagens principais e completude interna sobrevive incondicionalmente, mas o limite é frouxo para fontes reutilizadas.
   • Sobre $U$, o limite é estritamente mais preciso (registrando que duas leituras respeitam um único disjunto), mas a especialização não é mais um homomorfismo, quebrando a propriedade de renomeação.
   • Sobre $L$, o objeto perde a disjunção de ramos, falhando em distinguir entre execuções alternativas e execuções combinadas.
3. Impossibilidade de Renomeação e Estreiteza: Os autores provam que para qualquer mecanismo sonoro da forma de atributo independente que suporte renomeação monótona, o limite certificado para uma fonte reutilizada sob um rótulo "saturado" (onde $m \otimes m = \top$) é $\top$. Isso significa que, sob rótulos de barreira ética ou compartilhamento de segredos, uma segunda leitura de uma fonte não certifica nada, fazendo com que o mecanismo rejeite programas que na verdade satisfazem a política.
4. O Reparo (Especialização Adiada): Para recuperar a precisão, o artigo propõe adiar a especialização para o nível do julgamento. Em vez de aplicar o mapa de rotulagem ao ambiente (o que força uma estrutura homomórfica), o mapa é aplicado apenas à observação final (leitura).
   • Esta abordagem usa o Objeto Set ($U$) para a tipagem e o mapa $\alpha_\sigma$ para a leitura.
   • O mapa de leitura resultante é provado como sendo o mapa menor sound join-preserving (preservador de junção e mínimo para a sonoridade).
   • Este "reparo" sacrifica a capacidade de apresentar o resultado como uma derivação dentro do sistema alvo (renomeação), mas alcança o limite mais estreito possível para mecanismos de atributo independente.
5. Decidibilidade: O artigo mostra que a verificação de conformidade é decidível. Embora $U_N$ seja infinito, o limite especializado depende apenas de multiplicidades até a ordem do rótulo (por exemplo, 2 para barreiras éticas), permitindo truncamento finito. $U$ é um reticulado finito, garantindo a terminação.

Significância e Alegações
O artigo afirma que a transição de sistemas baseados em reticulados para sistemas baseados em quantales força uma escolha fundamental que era anteriormente oculta: pode-se ter renomeação monótona ou estreiteza, mas não ambos.

• Para o Paradigma de Renomeação: O artigo demonstra que a abordagem do "objeto universal", que permite analisar um programa uma única vez e reutilizar o resultado para qualquer política, atinge um teto duro. Para políticas disjuntivas, esse teto é tão baixo (frequentemente $\top$) que torna o mecanismo inútil para cenários comuns como compartilhamento de segredos ou barreiras éticas, onde um valor é usado múltiplas vezes.
• Para a Precisão: O artigo fornece uma solução construtiva (especialização adiada) que recupera a precisão perdida. Ele mostra que, ao manter o tipo universal no Objeto Set ($U$) e aplicar a rotulagem apenas ao final, é possível certificar programas que o paradigma de renomeação rejeita.
• Implicação Prática: A distinção entre "uma fonte lida duas vezes" (seguro sob políticas disjuntivas) e "duas fontes lidas uma vez" (inseguro) é preservada apenas pelo Objeto Set. O objeto multiset (amigável à renomeação) e o objeto locale (amigável aos reticulados) falham em distinguir esses casos corretamente no contexto de políticas disjuntivas.

Os autores concluem que, enquanto o objeto da era dos reticulados é um quociente que perde a disjunção de ramos, e o objeto multiset perde a correlação de mesma fonte, o Objeto Set ($U$) é o único que retém ambos. O custo dessa precisão é a perda da propriedade de renomeação, uma troca que é necessária para a imposição de políticas disjuntivas. O artigo não afirma resolver o problema para análias relacionais ou mecanismos sensíveis ao caminho (que são sugeridos como direções futuras em trabalhos relacionados), mas caracteriza plenamente os limites e as possibilidades da família de atributos independentes.