Security Properties in the lambda-calculus.
Propriétés de sécurité dans le lambda-calcul.
Abstract
We examine security properties in the lambda-calculus through the labelled lambda-calculus. Labels express dynamically the dependence between current terms and past reductions. The property of context irreversibility holds in the labelled lambda-calculus: once a context is involved in a reduction, it irreversibly disappears in the remaining of the reduction. We examine fundamental properties of variants of the labelled lambda-calculus. For that purpose, we introduce an elegant proof of Finite Developments Theorem. We then prove that the labels of the weak lambda-calculus express a sharing property. Lambda-calculus labels allow to express security policies such as Stack Inspection and Chinese Wall. We define independence. Intuitively, a reduction is independent from the interaction between principals A and B if it may be decomposed into two reductions: ! a reduction ignoring A and a reduction ignoring B. We prove that this independence property is guaranteed by the Chinese Wall policy. Lambda-calculus labels also express the interference property. In this case, we identify the subterms of a term M that influence the result of the reduction of M. In a lambda-calculus with references, in addition to the functional interference that already exists in the pure lambda-calculus, we identify a memory interference due to the use of references. Labels allow to identify the time intervals during which a reference influences the result of a reduction.
Nous examinons les propriétés de sécurité du lambda-calcul au travers du prisme du lambda-calcul étiqueté. Les étiquettes expriment dynamiquement la dépendance des termes présents vis-à-vis des réductions passées. Nous montrons que le lambda-calcul étiqueté vérifie la propriété d'irréversibilité des contextes: une fois qu'un contexte est intervenu dans une réduction, il disparaît irréversiblement dans la suite de cette réduction. Nous examinons les propriétés fondamentales de variantes du lambda-calcul étiqueté. Pour cela, nous introduisons une preuve élégante du théorème des développements finis dans la cadre du lambda-calcul par valeur étiqueté. Puis nous prouvons que les étiquettes du lambda-calcul faible expriment le partage. Les étiquettes du lam! bda-calcul permettent d'exprimer des politiques de sécurité telles que l'inspection de pile et la Muraille de Chine. Nous définissons la notion de réduction indépendante de deux principaux A et B: une telle réduction peut se décomposer en deux réductions: une réduction qui ignore A et une réduction qui ignore B. Nous prouvons que la Muraille de Chine garantit cette propriété d'indépendance. Les étiquettes du lambda-calcul permettent aussi d'exprimer la propriété d'interférence: il s'agit ici d'identifier les sous-termes d'un terme M qui influencent le résultat de la réduction de M. Dans le lambda-calcul muni de références, en plus de l'interférence fonctionnelle déjà présente dans le lambda-calcul pur, on identifie l'interférence de mémoire due à l'utilisation des référe! nces. Les étiquettes permettent d'identifier les int! ervalles de temps pendant lesquels une référence influence le résultat d'une réduction.
Loading...