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.