Journal IKOS, un analyseur statique développé à la NASA

Posté par . Licence CC by-sa.
Tags : aucun
60
14
déc.
2018

Salut à tous,

Laissez moi vous présenter IKOS: https://github.com/NASA-SW-VnV/ikos

IKOS est un analyseur statique pour C et C++ basé sur LLVM, développé à la NASA. Il est gratuit et open source.

IKOS permet de détecter des bugs dans vos programmes C et C++. Contrairement à un analyseur statique « classique », il se repose sur une théorie mathématique appelée Interprétation Abstraite. IKOS prouve automatiquement l’inexistence de bugs dans vos programmes, pour toutes les exécutions possibles. En contrepartie, IKOS peut générer des faux positifs, dans les cas où le code n'a pas pu être prouvé correct par l'analyse. IKOS est similaire à Polyspace, Astrée ou Frama-C (analyse de valeur).

IKOS peut détecter la plupart des bugs en C, tels que les débordements de tampon, les divisions par zéro, etc. La liste complète (en anglais) est disponible ici. Cette liste est globalement similaire à la liste des checks d'UBSan. IKOS peut aussi être utilisé pour prouver une condition arbitraire, en utilisant __ikos_assert(condition).

IKOS a été conçu pour analyser des codes de systèmes embarqués écrit en C, et c'est la qu'il est le plus efficace.

Pour tout problème, n'hésitez pas à ouvrir un rapport de bug sur Github (en anglais si possible). Nous apprécions aussi les retours par email: ikos@lists.nasa.gov

  • # Excellent !

    Posté par . Évalué à 3.

    Je teste dès que je rentre. :o

    • [^] # Re: Excellent !

      Posté par . Évalué à 1.

      Bon je n'ai pas beaucoup cherché, mais je n'ai pas réussi à faire marcher ça sur debian 8 (galère avec le changement d'abi des compilos, puis boost filesystem qui m'envoie chi… à l'exécution).

      J'ai réessayé aujourd'hui au boulot (ubuntu 18) aucun souci majeur.
      (Juste ça ne compile pas avec ninja ?!?)
      J'aurais aimé le passer sur le code du boulot, mais si j'ai bien compris, il n'y a pas de moyen d'analyser des bibliothèques dynamiques ?
      Ou alors je n'ai pas trouvé comment passer un entry-point à scan-ikos ?

      • [^] # Re: Excellent !

        Posté par . Évalué à 1.

        Bon je n'ai pas beaucoup cherché, mais je n'ai pas réussi à faire marcher ça sur debian 8 (galère avec le changement d'abi des compilos, puis boost filesystem qui m'envoie chi… à l'exécution).

        Je n'ai eu aucun problème sous Debian 8 personnellement. Regarde ce Dockerfile.

        (Juste ça ne compile pas avec ninja ?!?)

        En effet, je viens de voir ça. Étrange!

        J'aurais aimé le passer sur le code du boulot, mais si j'ai bien compris, il n'y a pas de moyen d'analyser des bibliothèques dynamiques ?
        Ou alors je n'ai pas trouvé comment passer un entry-point à scan-ikos ?

        Malheureusement, on ne peut pas analyser de bibliothèques dynamiques avec ikos.
        Par contre, tu peux créer un programme qui va appeler les fonctions de ta bibliothèque de façon arbitraire, et lancer ikos dessus.

  • # Ton journal est pertinent

    Posté par . Évalué à 1. Dernière modification le 14/12/18 à 20:04.

    … mais ça fait un peu "vu à la télé ! Wow !".

  • # Une bonne nouvelle pour les fans de microcontrôleur ?

    Posté par . Évalué à 5.

    Systèmes embarqués dans le sens bare metal, sans OS ?

    • [^] # Re: Une bonne nouvelle pour les fans de microcontrôleur ?

      Posté par . Évalué à 6. Dernière modification le 15/12/18 à 01:11.

      En général, les projets utilisant IKOS en interne tournent sur un système d'exploitation temps réel.
      En pratique, rien ne t'empêche d'utiliser IKOS pour un système sur bare metal. Dans ce cas, il te faudra probablement utiliser l'option --no-libc lors de l'analyse.

  • # Vérification du code multi-threadé ?

    Posté par (page perso) . Évalué à 1.

    Je n'arrive pas à trouver d'infos dessus, mais vérifie-t-il si un code multi-threadé est correct ?

    De toute façon, ça ne peut être qu'un outil temporaire, en attendant de porter le code en Rust :P

  • # Licence Nasa

    Posté par (page perso) . Évalué à 2.

    Quel dommage d'avoir choisi cette licence par contre… :/

    J'ai ouvert ce ticket: https://github.com/NASA-SW-VnV/ikos/issues/42

    • [^] # Re: Licence Nasa

      Posté par . Évalué à 3. Dernière modification le 17/12/18 à 00:40.

      C'est la licence de base pour les projets open source NASA. On ne m'a pas donné le choix.

  • # Classique ?

    Posté par (page perso) . Évalué à 4.

    Contrairement à un analyseur statique « classique », il se repose sur une théorie mathématique appelée Interprétation Abstraite.

    Euh, je suis le seul à trouver que l'interprétation abstraite, c'est tout à fait classique pour l'analyse statique ? Cousot et Cousot 77, ça a été publié il y a 41 ans, quand même…

    • [^] # Re: Classique ?

      Posté par (page perso) . Évalué à 2.

      En effet, la plupart des analyseurs sérieux reposent sur l'interprétation abstraite (Frama-C, Astrée, CodeProver, cités dans le post originel).

      Il serait intéressant de comparer les fonctionnalités offertes vis à vis des autres outils cités précédemment

      Mes messages engagent qui je veux.

    • [^] # Re: Classique ?

      Posté par . Évalué à 1.

      Quand je disais « classique », je pensais à cppcheck, clang-tidy et autre. C'est à dire, des analyseurs avec des heuristiques pour trouver des bugs.

      C'est vrai que l'interprétation abstraite à 40 ans, mais en général quand je parle avec des ingénieurs, ils n'ont aucune idée de ce que c'est.

    • [^] # Re: Classique ?

      Posté par . Évalué à 2.

      C'est classique effectivement, mais je ne connais pas d'analyseur statique libre qui utilise ça ? Me trompe-je ?

      • [^] # Re: Classique ?

        Posté par . Évalué à 5.

        Frama-C est sous LGPL avec des parties en BSD.

        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

  • # intérêt de l'outil limité pour de l'embarqué.

    Posté par (page perso) . Évalué à 1.

    Qu'on me corrige si je me trompe mais pour moi cet outil ce rapproche plus de frama-C que de cppcheck.
    De souvenir avec Frama-C il fallait écrire du code pour l'analyse de source. Mais enfin c'était peut-être pour des fonctions de "couverture de code".

    Pour de l'embarqué (monde des uC) c'est toujours compliqué vu que l'on a des dépendances sur le matériel, et que l'outil qui s'exécute sur le PC ne peut réaliser une analyse complète (j'ai vu que ces analyseurs compilait le code).
    Pour moi l'intérêt serait confirmé si l'outil pouvait répondre la conformité du code par rapport à la norme MISRA-C. Et forcément ça demande plus que de la détection de bug/faille.

    On ajoutera à ça le besoin d'avoir des métriques "personnalisées" dans les métriques.

    Pour un client j'avais utilisé OClint :
    - analyse statique basée sur LLVM
    - système d'intégration de métriques personnalisée sous la forme d'un fichier de conf et de DLL permettant de vérifier la convention de nommage et autres regles basées sur des regex permettant d'analyser l'AST généré ou le nombre cyclomatique d'une fonction.
    - à ça vous ajoutez la génération d'un rapport type tableur pour toutes les anomalies, que l'on pouvait trier par niveau de gravité.

    Pour l'analyse statique, comme il fallait compiler les fichiers que l'on avait un projet type 'Makefile générique', on a utilisé bear pour générer une base JSON de compilation de fichiers individuel (que sait générer cmake).

    Ca marchait très bien sous Linux x86.
    Mais voilà pour de l'embarqué uC ca perd de sa saveur car la compilation n'est plus possible à moins d'avoir un LLVM configuré pour la cible ou un code source instrumenté pour permette une analyse partielle.
    On doit avoir le même pb avec cet outil non ?

    • [^] # Re: intérêt de l'outil limité pour de l'embarqué.

      Posté par . Évalué à 2. Dernière modification le 21/01/19 à 15:15.

      De souvenir avec Frama-C il fallait écrire du code pour l'analyse de source. Mais enfin c'était peut-être pour des fonctions de "couverture de code".

      C'est un peu inexact tout dépend du degré de sûreté que l'on souhaite établir.

      Typiquement montrer que le code ne contient pas de runtime errors (donc accès pourris, etc), ne demande généralement pas (ou très peu) de travail d'annotations. En gros, on configure quelques petites choses (par exemple, les adresses matérielles qui sont valides, la précision de l'analyse, etc), on pousse le bouton et on attend le résultat.

      Après, effectivement, on peut vouloir aller plus loin en montrant que le code a certaines bonnes propriétés (en plus de ne pas en avoir de mauvaises), et là ça nécessite effectivement d'exprimer à l'outil ce qu'on entend par "bonne propriété".

      Pour moi l'intérêt serait confirmé si l'outil pouvait répondre la conformité du code par rapport à la norme MISRA-C. Et forcément ça demande plus que de la détection de bug/faille.

      C'est assez bizarre comme idée de qualifier MISRA d'un super haut niveau de sûreté. Les règles MISRA donnent des directives pour améliorer le niveau de sûreté, mais ne donnent pas de "garantie" (façon de parler) que ça entraînera l'absence de problèmes.

      Il y a quelques distinctions à faire, notamment le but de l'outil :

      • limiter la création de problèmes,
      • garantir l'absence de création de problèmes,
      • détecter la présence de problèmes,
      • assurer l'absence de problèmes

      MISRA c'est le premier point, mais ça ne donne pas de garantie. Pour cela, il y a d'autres outils qui permettent par exemple de générer du C correct (méthode B, ou encore F-Star), et c'est le second point.
      Même quand on a suivi MISRA, on peut encore chercher à détecter des problèmes (point 3), si on a suivi MISRA, il n'est pas sûr que les outils en trouvent mais ce n'est pas impossible.

      Ici, je ne sais pas à quoi on a à faire exactement (je n'ai pas encore regardé en détail), mais des outils comme Astrée ou l'interprétation abstraite de Frama-C appartiennent au quatrième point. On ne laissera pas passer un problème (et on a de bonnes chances même, de générer de fausses alarmes), s'il a la moindre chance de pouvoir se présenter.

      EDIT: de ce que je lis IKOS n'est pas un analyseur dit "sound" comme l'interprétation abstraite de Frama-C ou Astrée peuvent l'être. L'idée est d'avoir un taux de précision supérieur à 90%.

      Mais voilà pour de l'embarqué uC ca perd de sa saveur car la compilation n'est plus possible à moins d'avoir un LLVM configuré pour la cible ou un code source instrumenté pour permette une analyse partielle.
      On doit avoir le même pb avec cet outil non ?

      Pour celui là je ne sais pas, mais pour des outils comme Astrée ou Frama-C, ils sont assez configurables de ce côté même si ça demande pas mal d'huile de coude.

      • [^] # Re: intérêt de l'outil limité pour de l'embarqué.

        Posté par (page perso) . Évalué à 0.

        Bonjour,
        Merci de cette réponse.
        De ma petite expérience Frama-C (Linux Mag), on visait beaucoup plus haut. Je vois la norme MISRA-C comme l'un des premiers échelons de garantie de qualité du code, connu de tous (puisque c'est une norme).
        Et c'est n'est pas si simple a appliquer dans mon cas, sans passer par une revue de code.

  • # Différence avec Frama-C/Value Analysis

    Posté par (page perso) . Évalué à 1.

    Bonjour,

    Pourquoi un nouvel analyseur a été développé au lieu d'utiliser Frama-C/Value Analysis ?

    Quels intérêts et différences principales d'IKOS par rapport à Frama-C/Value Analysis au jour d'aujourd'hui ?

    Merci,
    david

    • [^] # Re: Différence avec Frama-C/Value Analysis

      Posté par . Évalué à 0.

      De ce que je comprends de leur publi, ici ils visent la détection et pas la garantie d'absence de problèmes. Donc ils essaient de limiter les faux positifs, quitte à en laisser passer un peu.

      C'est assez étrange du coup, d'utiliser l'interprétation abstraite pour concurrence des méthodes heuristique. Mais si ça marche, pourquoi pas ?

Suivre le flux des commentaires

Note : les commentaires appartiennent à ceux qui les ont postés. Nous n'en sommes pas responsables.