Compilation de déclarations dans des cadriciels : une méthodologie indépendante du langage

Abstract

Dans le domaine des plates-formes ouvertes, l’utilisation des cadriciels (frameworks) enrichis par des déclarations pour exprimer les permissions de l’application est de plus en plus répandue. Ceci est une réaction logique au fait qu’il y a une explosion d’adoption des appareils embarqués et mobiles. Leur omniprésence dans notre vie quotidienne engendre des craintes liées à la sécurité et à la vie privée, car l’usager partage de plus en plus ses données et ressources privées avec des tiers qui développent des applications auxquelles on n’a pas de raison de faire confiance. Malheureusement, la manière dont ces langages de spécification ainsi que ces cadres d’applications sont développés est généralement assez ad hoc et repose sur un domaine d’application et un langage de programmation fixes. De plus, ces cadriciels ne sont pas assez restrictifs pour régler le problème de la fuite de données privées et ne donnent souvent pas non plus assez d’informations à l’usager sur le comportement attendu de l’application. Cette thèse présente une méthodologie généraliste pour développer des cadriciels dirigés par des déclarations, qui cible un spectre large de langages de programmation. Nous montrons comment des langages de déclaration expressifs permettent de spécifier avec modularité les droits d’accès aux ressources ainsi que le flux de contrôle d’une telle application. Ces langages peuvent ensuite être compilés en un cadriciel garantissant à l’usager final le respect de ces permissions. Par rapport aux cadriciels existants, notre méthodologie permet de guider la personne qui développe des applications à partir des spécifications ainsi que d’informer l’usager final sur l’usage des ressources sensibles. Contrairement aux travaux existants, la méthodologie présentée dans cette thèse ne repose par sur un langage de programmation particulier. Nous montrons comment mettre en oeuvre de tels cadriciels dans un spectre de langages : des langages avec typage statique ou dynamique, et suivant le paradigme objet ou fonctionnel. L’efficacité de l’approche est montrée à travers des prototypes dans le domaine des applications mobiles dans deux langages très différents, à savoir Java et Racket, ce qui montre la généralité de notre approche.