Abstract FR:

Le but de cette these est la verification des proprietes de securite de programmes paralleles. Dans la premiere partie de cette these, nous presentons un mecanisme de controle d'acces et nous l'integrons dans un langage objets-orientes parallele. La deuxieme partie de la these presente un systeme de preuve de securite pour un langage parallele. Ce systeme est utilise pour verifier qu'il n'existe pas de fuite d'informations illegale entre les variables d'un programme. Nous adaptons ce mecanisme en une version pour un compilateur ainsi qu'en un mecanisme qui s'integre dans la machine d'execution du langage. Ce derier mecanisme verifie les proprietes de fuite d'informations pendant l'execution du programme. Enfin dans la troisieme partie de la these, nous presentons un mecanisme qui s'integre dans le systeme d'exploitation qui vise a empecher des acces illegaux aux donnees de programmes.