Renaming or Tightness: Enforcing Disjunctive Information Flow Policies

Résumé technique : Renommer ou Serrer : l'application de politiques de flux d'information disjonctives

Énoncé du problème
Les politiques de flux d'information disjonctives restreignent une valeur à dépendre d'au plus un des deux secrets, interdisant la combinaison de libérations autrement permissibles (par exemple, un mur éthique empêchant un rapport de dépendre à la fois des fichiers du Client A et du Client B, ou un schéma de partage de secret ne libérant qu'une seule part). Contrairement aux politiques classiques basées sur les treillis, où la jonction de deux dépendances admissibles est admissible, les politiques disjonctives ne sont pas de forme « treillis ». Hunt et Sands ont précédemment fourni une sémantique pour ces politiques en utilisant le « quantale de l'information », où la conjonction est un tenseur non idempotent ($\otimes$) plutôt qu'une jonction. Cependant, la couche d'application — spécifiquement, ce qu'un système de typage sensible au flux peut certifier de telles politiques — est restée un problème ouvert.

Le défi central est que les systèmes de typage sensibles au flux existants, qui reposent sur un objet universel pour permettre une analyse indépendante de la politique (via un renommage monotone), échouent à préserver la précision sous des politiques disjonctives. Plus précisément, lorsqu'une source est lue deux fois (par exemple, un résumé utilisé à la fois dans un en-tête et dans un tableau), les mécanismes standards perdent la corrélation selon laquelle les deux lectures respectent le même disjonct. Par conséquent, ils sur-approximent le flux d'information, certifiant que la sortie révèle les deux secrets ($\top$) même lorsque la politique est respectée.

Méthodologie
Les auteurs construisent une famille de systèmes de typage sensibles au flux ($F_1$) sur un quantale affine commutatif arbitraire $M$. L'analyse procède en étudiant l'« objet universel » à partir duquel tous les systèmes spécifiques à une politique se spécialisent. À l'ère des treillis, l'ensemble des puissances des variables servait d'objet universel unique. L'article démontre qu'au-dessus d'un quantale, cet objet se scinde en trois candidats distincts, possédant chacun des propriétés différentes concernant la précision et la capacité à supporter le renommage monotone.

1. L'Objet Multiensemble ($U_N$) : Le monoïde commutatif libre sur les variables (les éléments sont des multiensembles). Il supporte un renommage monotone complet et des typages principaux, mais perd la « corrélation de même source ». Il traite deux lectures d'une source comme deux utilisations indépendantes, menant à une sur-approximation ($\sigma(v) \otimes \sigma(v)$).
2. L'Objet Ensemble ($U$) : Le monoïde commutatif idempotent libre (les éléments sont des ensembles de variables, représentés comme des ensembles descendants de l'ensemble des puissances). Il préserve la corrélation de même source (deux lectures d'une source comptent pour une seule) mais brise la propriété homomorphe requise pour le renommage monotone. La spécialisation ici est une section oplaxe, et non un homomorphisme.
3. Le Locale Libre ($L$) : L'objet de l'ère des treillis (ensembles de variables avec l'union comme combinaison). Il est précis pour les lectures uniques, mais confond la disjonction de branchement avec la combinaison de tenseur, effaçant la distinction entre « l'exécution A a utilisé X, l'exécution B a utilisé Y » et « une exécution a utilisé X et Y ».

L'article analyse les compromis entre ces objets, prouvant qu'aucun mécanisme de la forme « attribut indépendant » (où les environnements associent les variables à des éléments uniques du quantale) ne peut simultanément supporter le renommage monotone et atteindre des bornes serrées pour les politiques disjonctives.

Contributions clés et résultats

1. Famille de systèmes de typage ($F_1$) : Une famille de systèmes de typage sonne ancrée dans les lemmes de composition de Hunt et Sands. Elle gère les boucles en utilisant la clôture idempotente du facteur de garde, un ajustement nécessaire pour les quantales qui est invisible dans les treillis.
2. La scission de l'objet universel : L'article établit une trichotomie :
   • Sur $U_N$, l'intégralité du mécanisme de typages principaux et de complétude interne survit inconditionnellement, mais la borne est lâche pour les sources réutilisées.
   • Sur $U$, la borne est strictement plus précise (enregistrant que deux lectures respectent un seul disjonct) mais la spécialisation n'est plus un homomorphisme, brisant la propriété de renommage.
   • Sur $L$, l'objet perd la disjonction de branchement, échouant à distinguer les exécutions alternatives des exécutions combinées.
3. Impossibilité du renommage et de la précision (tightness) : Les auteurs prouvent que pour tout mécanisme de forme « attribut indépendant » qui supporte le renommage monotone, la borne certifiée pour une source réutilisée sous un label « saturé » (où $m \otimes m = \top$) est $\top$. Cela signifie que sous des labels de type mur éthique ou partage de secret, une seconde lecture d'une source ne certifie rien, provoquant le rejet par le mécanisme de programmes qui satisfont pourtant la politique.
4. La Réparation (Spécialisation Différée) : Pour recouvrer la précision, l'article propose de différer la spécialisation au niveau du jugement. Au lieu d'appliquer la carte de labellisation à l'environnement (ce qui impose une structure homomorphe), la carte est appliquée uniquement à l'observation finale (la lecture).
   • Cette approche utilise l'Objet Ensemble ($U$) pour le typage et la carte $\alpha_\sigma$ pour la lecture.
   • La carte de lecture résultante est prouvée être la carte la moins sonore préservant les jonctions.
   • Cette « réparation » sacrifie la capacité de présenter le résultat comme une dérivation au sein du système cible (renommage), mais elle atteint la borne la plus serrée possible pour les mécanismes à attribut indépendant.
5. Décidabilité : L'article montre que la vérification de la conformité est décidable. Bien que $U_N$ soit infini, la borne spécialisée dépend uniquement des multiplicités jusqu'à l'ordre du label (par exemple, 2 pour les murs éthiques), permettant une troncature finie. $U$ est un treillis fini, garantissant la terminaison.

Signification et affirmations
L'article affirme que la transition des systèmes basés sur les treillis vers les systèmes basés sur les quantales force un choix fondamental qui était auparavant caché : on peut avoir le renommage monotone ou la précision, mais pas les deux.

• Pour le paradigme du renommage : L'article démontre que l'approche de l'« objet universel », qui permet d'analyser un programme une seule fois et de réutiliser le résultat pour n'importe quelle politique, rencontre un plafond dur. Pour les politiques disjonctives, ce plafond est si bas (souvent $\top$) qu'il rend le mécanisme inutile pour des scénarios courants comme le partage de secret ou les murs éthiques où une valeur est utilisée plusieurs fois.
• Pour la précision : L'article fournit une solution constructive (spécialisation différée) qui recupère la précision manquante. Il montre qu'en gardant le type universel dans l'Objet Ensemble ($U$) et en appliquant le labellisation seulement à la fin, on peut certifier des programmes que le paradigme du renommage rejette.
• Implication pratique : La distinction entre « une source lue deux fois » (sûre sous des politiques disjonctives) et « deux sources lues une fois » (non sûre) n'est préservée que par l'Objet Ensemble. L'objet multiensemble (favorable au renommage) et l'objet locale (favorable aux treillis) échouent tous deux à distinguer correctement ces cas dans le contexte des politiques disjonctives.

Les auteurs concluent que si l'objet de l'ère des treillis est un quotient qui perd la disjonction de branchement, et que l'objet multiensemble perd la corrélation de même source, l'Objet Ensemble ($U$) est le seul qui conserve les deux. Le coût de cette précision est la perte de la propriété de renommage, un compromis nécessaire pour l'application des politiques disjonctives. L'article ne prétend pas résoudre le problème pour les analyses relationnelles ou les mécanismes sensibles au chemin (suggérés comme directions futures dans des travaux connexes), mais il caractérise pleinement les limites et les possibilités de la famille des attributs indépendants.