Verification of Robust Properties for Access Control Policies

Resumo Técnico: Verificação de Propriedades Robustas para Políticas de Controle de Acesso

1. O Problema

A verificação automática de políticas de controle de acesso (como as baseadas em XACML) tradicionalmente assume que a política está completa e totalmente determinada antes que a verificação possa ocorrer. No entanto, na prática, as políticas são desenvolvidas de forma iterativa, compostas por componentes mantidos independentemente e estendidas conforme a estrutura organizacional evolui.

As abordagens existentes (baseadas em modelos, como SMT ou BDDs, ou baseadas em lógica, como Programação em Conjuntos de Respostas - ASP) enfrentam limitações críticas neste cenário:

• Dependência de Completude: Elas exigem que todas as decisões pendentes (ex: atribuições de funções não finalizadas) sejam resolvidas para gerar um modelo ou um "modelo estável".
• Não Composicionalidade: Se uma política é estendida ou uma decisão pendente é resolvida, a verificação anterior torna-se inválida e deve ser refeita do zero.
• Incapacidade de Raciocínio sobre o Futuro: Elas não conseguem determinar se uma propriedade de segurança é garantida pela estrutura da política, independentemente de como as decisões pendentes serão resolvidas no futuro.

O artigo propõe resolver a lacuna de verificar propriedades robustas: restrições de segurança que são garantidas pela estrutura inferencial da política, independentemente de como as decisões pendentes sejam resolvidas ou de como a política seja estendida posteriormente.

2. Metodologia e Framework Semântico

Os autores introduzem um framework baseado em Semântica de Extensão de Base (Base-Extension Semantics), uma forma de semântica proof-theoretic (baseada na prova).

• Julgamento de Suporte ($\Vdash_P \phi$): O núcleo do framework é um julgamento que afirma que a política $P$ possui a propriedade robusta $\phi$. Diferente da verdade em um modelo estático, este julgamento avalia o comportamento inferencial da política através de todas as suas possíveis extensões futuras.
• Extensão de Política ($Q \supseteq P$): Uma política $Q$ é uma extensão de $P$ se contém todas as regras de $P$ mais novas regras. O framework quantifica universalmente sobre todas as extensões possíveis.
• Conectivos Lógicos Robustos: O artigo define conectivos específicos para capturar diferentes aspectos do raciocínio robusto:
  • Implicação ($\Rightarrow$): Garante que, se $\phi$ for estabelecido em qualquer extensão futura, $\psi$ também será. É um condicional inferencial, não material.
  • Disjunção Robusta ($\oplus$): Permite raciocinar sobre alternativas pendentes (ex: "Alice, Bob ou Carol serão o chefe"). A propriedade é válida se as consequências de segurança forem as mesmas, independentemente de qual alternativa for escolhida, sem precisar comprometer-se com uma escolha específica.
  • Conjunção Robusta ($\otimes$): Garante que múltiplas propriedades de segurança sejam mantidas simultaneamente e que suas consequências conjuntas sejam deriváveis, evitando falhas que só aparecem quando as regras são combinadas.
  • Negção ($\neg$): Definida como a implicação para a "corrupção" da política (o estado onde todas as fórmulas atômicas são deriváveis, quebrando o controle de acesso). $\neg \phi$ significa que $\phi$ é estruturalmente incompatível com a política.

3. Contribuições Principais

1. Identificação do Problema: Formalização da "verificação de propriedades robustas" como um problema proof-theoretic, distinto da verificação tradicional baseada em modelos completos.
2. Definição Semântica: Introdução do julgamento de suporte $\Vdash_P \phi$ com conectivos ($\Rightarrow, \oplus, \otimes, \neg$) que satisfazem três requisitos:
   • Inferencial: Baseado na estrutura de derivação, não em modelos de estado completo.
   • Composicional: Propriedades verificadas persistem sob extensão da política (Teorema da Monotonicidade).
   • Finitário: Apesar de quantificar sobre um conjunto infinito de extensões, o processo de verificação é decidível.
3. Redução Computacional: Demonstração de que a verificação de propriedades robustas pode ser reduzida à busca de prova (proof-search) em uma linguagem de programação lógica de segunda ordem.
4. Teoremas de Corretude: Prova de Sonsseza e Completude para a redução entre o julgamento semântico e a execução lógica.

4. Resultados e Mecanismo de Computação

O artigo demonstra que, embora a definição semântica envolva quantificação universal sobre todas as extensões de política (um conjunto infinito), essa complexidade pode ser colapsada para uma execução prática:

• Codificação de Objetivos: As propriedades robustas são codificadas em objetivos de lógica de programação (usando uma linguagem de cláusulas de Horn estendida com quantificadores de segunda ordem sobre átomos).
• Mapeamento Operacional:
  • A quantificação universal sobre extensões é realizada operacionalmente através da regra Generic (introdução de variáveis eigen/frescas) na busca de prova uniforme.
  • A disjunção robusta e a conjunção robusta são mapeadas para formas de eliminação de segunda ordem (estilo continuations-passing style).
• Teorema 12 (Sonsseza e Completude): Estabelece que $\Vdash_P \phi$ se e somente se o programa lógico $P$ prova o objetivo codificado $\lceil \phi \rceil$ ($P \vdash_O \lceil \phi \rceil$).
• Eficiência: Isso transforma um problema de verificação teoricamente infinita em um procedimento de busca de prova finito e executável em sistemas de programação lógica padrão (como $\lambda$Prolog ou Twelf).

5. Significado e Impacto

• Mudança de Paradigma: O trabalho desloca o foco da verificação de "estados finais" para a verificação de "compromissos estruturais". Permite que administradores de segurança garantam propriedades antes que todas as atribuições de funções ou regras sejam finalizadas.
• Composicionalidade Prática: Graças ao teorema da monotonicidade, uma propriedade verificada em uma política parcial não precisa ser re-verificada quando a política é estendida, reduzindo drasticamente o custo computacional em ambientes de políticas dinâmicas e grandes.
• Complementaridade: O framework não substitui ferramentas existentes como Zelkova ou Margrave, mas complementa-as. Ele atua em estágios anteriores do ciclo de vida da política (desenvolvimento e integração de componentes), enquanto as ferramentas tradicionais atuam na política implantada e completa.
• Aplicabilidade: O método é aplicável a políticas expressas em XACML (traduzidas para lógica) e outros formalismos baseados em regras, oferecendo uma base teórica sólida para a verificação de segurança em sistemas complexos e evolutivos.

Em suma, o artigo fornece uma solução formal e computacionalmente viável para garantir que as políticas de controle de acesso mantenham suas propriedades de segurança essenciais, independentemente de como o sistema evolua ou como decisões pendentes sejam resolvidas no futuro.