Le paradigme du code mobile implique la distribution des applications par les producteurs de code à environnements hétérogènes dans lesquels elles sont exécutées. Une pratique étendue de ce paradigme est constituée par le développement d'applications telles que les applets ou les scripts Web, transferés à travers un réseau non sécurisé comme Internet à des systèmes distants, par exemple un ordinateur, un téléphone mobile ou un PDA (Assistant personnel). Naturellement, cet environnement peux ouvrir la porte au déploiement de programmes malveillants dans des plateformes distantes. Dans certains cas, la mauvaise conduite du code mobile ne constitue pas un risque grave, par exemple lorsque l'intégrité des données affectées par l'exécution n'est pas critique ou lorsque l'architecture d'exécution impose de fortes contraintes sur les capacités d'exécution du code non sécurisé. Il y a toujours, toutefois, des situations dans lesquelles il est indispensable de vérifier la correction fonctionnelle du code avant son exécution, par exemple lorsque la confidentialité de données critiques comme l'information des cartes de crédit pourrait être en danger, ou lorsque l'environnement d'exécution ne possède pas un mécanisme spécial pour surveiller la consommation excessive des ressources. George Necula a proposé une technique pour apporter de la confiance aux consommateurs sur la correction du code sans faire confiance aux producteurs. Cette technique, Proof Carrying Code (PCC), consiste à déploier le code avec une preuve formelle de sa correction. La correction est une propriété inhérente du code reçuu qui ne peut pas être directement déduite du producteur du code. Naturellement, cela donne un avantage à PCC quant-aux méthodes basées sur la confiance à l'autorité d'un tiers. En effet, une signature d'une autorité ne suffit pas à fournir une confiance absolue sur l'exécution du code reçu. Depuis les origines du PCC, le type de mécanisme utilisé pour générer des certificats repose sur des analyses statiques qui font partie du compilateur. Par conséquent, en restant automatique, il est intrinsèquement limité à des propriétés très simples. L'augmentation de l'ensemble des propriétés à considerer est difficile et, dans la plupart des cas, cela exige l'interaction humaine. Une possibilité consiste à vérifier directement le code exécutable. Toutefois, l'absence de structure rend la vérification du code de bas niveau moins naturelle, et donc plus laborieuse. Ceci, combiné avec le fait que la plupart des outils de vérification ciblent le code de haut niveau, rend plus appropriée l'idée de transferer la production de certificats au niveau du code source. Le principal inconvénient de produire des certificats pour assurer l'exactitude du code source est que les preuves ne comportent pas la correction du code compilé. Plusieurs techniques peuvent etre proposées pour transférer la preuve de correction d'un programme à sa version exécutable. Cela implique, par exemple, de déployer le programme source et ses certificats originaux (en plus du code exécutable) et de certifier la correction du processus de compilation. Toutefois, cette approche n'est pas satisfaisante, car en plus d'exiger la disponibilité du code source, la longueur du certificat garantissant la correction du compilation peut être prohibitive. Une alternative plus viable consiste à proposer un mécanisme permettant de générer des certificats de code compilé à partir des certificats du programme source. Les compilateurs sont des procédures complexes composées de plusieurs étapes, parmi lesquelles le programme original est progressivement transformé en représentations intermédiaires. Barthe et al. et Pavlova ont montré que les certificats originaux sont conservés, à quelques différences près non significatives, par la première phase de compilation: la compilation non optimale du code source vers une représentation non structurée de niveau intermédiaire. Toutefois, les optimisations des compilateurs sur les représentations intermédiaires représentent un défi, car a priori les certificats ne peuvent pas être réutilisés. Dans cette thèse, nous analysons comment les optimisations affectent la validité des certificats et nous proposons un mécanisme, Certificate Translation, qui rend possible la génération des certificats pour le code mobile exécutable à partir des certificats au niveau du code source. Cela implique transformer les certificats pour surmonter les effets des optimisations de programme.

Dans le domaine de la Défense, les contrats export s'accompagnent souvent de transferts de technologie. Un compromis est donc nécessaire entre la protection de la propriété industrielle, celle du secret national et les demandes client. Nous étudierons dans ce contexte et au sein de DCNS les transformations de sécurisation de programme, principalement l'obfuscation et le watermarking. Nous présenterons ces transformations et les principaux résultats théoriques qui les concernent, ainsi que leur adéquation au besoin de sécurité. Nous étudierons la formalisation et la mise en oeuvre des principales techniques connues de transformations. Celles-ci ont pour objectif de rendre diffcile la rétro-ingénierie tout en préservant les fonctionnalités et les performances des systèmes. Nous aborderons les grandes familles existantes et leur implémentation à travers le bytecode Java. Ensuite, nous étudierons l'intégration de ces techniques dans le cycle de développement d'un logiciel complexe. Un premier focus sera effectué sur la mise en oeuvre de certaines techniques de transformation où leurs limites seront exhibées et des pistes d'amélioration proposées. Nous présenterons l'outillage réalisé pour cette analyse et les perspectives d'utilisation envisagées. Enfin, nous présenterons les mécanismes déployés en amont de la transformation permettant d'intégrer au plus tôt la gestion des contraintes et en aval pour vérifier que les techniques utilisées sont conformes à celles demandées afin de renforcer la confiance dans les transformations effectuées.

Par "approche langage" on entend désigner une approche qui s'exprime, soit dans un langage de programmation, soit par un langage de programmation.<br />Les approches qui s'expriment dans le langage ne font appel à aucun formalisme éloigné (e.g. sémantique). Le langage de programmation est l'unique cadre de travail pour exprimer le problème, le résoudre et appliquer la solution. Nous montrons :<br /><br />- comment la compilation des langages fonctionnels peut s'exprimer dans le langage lui-même par transformation de programme. Ce cadre unifié permet de décrire, prouver, comparer et classifier la plupart des mises en œuvre de langages fonctionnels,<br /><br />- deux optimisations de l'implémentation des langages fonctionnels (une analyse de globalisation et un GC étendu) qui reposent sur la syntaxe et le type des expressions.<br /><br /><br /> Pour les approches qui s'expriment par un langage de programmation, il s'agit de prévenir le problème ou d'assurer une propriété via l'utilisation d'un langage (ou d'une discipline de programmation). Nous illustrons ce style d'approche par trois exemples :<br /><br /><br />- les types graphes qui permettent de définir et vérifier le partage des structures de données à pointeurs,<br /><br />- un langage dédié au parallélisme qui garantit une analyse de coût précise et un choix automatique de la meilleure distribution,<br /><br />- un style de programmation par aspects qui permet d'imposer automatiquement des propriétés aux programmes.