OSIS 2017 - Langages et Outils pour la fiabilité logicielle

Dans le cadre des journées Open Source Innovation Spring, nous avons participé à celle dédiée aux langages et la fiabilité logicielle.

Au programme, expositions de travaux autour de la sûreté des langages, des enjeux de la sécurité et des prouesses en terme de performances de certaines technologies.

I - Quand Ada et SPARK pillent d'autres langages pour augmenter la sécurité

Intervenant : Raphaël AMIARD

Biographie : Raphaël Amiard est un ingénieur logiciel chez AdaCore travaillant sur le développement d'outils et de compilateurs.

Présentation :

Ada est langage existant depuis de nombreuses années, initialement commandé par le ministère de la défense américain, ce langage standardisé repose sur la déclaration de types explicites en faisant un des premiers langages orienté sûreté.

Raphaël Amiard nous expose ses travaux visant à renforcer le langage Ada. Le langage SPARK qui est un sous ensemble de Ada permet la preuve formelle et donc la programmation par contrats renforçant le niveau de sûreté de son cousin Ada. Toujours dans cet objectif de sûreté, des fonctionnalités ont été empruntées à différents langages telles que le “pattern matching” d'Ocaml et l'élimination des pointeurs nuls par une gestion des propriétés améliorée dans le but de proposer une meilleure version du langage Ada.

II - Projet Rudder : d'une programmation objet classique aux Free Monads en 8 ans de Scala

Intervenants : Vincent Membré & François Armand

Biographies :

• François Armand, papa³, développeur passionné, Scala depuis >10 ans, cofondateur & CTO de Normation, lead-dev Rudder.
• Vincent Membré, Développeur Lambda chez Normation, depuis 5 ans ( Scala \o/, mais pas uniquement) , Release manager sur Rudder, presque double papa.

Présentation :

Évolutions à travers le projet de gestion d'infrastructure Rudder du langage Scala basé sur initialement sur Java. Présentation du concept de programmation dirigée par les types avec l'introduction de typage non mutables pour davantage de sûreté. Initiation aux monads et Free monads pour une meilleure maintenance du code Scala.

III - Quelques principes de sécurité pour le développement d'applications robustes

Intervenant : Eric Jaeger

Biographie : Fonctionnaire SSI du ministère de la défense depuis fin 2014, après un passage d'une dizaine d'années par l'ANSSI où il a notamment travaillé sur la prise en compte de la sécurité dans le développement logiciel.

Présentation :

Démonstration des concepts de sécurité à travers les exploits et les risques liés aux appareils informatisés.

Présentation de certaines failles autour de langages vastement utilisés tel que PHP avec l'appel de fonctions par l'intermédiaire de type string, Java par la modification des visibilités grâce à l'introspection, Ocaml la possibilité de réaliser des changements de type ... remettant en cause les développeurs de ces langages tout autant que leur utilisateurs.

IV - Vers de la détection de malware statique

Intervenant : Tayssir Touilli

Biographie : Directrice de recherche (DR - CNRS) au LIPN

Présentation :

Les actuels antivirus se basant pour la plupart sur signatures que tous les éditeurs d'antivirus partagent afin d'identifier les malwares. Dans un contexte de malware grandissant, le LIPN propose une nouvelle approche visant la détection de comportements malveillant. Cette technique repose sur l'utilisation d'automates à pile et de règles sémantiques afin détecter un comportement malveillant de manière générique plutôt que de détecter la manière de l'implémenter.

L'outil se base sur l'analyse de code binaire de manière statique et se révèle plus efficace que la majeur partie des antivirus actuels. Avec le peu de règles sémantiques actuellement définies il est possible de détecter plus de 800 virus dont beaucoup passe incognito à travers nos antivirus usuels.

L'enjeu est maintenant de pouvoir réaliser un outils permettant d'extraire les règles sémantiques des malwares afin de pouvoir contrer les futures évolutions de ceux-ci.

V - Mise au point sur cartes graphiques

Intervenant : Mathias Bourgoin

Biographie : Maître de conférences (LIFO, Univ Orléans)

Présentation :

La programmation GPGPU est maintenant très répandue et peu onéreuse. Une correcte utilisation de celle-ci permet un impressionnant gain de performance.

Cependant, elle exige généralement que les développeurs combinent plusieurs modèles de programmation, à travers des langages et des outils très complexes. Les programmes GPGPU sont ainsi difficiles à concevoir et à déboguer.

Mathias Bourgoin nous présente donc une solution de profilage portable et compatible avec un grand nombre d'architecture GPU basée sur SPOC, une bibliothèque portable en Ocaml associée à un DSL permettant de générer du code GPGPU à l'exécution.

Basé sur SPOC et Saren l'outil de profilage se veut simple d'utilisation, compatible avec des environnement GPU hétérogènes et permettant à la demande d'obtenir des informations utiles reliables au code écrit à l'origine et non au code généré (qui la plupart du temps bien différent).

VI - Développement des applications Web et mobiles du réseau social Be Sport grâce à la programmation multi-tier typée et au framework Ocsigen

Intervenant : Vincent Balat

Biographie : CTO de Be Sport

Présentation :

Be Sport est une start-up qui développe une plateforme sociale réunissant tous les acteurs du sport : les fans, athlètes, media, marques, etc. Pour permettre de développer rapidement, et avec des moyens limités, ses applications Web et mobiles, Be Sport a fait le choix d'utiliser le framework Ocsigen, qui propose une façon radicalement nouvelle de programmer, basée sur une version multi-tiers du langage OCaml, et une utilisation intensive du typage statique.

Les applications Web et mobiles (iOS, Android) sont écrites avec un code source unique, qui permet de décrire les côtés serveur et client, et la version Web et mobile, le typage garantissant la fiabilité.

Conclusion

Cette journée a été riche en contenu innovants. La thématique sécurité de cette conférence met le doigt sur des problèmes touchant certes majoritairement les langages impératifs mais également certains langages fonctionnels.

L'utilisation de typage statique au sein de notre programmation permet de garantir une bon niveau de sûreté et de détecter à la phase de compilation les éventuelles erreurs qui par opposition au typage dynamique lui garantit une meilleure maintenabilité.

Les langages fonctionnels sont également mis en avant de part leur expressivité et le fait qu'ils reposent des concepts mathématiques déjà formalisés. Ils permettent un développement fiable et surtout plus concis au regard des langages impératifs par exemple.