Blanc, Tomasz (2006) Security Properties in the lambda-calculus. PhD thesis INRIA Rocquencourt - MOSCOVA, INRIA Rocquencourt - MOSCOVA, EP/X p.179.

Alternative Locations: http://www.imprimerie.polytechnique.fr/Theses/Files/Blanc.pdf

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.

Statistiques de consultation

Repository Staff Only: edit this item