Resumo

  • O artigo solo de Dorothy E. Denning, de 1976, organiza classes de segurança como uma ordem parcial e usa o menor limite superior, ou join, para classificar resultados influenciados por várias entradas.
  • A análise trata fluxos explícitos e dependências implícitas de controle, mas prova apenas o que a representação do programa, os rótulos declarados e a ordem escolhida conseguem expressar.
  • Canais encobertos, classificação errada, falhas de implementação e desclassificação sem fundamento continuam exigindo controles próprios. Passar na retícula não certifica o sistema inteiro.

Quando duas entradas influenciam a mesma saída, qual rótulo deve prevalecer? Em “A Lattice Model of Secure Information Flow”, Dorothy E. Denning responde calculando a classe mínima que ambas podem alcançar. Esse menor limite superior é o join.

Na notação do artigo, A → B significa que informação da classe A tem permissão para fluir para B. A relação é reflexiva, transitiva e antissimétrica: uma ordem parcial. Assim, compartimentos diferentes podem ser incomparáveis e ainda ter uma classe superior comum. Para uma saída c dependente de a e b, exige-se class(a) join class(b) → class(c).

A fórmula prova coerência interna. Não prova que c seja inofensiva, que as classes estejam corretas ou que o mundo execute exatamente o programa analisado. A distinção entre permissão e segurança empírica é o centro da leitura.

Dependência vai além da cópia

Um fluxo existe quando uma informação afeta outra. b := a é explícito. Já if a = 0 then b := c permite inferir algo sobre a observando se b mudou; há fluxo implícito de a para b, além da atribuição de c.

Essa formulação alcança um problema moderno: decisões, falhas, contadores e tempos carregam sinais mesmo quando nenhum campo foi copiado. Um inventário de permissões de leitura não captura essas influências. A análise precisa propagar a classe das condições para os resultados que elas controlam.

Isso torna possível uma certificação antes da execução. O trabalho posterior “Certification of Programs for Secure Information Flow” detalha a técnica. A autoria precisa ficar correta: o texto de 1976 é somente de Dorothy E. Denning; o artigo de certificação é de Dorothy E. Denning e Peter J. Denning, publicado em 1977 após o Purdue Technical Report 76-181.

Para variáveis e construções modeladas, a garantia é concreta. Um revisor pode verificar se cada dependência derivada alcança apenas destinos permitidos e repetir o teste após alterações do código. Isso é mais forte do que uma intenção informal e mais estreito do que um selo geral de segurança.

O que ficou fora do modelo

O artigo de 1976 limita-se a canais legítimos e de armazenamento. Ele não resolve canais encobertos, como um processo que sinaliza informação alterando a carga do sistema. Também não verifica fluxos que a semântica do programa não especifica. Falta de checagem de limites, referências pendentes, defeitos do compilador, divergência entre fonte e binário ou falha de hardware podem invalidar a ligação com a execução.

Os próprios rótulos são decisões humanas. Se um segredo for marcado como público, a análise pode autorizar com perfeição o fluxo errado. No sentido inverso, permitir apenas fluxos para cima favorece a superclassificação. O estudo conjunto “Data Security” discute desclassificação autorizada, programas que perdem informação e canais de tempo ou consumo. São mecanismos importantes, mas exigem autoridade, justificativa e evidência fora da ordem da retícula.

Uma saída formalmente permitida ainda pode chegar a um endpoint frágil, a um público amplo demais ou a um serviço que remove o rótulo. Em 1999, Denning retomou a fronteira em “The Limits of Formal Security Models”: métodos formais operam dentro de modelos simplificados; ataques reais frequentemente saem da caixa. A conclusão correta é descrever o alcance, não abandonar a prova.

A cadeia que dá sentido ao resultado

O certificado precisa apontar para a versão da política e dos joins, a proveniência dos rótulos, a cobertura semântica do analisador e a identidade exata de fonte, compilador, dependências, binário e implantação. Desclassificações precisam de autoridade e registro. Runtime e endpoints devem preservar rótulos. Canais laterais precisam de testes e monitoramento próprios.

Bell–LaPadula faz parte da linhagem vizinha de segurança multinível e aparece nas referências de Denning. Não é substituto para o argumento dela. Controle de acesso pergunta se um sujeito pode operar; a retícula de fluxo calcula o que uma saída herda de todas as informações que a influenciam.

O legado está nessa disciplina: provar uma coisa importante, nomeá-la corretamente e não usar seu rigor para esconder o que permanece incerto.

Fontes