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 ?
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: Différence avec Frama-C/Value Analysis
Posté par KsassPeuk . En réponse au journal IKOS, un analyseur statique développé à la NASA. É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 ?
[^] # Re: intérêt de l'outil limité pour de l'embarqué.
Posté par KsassPeuk . En réponse au journal IKOS, un analyseur statique développé à la NASA. É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.