Présentation du projet

Ce projet s’inscrit dans le cadre d’une dynamique émergente mais forte de vérification de codes logiciels critiques pour des besoins de sécurité, de qualité et de valeur probante des résultats des logiciels. Il vise de pouvoir garantir un fonctionnement sans erreur de logiciels développés en langage Python.

L’objectif est de développer des outils d’analyse de code, applicables sur un sous-ensemble de Python, afin de pouvoir garantir des propriétés sur du code applicatif analysé. Cette sélection d’un sous-ensemble de Python est une des premières difficultés du projet.

Le consortium a décidé de développer un front-end Python sur un outil d’analyse formelle préexistant, FramaC, et le projet prévoit donc de développer un front-end « Frama-Py ». Afin d’accélérer le développement, le projet prévoit d’utiliser PyLint pour lire le code source, et produire un arbre de syntaxe enrichi.

Les partenaires développeront ensuite un ensemble d’outils d’analyse de code source Python, permettant aux développeurs de disposer d’une boîte à outils fournie pour l’analyse de code, avec des outils simples mais aussi des outils d’analyses sémantiques avancées, qui formeront un autre des verrous de ce projet.

Le projet prévoit de valider la pertinence de ces outils sur des cas d’usages dans le domaine de la gestion d’Infrastructure, de la vidéosurveillance et de la sécurité informatique. La synthèse des travaux réalisés sur les cas d’usages permettra la rédaction d’un guide des bonnes pratiques pour le développement de nouveaux codes Python ou pour la réécriture de codes existants, afin que ces codes puissent être vérifiables par les outils développés.

La dissémination se fera principalement en direction des communautés OpenSource, notamment en contribuant à la réécriture et à la vérification formelle de bibliothèques existantes. On envisage aussi la création d’un label « SAFEPYTHON ». On vise ainsi la création d’un pôle d’expertise sur l’analyse de codes Python en Ile de France.

Retombées attendues :

Les outils créés dans le projet sont destinés au marché du SAST (Static Application Security Testing), qui a été analysé par le Gartner. Compte tenu du poids actuel du langage Python, le marché de l’analyse de codes Python est un nouveau marché qui est estimé entre 10 M€ et 20 M€ par an, pour l’Europe à l’horizon 2015. Une bonne part pourrait être captée par le pôle d’expertise que nous avons l’ambition de créer en Ile de France.

C’est le marché que visent les partenaires qui sont déjà des acteurs du SAST (LOGILAB, CEA LIST, INRIA), avec une augmentation attendue de leur part de marché.

En complément, les retombées économiques indirectes du projet sont beaucoup plus importantes, puisque les partenaires qui proposent des expérimentations industrielles attendent du projet une amélioration de leur position concurrentielle sur leur propre marché :

  • Wallix attend une augmentation de CA significative (10% environ) de ses logiciels de sécurité,
  • Evitech anticipe une augmentation sensible de son CA (20%), notamment par l’augmentation des revenus de maintenance logicielle
  • Oppida, centre d’évaluation de sécurité agréé par l’ANSSI, vise une augmentation de la productivité dans ses missions d’évaluation, et une augmentation de CA très significative.

Travaux envisagés :

  • Formalisation de la liste des vulnérabilités Python étudiées, et définition (syntaxique et sémantique) d’un sous-ensemble du langage propice à l’application des techniques d’analyse de code
  • Identification des propriétés à rechercher pour améliorer la sûreté de fonctionnement de codes Python : typage des constructions Python, problèmes de conversion de types, etc.
  • Développement des Front-end FramaPy et Pylint étendu
  • Développements d’outils d’analyse de conformité de codes existants au sous-langage RPython choisi, et de métriques sur les programmes écrits dans ce langage
  • Développements d’outils d’analyse sémantique du flot de données dans un programme RPython.
  • Rapports d’expérimentation des cas d’usage et analyse de l’impact du projet sur la valeur probante des résultats fournis par les logiciels :
  • Méthodologie et guide de bonnes pratiques : liste des bibliothèques publiques vérifiées formelles, création d’un label.