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 kp . Évalué à 3.
Je teste dès que je rentre. :o
[^] # Re: Excellent !
Posté par kp . É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 Maxime Arthaud . Évalué à 1.
Je n'ai eu aucun problème sous Debian 8 personnellement. Regarde ce Dockerfile.
En effet, je viens de voir ça. Étrange!
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 karchnu . Évalué à 1. Dernière modification le 14 décembre 2018 à 20:04.
… mais ça fait un peu "vu à la télé ! Wow !".
[^] # Re: Ton journal est pertinent
Posté par Maxime Arthaud . Évalué à 5.
D'accord. J'aurais peut-être du ajouter quelques exemples.
# Une bonne nouvelle pour les fans de microcontrôleur ?
Posté par Charly.the.daemon . É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 Maxime Arthaud . Évalué à 6. Dernière modification le 15 décembre 2018 à 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 Boiethios (site web personnel) . É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
[^] # Re: Vérification du code multi-threadé ?
Posté par cppuser . Évalué à 3.
Certes, mais s'il faut attendre 2030 je ne suis pas sûr que le matériel sera encore fonctionnel ;-D
[^] # Re: Vérification du code multi-threadé ?
Posté par Maxime Arthaud . Évalué à 3. Dernière modification le 15 décembre 2018 à 17:55.
Non, malheureusement on ne supporte pas le multi-thread.
# Licence Nasa
Posté par Sylvestre Ledru (site web personnel) . É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 Maxime Arthaud . Évalué à 3. Dernière modification le 17 décembre 2018 à 00:40.
C'est la licence de base pour les projets open source NASA. On ne m'a pas donné le choix.
[^] # Re: Licence Nasa
Posté par Sylvestre Ledru (site web personnel) . Évalué à 2.
J'avais lu que Apache 2 était aussi une option valide.
C'est plus le cas?
[^] # Re: Licence Nasa
Posté par Maxime Arthaud . Évalué à 1.
En effet, la NASA supporte aussi Apache.
En fait, ce projet a commencé en 2011 et a été publié à cette époque avec la licence NOSA, bien avant que j'arrive.
# Classique ?
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 4.
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 Harvesterify (site web personnel) . É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 Maxime Arthaud . É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 kp . É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 kantien . É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 Selso (site web personnel) . É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 KsassPeuk . Évalué à 2. Dernière modification le 21 janvier 2019 à 15:15.
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é".
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 :
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%.
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 Selso (site web personnel) . É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 David Mentré (site web personnel) . É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 KsassPeuk . É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 à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.