, inspection de pile peutêtrepeutêtre vue de façon synthétique comme un mécanisme de sécurité qui contrôle l'exécution d'un programme en prenant des décisionsdécisionsà partir d'informations locales et globales. Les permissions statiques, déterminées en fonction du principal de la fonction courante constituent l'information locale. L'information globale est représentée par les permissions dynamiques qui sont calculéescalculéesà partir de la cha??necha??ne d'appel aboutissantàaboutissantà la fonction courante. Dans le ? t -calcul, on adapte ce mécanisme en attribuant auxétiquettesauxétiquettes le rôle d'information locale et aux chemins le rôle d'information globale. Dans ce calcul, les contractions des radicaux sont conditionnées par l'´ etiquette du radical et le chemin menant au radical. Ce calcul estétudiéàestétudiéestétudié`estétudiéà travers le prisme de la propriété de confluence locale. Une condition suffisante sur les conditions pour obtenir un langage localement confluent esténoncéeesténoncée. A partir de ce langage, on obtient une variante, le ? ts -calcul
, On souhaite savoir si l'observation de la valeur V (intuitivement publique) permet d'obtenir une information sur certains sous-termes (intuitivement secrets) de M . Si on se place dans le cadre du ?-calcul, lesétiquetteslesétiquettes du ?-calcul fournissent une analyse dynamique de dépendance des termes vis-` a-vis des sous-termes du terme initial. Ainsi, l'´ etiquette de tête de V permet d'obtenir le préfixe X des sous-termes de M dont V dépend. Ces sous-termes interfèrent dans V . A contrario, les soustermes qui sont effacés dans X n'interfèrent pas dans V . Par conséquent, V ne donne aucune information sur ces sous-termes. Dans ce cas, l'ensemble des sous-termes qui interfèrent co¨?ncideco¨?ncide avec le préfixe minimum de la propriété de stabilité. Ainsi Dans le cas du ?-calcul par valeur, on obtient de même, le préfixe des sous-termes qui interfèrentinterfèrentà partir de l'´ etiquette de tête du terme obtenu avec la réductionréductionétiquetée du ?-calcul. Par conséquent, dans ce cas, l'ensemble des sous-termes qui interfèrent est simplement inclus dans le préfixe de stabilité du ?-calcul par valeur. Cette inclusion est logique puisque le préfixe de stabilité se réduit vers une valeur, alors que l'obtention d'une valeur est une hypothèse dans le cas de la non-interférence, NousétudionsNousétudions la propriété de non-interférence dans le chapitre 5. Leprobì eme est abordé de la façon suivante : on considère une réduction
, desécrituresdesécritures et des lectures en mémoire ont lieu. Certaines adresses de la mémoire peuvent interférer dans V . Plus précisément, une adresse peut contribueràcontribuerà V pendant certains intervalles de temps : entre uné ecriture et une lecture Si un effet de bord vient interférer entre cetté ecriture et cette lecture, la valeur lue est modifiée, ce qui entra??neentra??ne la modification de la valeur finale. A l'interférence " fonctionnelle " vient s'ajouter une interférence sur la mémoire
, A Core Calculus of Dependency, ACM Symposium on Principles of Programming Languages (POPL), pp.147-160, 1999.
, Access Control based on Execution History, Network and Distributed System Symposium (NDSS'03), pp.107-121, 2003.
, Analysis and Caching of Dependencies, ACM International Conference on Functional Programming (ICFP), pp.83-91, 1996.
, On Declassification and the Non-Disclosure Policy, Proceedings of the Computer Security Foundations Workshop (CSFW'05), 2005.
, (Optimal) duplication is not elementary recursive. Information and Computation, pp.21-56, 2004.
, The Optimal Implementation of Functional Programming Languages, 1999.
, The Lambda Calculus, Its Syntax and Semantics, 1981.
, Secure calling contexts for stack inspection, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '02, pp.76-87, 2002.
DOI : 10.1145/571157.571166
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.9068
, NET Volume I: The Common Language Runtime, 2002.
, The Chinese Wall Security Policy, Proceedings of the 1989 IEEE Symposium on Security and Privacy, pp.206-214, 1989.
, Combinatory Weak Weduction in Lambda-Calculus, Theoretical Computer Science, vol.198, pp.239-249, 1998.
, Security policies for downgrading, Proceedings of the 11th ACM conference on Computer and communications security , CCS '04, pp.189-209, 2004.
DOI : 10.1145/1030083.1030110
, Cryptography and Data Security, 1982.
, Certification of Programs for Secure Information Flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
, Stack Inspection: Theory and Variants, 2001.
DOI : 10.1145/565816.503301
, Security Policies and Security Models, 1982 IEEE Symposium on Security and Privacy, pp.11-20, 1982.
DOI : 10.1109/SP.1982.10014
, Inside Java TM 2 Platform Security, 1999.
, The geometry of optimal lambda reduction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, 1992.
DOI : 10.1145/143165.143172
, An abstract standardisation theorem, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.72-81, 1992.
DOI : 10.1109/LICS.1992.185521
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9163
, On Lisp: Advanced Techniques for common Lisp, 1993.
, The Confused Deputy, ACM SIGOPS Operating Systems Review, vol.22, issue.4, pp.36-38, 1988.
DOI : 10.1145/54289.871709
, The SLam calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.365-377, 1998.
DOI : 10.1145/268946.268976
, Verification of control flow based security properties, Proceedings of the 1999 IEEE Symposium on Security and Privacy (Cat. No.99CB36344), pp.89-103, 1999.
DOI : 10.1109/SECPRI.1999.766902
, Combinatory Reduction Systems, 1980.
, An algorithm for optimal lambda calculus reduction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.16-30, 1990.
DOI : 10.1145/96709.96711
, NET Framework Security, 2002.
, On the Global Dynamics of Optimal Graph Reduction, ACM International Conference on Functional Programming, 1997.
, Didier Rémy et Jérôme Vouillon. The Objective Caml manual
, Réductions correctes et optimales dans le lambda-calcul, Thèse de doctorat, 1978.
, Explicit Substitutions and Programming Languages, Proc. 19th Conference on the Foundations of Software Technology and Theoretical Computer Science Electronic Notes in Theoretical Computer Science, pp.181-200, 1999.
DOI : 10.1007/3-540-46691-6_14
, The Java Virtual Machine Specification, 1996.
, Jif: Java + information flow, 2001.
, On Theories with a Combinatorial Definition of "Equivalence", The Annals of Mathematics, vol.43, issue.2, pp.223-243, 1942.
DOI : 10.2307/1968867
, Haskell 98 Language and Libraries : The Revised Report, 2003.
, A Systematic Approach to Access Control, Programming Languages and Systems (ESOP 2001), volume 2028 de LNCS, pp.30-45, 2001.
, Information Flow Inference for Free, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pp.46-57, 2000.
, Information flow inference for ML, ACM Transactions on Programming Languages and Systems, vol.25, issue.1, pp.117-158, 2003.
DOI : 10.1145/596980.596983
, Inférence de flots d'information pour ML: formalisation et implantation
, A type-based approach to program security, Lecture Notes in Computer Science, vol.1214, pp.607-621, 1997.
DOI : 10.1007/BFb0030629
, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.167-187, 1996.
DOI : 10.3233/JCS-1996-42-304
, Semantics and pragmatics of the lambda-calculus, 1971.
, SAFKASI: a security mechanism for language-based systems, ACM Transactions on Software Engineering and Methodology, vol.9, issue.4, pp.341-378, 2000.
DOI : 10.1145/363516.363520