Mon second postdoc dans les équipes TAMIS puis DiverSE se déroule dans le cadre du projet européen TeamPlay, encadré par le chargé de recherche Olivier Zendra à Inria-Rennes. Ce projet vise à permettre au développeur d'avoir accès aux propriétés extra-fonctionnelles de son code, en particulier le temps d'exécution, l'énergie consommée et la sécurité, ainsi que de pouvoir raisonner sur les compromis entre ces propriétés et de choisir entre les variantes du code obtenues par optimisation multicritère.

Mon intérêt pour ce projet vient notamment du fait que mes travaux sur les modèles de calcul traitaient aussi de propriétés extra-fonctionnelles comme l'expressivité et la complexité algorithmique et ceux sur les méthodes formelles sur la spatialité de l'information. Ce projet m'a permis d'étudier d'autres propriétés extra-fonctionnelles ainsi que leurs interactions, notamment comment les exprimer et comment vérifier qu'elles satisfont leurs contraintes. J'ai conçu une contremesure logicielle par échelonnement qui préserve le comportement algorithmique du programme tout en garantissant par construction une protection contre certaines attaques. J'ai travaillé sur l'imitation comportementale de tâches à protéger pour les systèmes embarqués en temps réel. Enfin, la méthodologie basée sur l'identité des indiscernables m'a permis de définir des métriques de sécurité quantifiant les fuites d'information sensible par les propriétés extra-fonctionnelles observables par un attaquant.

Le centre Inria-Rennes a la charge dans le projet TeamPlay des aspects sécurité, et nous avons développé une chaîne d'outils permettant :

• d'annoter un code en C pour déterminer les fragments du code à étudier et pour marquer une variable comme secrète,
• par une analyse statique basée sur une politique de teinte de déterminer dans ces fragments les variables contenant des données sensibles,
• d'identifier les branchements conditionnels sensibles, puis d'utiliser des outils d'analyse temporelle pour générer une variante du code où les deux branches sont équilibrées afin de réduire la fuite d'information par canal auxiliaire,
• de recueillir automatiquement les données temporelles ou énergétiques associées aux variantes du code étudié exécutées avec des échantillons d'entrées sensibles ou non,
• avec ces données de calculer différentes métriques de sécurité et de propager les niveaux de sécurité obtenus dans un fichier associant le code final avec ses différentes propriétés extra-fonctionnelles.

Ces valeur de propriétés extra-fonctionnelles peuvent ensuite être utilisées dans le reste du code, permettant au développeur de raisonner sur elles comme sur n'importe quelle autre variable. Les variantes non pertinentes d'un code sont éliminées, mais les variantes sur le front de Pareto sont des candidats pouvant être utilisés par l'aspect coordination du projet afin de satisfaire des contraintes en temps, énergie ou sécurité sur des architectures mono- ou multi-cœurs potentiellement hétérogènes.