Consulting, services, computer engineering. Implementation of technology solutions and support for businesses.

User Rating: 5 / 5

Star ActiveStar ActiveStar ActiveStar ActiveStar Active
 

 

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: