Abstract FR:

La securite informatique est traditionnellement abordee d'un point de vue systeme d'exploitation qui conduit a des mecanismes de controle dynamiques de bas niveau. Une alternative possible a cette approche consiste a fonder la conception et la mise en uvre de la securite sur les techniques de langages de programmation. L'approche langage de programmation presente des opportunites significatives en matiere de securite mais elle introduit egalement de nouveaux defis. Les opportunites proviennent essentiellement de la possibilite de fournir aux operations et aux entites impliquees une semantique bien definie, ce qui permet de concevoir des analyses statiques de securite de maniere rigoureuse. Les defis proviennent d'une part des difficultes a gerer le niveau de granularite tres fin de ce type de modele, et d'autre part d'une notion de sujet plus complexe. Notre these est que le meilleur moyen de relever ces defis est de partir d'une specification de haut niveau de la politique de securite globale du systeme tout en fournissant les moyens d'assurer de maniere automatique le respect de cette politique. Nous presentons un modele de programmes adapte a la securite ainsi qu'un formalisme pour decrire une classe de politiques de securite. Le cadre propose s'avere suffisamment expressif pour specifier la plupart des politiques de securite communement utilisees dans le contexte du code mobile ; en particulier, il permet de decrire le modele bac-a-sable de l'architecture originelle de java, tout comme son extension qui s'appuie sur des inspections de la pile. Ce modele permet en outre une verification automatique de la mise en uvre effective d'une politique de securite donnee. Pour ce faire, nous proposons une methode permettant de restreindre la semantique d'un programme a un systeme de transition fini qui depend de la politique a verifier. Nous avons montre l'applicabilite de notre methode aux systemes reposant sur le langage java, ce qui nous a conduit a proposer une definition formelle des regles de visibilite dans ce langage.