Security Properties in the lambda-calculus. - Archive ouverte HAL Access content directly
Theses Year : 2006

Security Properties in the lambda-calculus.

Propriétés de sécurité dans le lambda-calcul.

(1)
1

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.
Fichier principal
Vignette du fichier
Blanc.pdf (2.91 Mo) Télécharger le fichier
Loading...

Dates and versions

pastel-00002090 , version 1 (29-07-2010)

Identifiers

  • HAL Id : pastel-00002090 , version 1

Cite

Tomasz Blanc. Security Properties in the lambda-calculus.. Cryptographie et sécurité [cs.CR]. Ecole Polytechnique X, 2006. Français. ⟨NNT : ⟩. ⟨pastel-00002090⟩
213 View
169 Download

Share

Gmail Facebook Twitter LinkedIn More