Golo est un langage et une chaine d’outils open source dédié à la réalisation d’applications dynamiques. Le code produit est un bytecode Java, tournant sur une JVM et exploitant la nouvelle primitive invokeDynamic. Au delà des problématiques classiques des langages orientés objets, ce langage ajoute la possibilité de modéliser des objets dynamiquement en les augmentant.
Dans le cadre de ce stage, nous proposons d’étudier les possibilités d’augmentation de la confiance que l’on peut avoir en un programme Golo. Cela peut être adressé de plusieurs manières dont au moins les deux extrêmes que sont : génération d’un code instrumenté et analyse statique de programme. Dans tous les cas, il sera nécessaire d’ajouter une spécification des propriétés visées dans le programme. En s’inspirant par exemple du langage JML, il sera nécessaire de définir un langage de spécification adapté aux caractéristiques dynamiques de Golo. Golo étant typé implicitement, il pourra-t-être nécessaire d’ajouter la possibilité de spécifier des pré-conditions de types dans les annotations. Ainsi, il serait possible d’imaginer que certaines annotations seraient insérées dans code du programme compilé, tandis qu’une analyse statique du programme pourrait être enrichie par la connaissance de ces nouvelles hypothèses.
Dans la littérature, il sera par exemple possible de s’inspirer de Krakatoa (http://krakatoa.lri.fr/) qui est un outil dédié à la preuve de propriétés sur du code Java, ou sur des approches d’analyse focalisées sur un type particulier de vulnérabilité, comme la fuite d’informations [5]. De même des approchent d’instrumentation automatique existent [3,4] et peuvent être exploitées.
Idéalement, ce stage commencera avec une étude de Golo et de ses particularités, ainsi qu’une analyse de différentes approches existantes pour augmenter le niveau de confiance que l’on peut avoir en du code. Il y aura ensuite une proposition pour se focaliser sur une amélioration possible, avec sa description théorique. Dans un monde parfait, une preuve de concept développée dans le compilateur Golo sera également produite en fin de stage. Une première version de l'outil Hardened Golo existe, mais n'est pas encore stable.
Une première entrée en matière serait d'affiner la structure du projet et la mise en place de tests de non-régressions. Ensuite, la mise en place d'une analyse statique de type des objets devrait pouvoir se faire de manière naïve avant de définir des pistes d'avancées plus spécifiques.
Une autre façon d'aborder ce projet, et de valider automatiquement une spécification Golo, serait l’exécution symbolique de programmes. Cette technique de test permet de générer automatiquement des entrées qui peuvent déclencher des erreurs dans le logiciel et des tests pour couvrir la plupart des chemins d'exécution du programme.
Dans ce projet, de nombreux aspects peuvent être développés, en fonction des préférences du candidat :