Analyse statique de code

Un article de Haypo.

Retour aux articles de sécurité

L'analyse statique de code consiste à rechercher de manière automatique les erreurs dans le code source d'un programme sans l'exécuter. Exemples d'erreurs détectées :

  • Faille de sécurité de type dépassement de tampon (buffer overflow)
  • Double lock dans un thread, ou encore sleep dans un lock
  • Mélange entre la mémoire de l'espace noyau et de l'espace utilisateur (les droits d'accès sont différents) : voir l'outil sparse pour le noyau Linux (lien donné plus bas)
  • etc.

Sommaire

[modifier] Liste des outils d'analyse statique

Outils que j'ai testé et apprécié :

  • FlawFinder (écrit en Python, cool) : Donne de bons résultats
  • ncc : Outil permettant de suivre les appels de fonction (on navigue dans le code source comme dans un navigateur web : liens pour rentrer en profondeur, et bouton précédent pour remonter au parent).
  • RATS : À utiliser avant FlawFinder car plus synthétique (regroupe les fichiers+lignes où l'on trouve les même erreurs). C'est le successeur de ITS4.
  • SPlint : Fonctionne plutôt bien et donne une très grande quantité d'avertissements (on peut filtrer les informations donées). Avant la version 3.0 (sortie en 2002), le programme s'appellait « LClint » (lire la FAQ de SPlint pour les détails).

Par ordre alphabétique (je n'en ai quasiment testé aucun) :

  • c : Analyse du code du noyau Linux, projet lancé par Peter T. Breuer
  • CCured qui est basé sur CIL (pour langage C), écrit dans le langage OCaml
  • Chic
  • Cqual : Moteur permettant de faire des vérifications nombreuses et variées. Le programme a l'air bien conçu (je n'ai testé que les exemples). => Langage C, mais une version pour C++ existe.
  • Csur : Csur is a project about automatic analysis of cryptographic protocols written in C
  • czech : voir un article présentant la projet, on y trouve des diapositives intéressantes. C'est un logiciel libre.
  • Focal
  • Insecure : Programme propriétaire de l'éditeur Parasoft
  • MOPS (écrit en C et en Java)
  • pscan : Recherche les erreurs possibles de formattage de chaîne dans un programme C
  • Smatch
  • sparse : L'outil développé initialement par Linus Torvalds pour détecter des erreurs dans le noyau Linux
  • Verisoft
  • Why : Générateur de preuve pour Coq en se basant sur des contrats


Pour Java :

  • ESC/Java : Compaq Extended Static Checker for Java (ESC/Java)

J'avais également lu un article dans le magazine MISC sur "Comment écrire des scripts IDC [ pour trouver des failles de sécurité ]" (dans l'excellent désassembleur IDA Pro). TODO : Retrouver la source ...

Projets anciens et qui risquent de ne plus compiler aujour'dhui ... (comme par exemple BOON) :

  • BOON : Buffer Overrun detectiON, écrit dans le langage ML

[modifier] Voir aussi

Langages de programmation orientés sécurité :

  • Cyclone : Langage de programmation basé sur le C, mais safe (sûr en anglais)
  • Vault : A programming language for reliable systems, under development at Microsoft Research.
  • Langages fonctionnels :
    • Erlang
    • Haskell
    • Lisp
    • Meta Language : Langage de programmation généraliste fonctionnel (article sur Wikipédia ML). Une implémentation moderne est l'Objective Caml ou « OCaml » qui est orienté objet et développé par l'INRIA
    • Oz
    • Scheme (dérivé du Lisp)
    • etc.

Articles :

[modifier] Analyse dynamique

Gestion de la mémoire :

  • ElectricFence par Bruce Perens
  • Memwatch (supporte aussi les overflow et underflow de tampon mémoire)
  • Valgrind : Excellent dans sa catégorie (traque les fuites mémoires et les accès illégaux, a une granularité d'un bit pour les accès !)

[modifier] Preuve formelle et vérification d'un modèle

Voir la liste des outils d'aide à la preuve formelle et vérification d'un modèle.

Logiciel français (cocorico ! :-)) développé par l'INRIA : « The Coq proof assistant ».

[modifier] Articles connexes

Récupérée de « http://www.haypocalc.com/wiki/Analyse_statique_de_code »