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 (+3/-0).

    Je teste dès que je rentre. :o

    • [^] # Re: Excellent !

      Posté par . Évalué à 1 (+1/-0).

      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 (+1/-0).

        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 (+5/-5). 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 (+5/-0).

    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 (+6/-0). 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 (+1/-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 (+1/-1).

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

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

  • # Classique ?

    Posté par (page perso) . Évalué à 4 (+2/-0).

    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 (+1/-0).

      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 (+1/-0).

      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 (+2/-0).

      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 (+3/-0).

        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.

Envoyer un commentaire

Suivre le flux des commentaires

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