Résumé

  • Dans son article de 1976, Dorothy E. Denning ordonne les classes de sécurité et emploie leur borne supérieure minimale — le join — pour déterminer la classe minimale d’un résultat influencé par plusieurs entrées.
  • L’analyse couvre les transferts explicites et les dépendances implicites créées par le contrôle, mais seulement dans les limites des étiquettes déclarées et de la sémantique représentée.
  • Les canaux cachés, une mauvaise classification, un exécutable différent ou un déclassement injustifié restent des problèmes distincts. La conformité au treillis n’est pas un verdict global.

Lorsqu’un résultat dépend de deux entrées de classes différentes, où peut-il aller ? Dans « A Lattice Model of Secure Information Flow », publié en 1976, Dorothy E. Denning répond : vers une classe autorisée à recevoir leur borne supérieure minimale. Cette borne, le join, est la plus petite classe commune que les deux entrées peuvent atteindre selon la politique.

La relation A → B signifie que l’information de classe A est autorisée à entrer dans B. Elle est réflexive, transitive et antisymétrique : c’est un ordre partiel. Deux compartiments peuvent donc être incomparables tout en partageant une classe supérieure. Si c dépend de a et b, la condition devient class(a) join class(b) → class(c).

Cette formule n’affirme pas que c est sûr dans le monde réel. Elle établit qu’avec ces classifications et cet ordre, le flux modélisé vers c est permis. Le modèle transforme ainsi une intention de confidentialité en question mécanique, sans transformer les prémisses en vérités.

L’influence compte autant que la copie

Denning ne réduit pas le flux à un déplacement de données. b := a constitue un flux explicite. Mais dans if a = 0 then b := c, l’état final de b peut révéler si la condition portant sur a était vraie. Il existe donc un flux implicite de a vers b, même si aucune valeur de a n’a été copiée.

Cette idée est toujours décisive. Les logiciels communiquent par leurs branches, leurs erreurs, leurs compteurs et parfois leur consommation de ressources. Suivre uniquement les octets copiés revient à ignorer une partie des dépendances. Le treillis oblige au contraire à calculer la classe de ce qui influence le résultat.

L’analyse peut être réalisée avant l’exécution : classes des variables et des expressions, influence des conditions, puis vérification de chaque destination. « Certification of Programs for Secure Information Flow » approfondit ce mécanisme.

La chronologie et les signatures doivent rester exactes. L’article de 1976 sur le treillis est de Dorothy E. Denning seule. L’article de certification est cosigné par Dorothy E. Denning et Peter J. Denning ; il paraît en 1977 après le rapport technique Purdue 76-181. Confondre les deux attribuerait mal le travail et masquerait le passage du modèle à sa méthode de certification.

La limite est dans les hypothèses

Le texte de 1976 exclut explicitement les canaux cachés, par exemple l’influence d’un processus sur la charge du système. Il vise les canaux légitimes et de stockage. Il reconnaît aussi qu’une certification ne peut pas vérifier ce que le programme ne décrit pas : contrôle de limites absent, référence pendante, faute du compilateur, panne matérielle ou binaire qui ne correspond plus à la source certifiée.

Les étiquettes peuvent être erronées. Une donnée secrète déclarée publique traversera peut-être correctement un treillis mal renseigné. À l’inverse, l’interdiction systématique des flux descendants produit facilement une surclassification. L’étude conjointe « Data Security » examine ce problème, les déclassements autorisés et les programmes qui perdent volontairement de l’information. Aucun de ces mécanismes ne dispense d’indiquer qui autorise, quelle information a disparu et sur quelles preuves repose la décision.

Un résultat peut enfin respecter la politique formelle et arriver sur un terminal mal protégé, auprès d’un public trop large ou dans un service qui retire son étiquette. Les timings et consommations de ressources peuvent aussi communiquer en dehors des affectations ordinaires. Le modèle n’a pas promis de résoudre seul ces risques.

Dans son discours de 1999, « The Limits of Formal Security Models », Denning revient sur cette discipline : les méthodes formelles démontrent des propriétés à l’intérieur d’un modèle simplifié et de ses hypothèses, tandis que les attaques réelles sortent souvent de ce cadre. La leçon ne consiste pas à renoncer à la preuve, mais à ne pas élargir son libellé.

Une pièce dans une chaîne de preuves

Une organisation devrait donc relier le résultat formel à une politique versionnée, à la provenance des classifications, à la couverture sémantique de l’analyseur, puis à la chaîne exacte source–compilateur–binaire–déploiement. Le déclassement doit avoir sa propre autorité et son journal. Les contrôles d’exécution et de terminal doivent conserver les étiquettes. Les canaux latéraux appellent des tests et une surveillance séparés.

Bell–LaPadula appartient à l’histoire voisine de la sécurité multiniveau et figure dans les références de Denning. Il ne remplace pas son apport propre : relier dépendance informationnelle, combinaison de classes et certification de programme. Le contrôle d’accès demande si un sujet peut agir ; le treillis de Denning demande quelle classe résulte de toutes les informations qui influencent une sortie.

Voilà pourquoi ce travail reste utile. Il ne promet pas de tout prouver. Il rend une affirmation importante vérifiable, et empêche le reste de disparaître derrière elle.

Sources