LaFoSec : Étude de la sécurité intrinsèque des langages fonctionnels

Entrée en langue française / French entry Catégorie: Conférence
Auteurs: Éric Jaeger, Olivier Levillain, Damien Doligez, Christèle Faure, Thérèse Hardin et Manuel Maarek
Date: février 2013
Série: Mind your Languages

Un certain nombre d'idées reçues circulent sur l'apport relatif des différents langages de programmation en matière de sécurité, mais les études techniques détaillées sur le sujet sont relativement peu nombreuses. Après l'étude JavaSec consacrée au langage Java, l'ANSSI a souhaité lancer l'étude LaFoSec sur les langages fonctionnels et notamment le langage OCaml (caml.inria.fr, ocaml.org).

Cette étude, menée par un consortium composé de Saferiver, Normation, OPPIDA et du CEDRIC dans le cadre formel d'un marché du SGDSN, avait pour objectif principal d'étudier l'adéquation des langages fonctionnels pour le développement d'applications de sécurité, de proposer le cas échéant des recommandations, et de mettre en pratique certaines de ces recommandations.

Cette étude a notamment donné lieu à la livraison de 5 rapports, qui ont été validés par les laboratoires de l'ANSSI.

L' « État des lieux des langages fonctionnels » présente succinctement 7 langages fonctionnels (OCaml, F#, Scala, Haskell, LISP, Scheme, Erlang). L' « Analyse des langages OCaml, F# et Scala » étudie les grandes caractéristiques de 3 de ces langages dans une perspective de sécurité. Les rapports « Modèles d'exécution de OCaml » et « Outils associés au langage OCaml » complètent l'analyse du langage OCaml en s'intéressant plus spécifiquement aux outils de développement et de vérification, à la compilation et à l'exécution des programmes écrits dans ce langage. L'ensemble a notamment permis de proposer quelques recommandations à l'attention des développeurs, reprises dans le document « Recommandations relatives à l'utilisation du langage OCaml et à l'installation et la configuration des outils associés ». Ces documents sont disponibles sur le site de l'ANSSI (http://www.ssi.gouv.fr/lafosec).

Dans le cadre de l'étude, SafeRiver a développé un générateur de parsers XML en Ocaml. Après recette par l'administration, les sources ont été rendues disponibles sur GitHub (https://github.com/ANSSI-FR/xsvgen).

Présenté lors de la conférence JFLA à Aussois, France en février 2013

BibTeX Partie 1 Partie 2 Partie 3 Partie 4 Documents publiés sur le site de l'ANSSI xsvgen sur GitHub