Ryad Benadjila, Arnaud Ebalard et Patricia Mouy (ANSSI)
On va utiliser le C car il supporte pas mal de cibles. Il est portable, bonne performance, et a une grosse communauté.
Le parsera été fait de manière propre, simple et lisible en éliminant le nombre de bugs, et en ayant des garanties formelles.
On connait les limites de C.
On essaye de travailler sans faire d'allocations dynamiques,de la discipline. On ne fait pas de C++.
Compilation avec clang et la ligne de commande qui va bien
On a un set de données pour tester le parseur
Récupération d'une base de 200 millions de certificats reels, 252 GB de données, merci Google.
Ne peut-on pas injecter des certificats improbables?
Peu de chance de trouver des certificats "agressifs", mais des certificats "bizarres" qui pourraient faire crasher le parseur?
On n'a pas de RTE, runtime erros? On a fait un parseur garanti sans RTE.
Divisions par 0... Le parseur ne peut pas crasher sur ces vecteurs d'attaques.
On choisit les armes: l'outil parfait
Pas de faux positifs
simple et automatique
open source
on drop le code, on appuie sur le bouton : "il n'y a pas de bugs", ça n'existe pas encore
Comparaison : Frama-C est un framework d'analyse qui couple plusieurs plugins qui travaillent en symbiose pour arriver à un résultat. Basé sur les méthodes formelles.
On peut développer des plugins, c'est modulable.
On se limite à:
RTE plugin qui annote automatiquement le code du C ou des RTE pourraient se produire.
Outils d'analyses statiques: on repasse la main à l'humain qui va devoir traiter chacun des warnings: faux positif ou vrai erreur?
On peut retravailler le source, le nombre de warnings diminue, mais on accepte une certaine quantité de warnings.
Les boucles, on peut valider leur contenu
Frama-C donne un feedback dans le projet
exemple: parties du code trop compliqué sur une fonction qui fait 40 lignes. On découpe la fonction en factorisant le code;
Gestion des derniers warinigs:
Gestion des pointeurs de fonction
35 boucles, 516 goto
249 pointers dereference
Si on devait faire à la main la notation RTE, on y passerait beaucoup trop de temps
Cotés négatifs de l'outil Frama-C:
Il manque les designs patterns pour tel ou tel type de code. Pour certaines annotations certaines apparaissent compliquées.
plugin EVA (ajoute annotations de maniere automatique) et plugin WP .
cotés positifs de l'outil Frama-C:
plate forme ultra collaborative.
L'outil s'améliore en fonction des releases, tous les 6 mois environ.
version 17: chlorine
version 18: Argon, avec l'annotation "calls" nécéssaire pour WP
version 19: potassium: le parseur passe en moins de 2 minutes. Dépendances avec les solveurs mise en avant.
version beta: calcium . point notable: appel au Why3. options eva-auto-loop-unroll
STATUS
parseur qui fait de l'analyse syntaxique de certificats X509, prouvé garanti sans RTE
code:
https://github.com/ANSSII-FR/x509-parser
validé avec Frama-C
Autres outils d'analyse statique: Bug finder, Coverity, CodeSonar
Utilisés pour trouver un bug logique typique goto fail classique.
-code quality
-useless parts
detection des copy-paste erreurs
Comparaison descomportements bizarres:
EVA 58 warnings
CodeProver 53 warnings
IKOS 2.2 94 warnings
Validation fonctionnelle
Petit exemple: on parse une adresse IP. 4 octets IPV4. 1 digit, 1 point, etc. IPV6 c'est un peu plus compliqué, mais ca reste facile à parser.
valider par exemple le domaine d'une adresse email.
Plus on passe d'outils sur le code, mieux on a une garantie anti RTE dans le code
Les autres outils sont aussi très utiles pour trouver des bugs logiques
Cet article reflète exclusivement l'opinion de ses auteurs et n’engage en aucune façon Consultingit. J'espère que ça vous a plu. Vos commentaires/remarques sont les bienvenus: