On a bien vu avec la faille sur OpenSSL que des milliers de paires d'yeux qui regardent le code dans le logiciel libre ne sont pas vraiment des milliers tous les jours. C'est même très surprenant étant donné l'importance de ce code et l'impact que peuvent avoir ses failles, et même le fait que j'imaginais naïvement que ce genre de code était très scrutés par des black/white hats.
Donc c'est acquis : seuls les développeurs du logiciel lisent vraiment le code, ça n'a pas l'air d'être une tâche intéressante pour un humain. Après … on a aussi des outils pour faire de l'analyse de code automatique non ? Et on a des organisations qui font du packaging à grande échelle de logiciels et qui font passer automatiquement des moulinettes dessus.
Donc question naïve étant donné que j'ai très peu d'expérience avec les outils d'analyse statique, est-ce qu'une distro ne pourrait pas lancer une moulinette sur les paquets compilé, et publier les rapports d'analyse sur un site dédié ou les envoyer aux mainteneurs, charge à la communauté de décortiquer les rapports et de marquer les faux positifs et les vrais problèmes ?
# Coverity
Posté par zul (site web personnel) . Évalué à 10.
Un peu comme Coverity (ça pue c'est pas libre mais ça trouve quelques bugs). En l'occurence, il n'avait pas detecté le bug dans OpenSSL.
[^] # Re: Coverity
Posté par Krunch (site web personnel) . Évalué à 5.
Voire aussi :
https://linuxfr.org/users/krunch/journaux/le-gouvernement-us-paie-laudit-de-projets-libres
https://linuxfr.org/users/krunch/journaux/le-gouvernement-us-paie-laudit-de-projets-libres-la-suite
pertinent adj. Approprié : qui se rapporte exactement à ce dont il est question.
[^] # Re: Coverity
Posté par F(log) . Évalué à 2.
La meme chose qui fait le ranking des projets en terme de code quality ? (vive C/C++ en open source)
C'est quoi exactement leur but?
[^] # Re: Coverity
Posté par Zenitram (site web personnel) . Évalué à 10. Dernière modification le 18 avril 2014 à 10:28.
Gagner leur vie sur un créneau pas encore trop saturé.
Sinon, le "ranking" est pour la pub, leur métier est l'audit de code (et c'est plutôt pas mauvais, après il fut prendre le temps de corriger)
[^] # Re: Coverity
Posté par Misc (site web personnel) . Évalué à 5.
Ouais, et puis des distributeurs commerciaux pourraient même payer des gens pour regarder le code et les résultats, genre comme :
http://osdir.com/ml/kde-commits/2013-01/msg08528.html
ou https://www.redhat.com/archives/pki-devel/2012-July/msg00057.html
Ou ce genre de boite pourrait payer des gens pour bosser sur l'analyse statique :
https://fedoraproject.org/wiki/StaticAnalysis
En fait, chaque fois qu'on voit "tel faille a été trouvé par $grosse_boite", c'est pas forcément par hasard. Avec grosse boite étant Google, Suse, IBM, Red Hat, etc.
La rubrique security de LWN permet de voir un peu, ou oss-sec. Par exemple, comme c'est vendredi, ici, on voit bien qu'il y a eu un audit de code de systemd :
http://seclists.org/oss-sec/2013/q4/4
( bien sur, le fait d'avoir des gens payé à faire ça, ça implique pas qu'on fasse pas aussi des choses en tant que communauté, et pour ma part, je compte bien m'attaquer à ça et prêcher la bonne parole comme j'ai fait à l'OWF )
[^] # Re: Coverity
Posté par Meku (site web personnel) . Évalué à 6.
C'est parce que la NSA a introduit une faille dans Coverity pour qu'il ne détecte pas la faille qu'ils ont introduit dans OpenSSL ! COMPLOT !!!
[^] # Re: Coverity
Posté par Maclag . Évalué à 7.
Oui mais pourquoi la NSA fait tout ça?
C'est parce qu'elle est entièrement contrôlée par des cellules judéo-maçonniques qui cherchent à établir un Nouvel Ordre Mondial.
Et pourquoi les Juifs-Franc-Maçons veulent établir un NOM?
Mais enfin c'est évident: ils ont été infiltrés par des extra-terrestres!
Quasiment personne n'est au courant de l'existence des extra-terrestres, sauf la CIA! La CIA le sait parce qu'elle espionne la NSA, qui elle-même espionne les extra-terrestres, qui contrôlent les Franc-Maçons, qui contrôlent la NSA, qui contrôle le FBI, qui contrôle secrètement la CIA, qui contrôle le gouvernement américain, qui lui-même négocie avec les extra-terrestres.
Tout se tient!
[^] # Re: Coverity
Posté par Donk . Évalué à 2.
Encore un coup des chinois du FBI
[^] # Re: Coverity
Posté par Lutin . Évalué à 3.
Tu as oublié d'introduire l'assassinat Kennedy, le "suicide" de Kurt Cobain, la vraie raison de la seconde guerre mondiale et l'arrêt du LHC dans ton complot.
[^] # Re: Coverity
Posté par Krunch (site web personnel) . Évalué à 6.
Ainsi que la cabale DLFP.
pertinent adj. Approprié : qui se rapporte exactement à ce dont il est question.
# quitte à crowdsourcer
Posté par feth . Évalué à 8.
Pourquoi ne pas crowdsourcer en utilisant les failles comme on utilise les captchas pour reconnaître des numéros de rue ?
Madame et monsieur Michu vont moins faire les malins.
# euh...
Posté par antistress (site web personnel) . Évalué à 1.
J'ai hésité à plusser ou moinsser le journal, car je trouve l'idée de l'auteur intéressante mais je n'apprécie qu'il la qualifie de stupide…
[^] # Re: euh...
Posté par Thomas Douillard . Évalué à 4.
J'aurai du mettre "naïve", c'est vrai :) Si ça se trouve j'étais déjà tombé sur le projet de Sylvestre et je m'en souviens pas /o.
[^] # Re: euh...
Posté par BAud (site web personnel) . Évalué à 2.
/me file un \ à thoasm< (http://xkcd.com/859/
/o\
# Ça existe ou ça a existé :
Posté par kp . Évalué à 10.
Pour Debian, avec scan-build, l'analyseur statique de LLVM grâce à Sylvestre Ledru.
Il y a eu un GSoC qui a donné debile (lien mort ?) pour enrober tout cela. On en parle rapidement là. On dirait que ça n'est plus accessible, c'est dommage.
Je ne sais pas quel impact ça a eu (en termes de découverte et de correction de bugs).
J'imagine et j'espère que d'autres distributions essayent de faire des choses similaires.
[^] # Re: Ça existe ou ça a existé :
Posté par Thomas Douillard . Évalué à 3.
Ben si il passe dans le coin, faudrait qu'il nous donne des nouvelles :)
[^] # Re: Ça existe ou ça a existé :
Posté par Sylvestre Ledru (site web personnel) . Évalué à 10.
On a eu deux donations (Google & IRILL). On a acheté plein de serveurs avec. On a commencé la migration (d'où le site inaccessible) mais j'ai changé de boulot (donc avec le bootstrap, j'ai un peu moins de temps), et, surtout, le projet Tanglu a décidé d'adopter la partie build (pas la partie analyseur statique) et ils ont fait pas mal de modifications donc ça a repoussé la release… Ca devrait être en ligne d'ici quelques semaines.
On
vadevrait avoir un étudiant GSoC (mais faut pas lui dire, c'est pas encore officiel) pour travailler dessus pendant l'été mais l'idée générale est d'avoir pour chaque package Debian:* build avec gcc
* build avec clang
Analyseurs statiques:
* C++ avec clang analyzer / scan-build
* C++ avec cpplint
* lintian
* Java avec findbugs
* C/C++ avec Coccinelle
Apres, on devrait en rajouter d'autres (Javascript, Python, etc).
Bref, c'est pas du tout mort…
[^] # Re: Ça existe ou ça a existé :
Posté par barmic . Évalué à 10.
N'hésite pas à nous tenir au courant de l'évolution !
Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
[^] # Re: Ça existe ou ça a existé :
Posté par kp . Évalué à 1.
Ouf ! Ça me rassure. Merci pour ces très bonnes nouvelles.
[^] # Re: Ça existe ou ça a existé :
Posté par Sylvestre Ledru (site web personnel) . Évalué à 3.
s/cpplint/cppcheck/ j'ai mélangé avec pylint!
[^] # Re: Ça existe ou ça a existé :
Posté par Kioob (site web personnel) . Évalué à 1.
D'ailleurs, Debian vient de publier une nouvelle version du paquet openssl, sensé corriger 3 failles.
Est-ce grâce à ces outils d'analyse, ou simplement parce qu'un grand nombre de paires d'yeux se sont finalement penché sur le code ?
alf.life
[^] # Re: Ça existe ou ça a existé :
Posté par pasBill pasGates . Évalué à 2.
Je ne vois que 2 failles, dont une datant de 2010…
[^] # Re: Ça existe ou ça a existé :
Posté par Kioob (site web personnel) . Évalué à 2. Dernière modification le 19 avril 2014 à 14:28.
Pour celle marquée 2010, oui j'ai eu un doute aussi, si je comprends bien ces indications le bug a été identifié en 2010, mais ce n'est que récemment qu'il a été considéré comme problème de sécurité (et donc qu'il n'avait pas été backporté jusque là).
Quant au nombre il y en a bien 3 comme expliqué dans le message de Debian, mais la troisième n'a pas (encore ?) de numéro de CVE. Je cite :
alf.life
[^] # Re: Ça existe ou ça a existé :
Posté par Thierry Thomas (site web personnel, Mastodon) . Évalué à 6.
Il y a déjà un bon paquet d’années, je maintenais le port FreeBSD de xtel, un émulateur Minitel, et un jour j’avais reçu un courrier du "ports manager" de l’époque qui s’occupait de la production des paquets binaires et qui m’avait signalé un buffer overflow : en fait, après avoir créé les paquets, il avait une procédure qui les installait et qui faisait du fuzzing dessus. Par contre, je ne pense pas que c’était systématique, mais plutôt par échantillonnage.
D’autre part, il y a aussi des outils d’analyse des sources – ne serait-ce que sans outils supplémentaires les vérifications de clang et de plus en plus de Gcc –, mais c’est loin d’être automatisable à 100 % ! Il y a plein de faux positifs qui doivent être annotés, et ça demande une analyse humaine longue et complexe.
# Debile
Posté par claudex . Évalué à 10.
C'est tellement stupide que ça en devient complètement Debile
« Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche
[^] # Re: Debile
Posté par claudex . Évalué à 10.
À force de réfléchir des heures à ma formulation, je me suis fais grillé.
« Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche
# Les analyseurs ne sont pas non plus une panacee
Posté par reno . Évalué à 8.
Dans le cas d'openssl il y a eu des analyses, mais elles ont loupes ce bug, cf http://blog.regehr.org/.
L'analyse ne fait pas tout, après il faut distinguer les faux positif des vrais bugs, corriger le bug sans en introduire un nouveau (Debian..)
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Patrick Nicolas . Évalué à 6. Dernière modification le 18 avril 2014 à 08:13.
Un analyseur de code va chercher des mauvaises utilisations du langage : valeurs non initialisées, mémoire non libérée, comportement non défini ou ambigüité pour le lecteur.
Dans le cas de openSSL c'est une catégorie de failles qui peut être détectée automatiquement mais avec certaines limites. Le problème était de lire une adresse d'un tableau sans vérifier la taille, en C un tableau est simplement un pointeur vers le premier élément et l'information de son type. L'analyseur devrait donc pouvoir retracer comment la mémoire a été attribuée pour savoir si la lecture est valide. Si il y a un appel de fonction entre les deux, l'analyse devrait se faire sur le programme entier et non les fichiers séparément.
Je suis du genre à lancer tous les compilateurs et analyseurs que je trouve avec le niveau maximal d'avertissements pour me rassurer, mais je sais que ça n'est pas (encore) suffisant.
PS : on peut configurer le correcteur d'orthographe de linuxfr pour qu'il accepte la réforme de 1990 ? Il n'aime pas mon tréma sur ambigüité.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par feth . Évalué à 10.
Je préfèrerais qu'on fasse un linuxfr à part pour les gens qui préfèrent l'orthographe imprévisible et capricieuse de 1990.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par ariasuni . Évalué à 2.
Pas plus imprévisible que l’orthographe traditionnelle. Au contraire.
Écrit en Bépo selon l’orthographe de 1990
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par feth . Évalué à -2. Dernière modification le 23 avril 2014 à 09:44.
Tout dépend de tes références. Si ta référence est le français parlé (et non le français de l'école normale en 1850), je pense qu'il serait encore plus simple de supprimer complètement l'orthographe (et perso, en dehors de la littérature et des communications formelles, c'est à dire, sur linuxfr, les dépêches par opposition aux journaux, je serais plutôt partisan de cette option).
Edit: il n'y a pas «linuxfr» dans le dictionnaire de linuxfr.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par ariasuni . Évalué à 2.
Je ne suis pas du tout d’accord avec cette option:
Comme il y a plusieurs façons d’écrire chaque son, chacun écrit comme il veut, du coup c’est très difficile de reconnaitre un mot, à la fois pour un humain et pour le correcteur orthographique et/ou grammatical peut alors difficilement aider.
Bref, les règles devraient être beaucoup plus simple qu’actuellement, mais l’orthographe de 1990 est déjà un (petit) pas en avant. Elle corrige quand même un certain nombre d’anomalies et supprime pas mal d’exceptions.
Écrit en Bépo selon l’orthographe de 1990
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Sytoka Modon (site web personnel) . Évalué à 2.
J'avais lu quelques pars qu'elle rajoutais autant d'exception qu'elle en enlevait…
Ceci, comme Voltaire, je suis partisan d'un grand nettoyage et virer les exceptions en Choux, Hiboux, Pneu… et autres conneries qui bouffent un temps fou au primaire pour une utilité plus que moyenne. D'ailleurs, en espagnol, on dis Farmacia et Fotographia et cela n'empêche personne de dormir ;-)
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par BAud (site web personnel) . Évalué à 1.
s/quelques pars/quelques part/
s/Fotographia/fotografía/
Reste à enlever les verbes irréguliers en anglais et effectivement les études seront plus simples, permettant d'ajouter l'espéranto grâce au temps gagné.
De rien ;-)
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par ariasuni . Évalué à 2.
C'est pas «quelque part»?
Ou les règles de conjugaison en français. Ou simplifier la prononciation de l'anglais. Ou simplifier sa grammaire.
Ou utiliser l'espéranto.
Écrit en Bépo selon l’orthographe de 1990
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Sytoka Modon (site web personnel) . Évalué à 6.
C'est normal, il faut chercher à la lettre D. On l'écrit DLFP. C'est une des exceptions du Français ;-)
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par totof2000 . Évalué à 4.
Je ne connais pas Ada sur le bout des doigts, mais j'en ai quelques notions et il me semble qu'avec ce langage, il y aurait eu moyen de détectyer ce genre de bug. Y a-t-il des connaisseurs ici qui pourraient confirmer ?
Sinon, une solution à ce genre de problème ne serait-il pas d'utiliser un langage comme Ada pour développer des fonctionnalités secure, (ou - vu que c'est la mode en ce moment - inventer un langage qu'on appellerait "trusted C" par exemple et qui s'inspirerait de la syntaxe du C, permettrait de développer des libs interfacables facilement avec des progs C, mais aurait tous les contrôles que fait Ada à la compilation)
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Thomas Douillard . Évalué à 4.
Pour le C, je crois qu'il y a des normes industrielles, et juste une requête google "j'ai de la chance" donne ça par exemple : http://vst.cs.princeton.edu/veric/
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par totof2000 . Évalué à 4. Dernière modification le 18 avril 2014 à 11:45.
Intéressant comme lien. Je vais jeter un oeil. PAr contre, je serais intéressé par une comparaison avec Ada, si quelqu'un a les compétences pour le faire. Mais si ce genre d'outil permet de produire du code plus sûr, alors pourquoi ne pas l'utiliser, au moins sur les parties sensibles telles que les modules de crypto ?
Sinon, est-ce que toi (ou un auitre participant) aurait des exemples d'utilisation de ce genre d'outil ?
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Thomas Douillard . Évalué à 7.
Dans le genre méthodes formelles appliquées, il y a la méthode B, qui produit en sortie du C ou de l'ADA, avec tout démontré y compris le compilateur.
Méthode B
La boite qui fait le site http://www.methode-b.com/ en vit, ça a produit le code de la ligne de métro automatisée à Paris.
Sinon je dirai que ça demande des compétences qui sont pas celles du codeur de site PHP moyen, mais dans le domaine de la sécurité il y a des passionnés qui devraient s'y intéresser, c'est évident. Les méthodes formelles ont jusqu'à présent peinées à s'imposer, faute au surcout perçu et à la difficulter de former des gens (la méthode B était enseignée dans l'IUT de Nantes ou j'ai fait mon DUT, la plupart des têtes de l'amphi étaient un peu paumées bien qu'on ait rien fait de bien compliquée, faute au choc des cultures plus qu'à une réelle complexité je pense, et bien que le prof (avec une personnalité particulière et pas forcément adapté à la pédagogie) ait beaucoup réfléchi à la question de la transmission.
Il suffit de regarder le décallage entre le récent prix Turing et ses article ou il déplore qu'on cherche pas à écrire des specs potables pour démontrer que le code les vérifie : http://www.wired.com/2013/01/code-bugs-programming-why-we-need-specs/ idées qui sont jamais trop passées dans l'industrie de masse. Mais qui sais, le temps est peut être venu ?
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 7.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Blackknight (site web personnel, Mastodon) . Évalué à 3.
C'est justement l'objet d'une discussion en cours sur le newsgroup comp.lang.ada.
Pour faire court, un des principaux écueils est la disponibilité d'un compilateur Ada sur toutes les plateformes censées faire tourner OpenSSL.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par totof2000 . Évalué à 2.
Merci, c'est bien ce qu'il me semblait, vu ce que je connais du langage.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par ariasuni . Évalué à 2.
Le Rust est peut-être la solution à ce problème. Reste qu’il faudra quand même un peu de temps pour que le langage murisse et soit considéré assez sûr pour faire des bibliothèque de sécurité (et surtout que quelqu’un ai envie de s’y coller).
Écrit en Bépo selon l’orthographe de 1990
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Philip Marlowe . Évalué à 3.
Il faut te sortir de cette ambiguïté.
# Coccinelle
Posté par vlamy (site web personnel) . Évalué à 7.
Il y a Coccinelle aussi, qui est orienté C et est utilisé, notamment, sur le kernel Linux. Il paraît que c'est pas mal et en plus c'est Français :)
# Fuzzing technologies
Posté par kadreg . Évalué à 8.
Dans le cadre d'OpenSSL, la découverte par codenomicon s'est fait en utilisant leur technologie de Fuzzing (Codenomicon Defensics). Le fuzzing, c'est une analyse boite noire. On défini le protocole utilisé, et le fuzzer va forger des requêtes mal formées pour valider le comportement correct sur un input incorrect. Sachant que dans le cas de defensics, le coté mal formé peut être plus bas que le niveau protocolaire.
Pour avoir une idée de comment ça marche, leur site de fuzz-o-matic est assez sympa: http://www.codenomicon.com/fuzzomatic/
A noter que ce test va détecter une potentialité de bug exploitable : ce n'est pas aprce que ça plante qu'on peut faire plus que ça, cela demande une post-analyse.
D'ailleurs, codenomicon fait de temps en temps des analyses sur logiciels libres.
[^] # Re: Fuzzing technologies
Posté par barmic . Évalué à 4.
La difficulté de ces tests c'est de détecter les cas d'erreurs.
Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
[^] # Re: Fuzzing technologies
Posté par pasBill pasGates . Évalué à 4.
Avec le fuzzing justement pas non, car le resultat est habituellement un crash, c'est facile a voir :)
A mon avis d'ailleurs Codenomicon n'a probablement pas trouve ce bug en faisant tourner leur fuzzer, mais plutot de maniere manuelle( a mon avis ils etaient en train de regarder des captures de traffic ssl pendant du developpement/test de leur fuzzer et ils ont vu qqe chose de bizarre dans le paquet, ils ont gratte un peu plus et on vu), car il n'est pas aise de detecter un info leak.
# Vérification formelle
Posté par davandg . Évalué à 4.
Pour un logiciel aussi critique, ne faudrait-il pas faire de la vérification formelle ?
(C'est une vrai question)
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . Évalué à 4.
C'est un peu la question générale et le thème des réponses apportées. Qu'entends tu par vérification formelle ? Il y a de très nombreuses méthodes, l'aspect difficile étant de modéliser le programme à vérifier et de définir la spécification dans le même formalisme.
[^] # Re: Vérification formelle
Posté par Thomas Douillard . Évalué à 6. Dernière modification le 18 avril 2014 à 13:43.
C'est ce que fait la méthode B, les spécifications générales sont faite dans le même langages, ensuite on comble les trous en implémentant petit à petit, et en vérifiant que ce qu'on a écrit correspond bien avec ce qu'on a écrit à l'étape de ''raffinage'' précédente.
Ça m'a fait un peu penser au système de ''trou'' dans le code que la dernière version d'Haskell a introduit, cf. la dépêche : on a des bouts de code pas implémenté, mais le compilo donne le type de ce qui reste à faire.
PS: je crois que je viens de trouver un bug : il y a
Vous avez jugé ce commentaire inutile. qui s'affiche sur ma page, mais un seul +1 pour le commentaire, et je pense avoir cliqué sur pertinent.
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . Évalué à 2. Dernière modification le 18 avril 2014 à 14:51.
La méthode B est un exemple des très nombreuses façons de faire de la vérification formelle (encore que B ne fait pas que de la vérification). Il faut aussi regarder toutes les implémentations de model checking, pour ce qui est de la logique temporelle majoritairement, mais aussi les assistants de preuves comme Coq ou encore les outils de comparaison type boite noire, souvent basés sur de la bissimulation, justement pour montrer qu'un programme est bissimilaire à une spécification. Il existe encore d'autres domaines de vérification formelle, donc c'est très très large et cela ne se réduit pas à la méthode B (qui, d'après ce que j'en ai entendu par un de ses concepteurs, a permis de trouver un bug dans le simulateur utilisé pour valider le programme de la ligne 14).
Pour ce qui est de cette histoire de bug sur le karma (pertinent/inutile), je n'ai rien compris, mais si c'est la question, je n'ai jamais cliqué sur le lien « inutile » de quelque commentaire que ce soit :)
[^] # Re: Vérification formelle
Posté par Thomas Douillard . Évalué à 2.
Sans compter les techniques d'interprétations abstraite qui peuvent prouver certains trucs aussi.
[^] # Re: Vérification formelle
Posté par davandg . Évalué à 1.
Connais-tu des tutos pour appliquer ces méthodes à du code C ?
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . Évalué à 2.
Non je ne connais pas de tuto, malheureusement.
Par contre, ce qui est sûr, c'est que tous les gens que j'ai vu coder sur des trucs critiques n'utilisaient pas C, ou alors via des générateurs de code, comme c'est le cas notamment dans certaines branches de l'aéronautique.
[^] # Re: Vérification formelle
Posté par gnx . Évalué à 4.
Moi, ce qui est sûr, c'est que je n'ai vu que du C sur les trucs critiques que j'ai rencontrés :-)
[^] # Re: Vérification formelle
Posté par lasher . Évalué à 4.
Vous n'avez pas forcément la même notion de ce qui est critique. :-)
De plus, même lorsque la performance est effectivement critique, disons dans l'embarqué, il y a tout un tas de choses interdites même si le C les autorise : allocation dynamique, récursion, etc.
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . Évalué à 4. Dernière modification le 24 avril 2014 à 07:45.
C'est vrai que ce que j'entends par critique c'est le point de vue sécurité (bug = potentielle mort d'homme). Il est vrai que si tu as des contraintes temps réel cela peut changer, mais je n'ai jamais vu de tel code et il me semblait que l'aérospatial misait beaucoup sur Ada pour ce genre de chose notamment.
Sinon tu n'as jamais vu d'Ada ou de Caml ?
[^] # Re: Vérification formelle
Posté par gnx . Évalué à 4.
Je sais ce que critique et sécurité veulent dire. Des réacteurs nucléaires, entre autres, ça doit compter :-)
Attention, ma remarque était juste pour contrebalancer la portée de ta constatation personnelle. Je ne nie en aucun cas qu'on puisse trouver de l'Ada, je tenais juste à dire que le C existe dans les systèmes critiques et qu'on peut encore ne faire que ça. Jamais entendu parler de Caml dans ces domaines, par contre (ce qui ne veut pas dire que ça n'existe pas non plus).
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . Évalué à 2.
Y a pas de soucis :)
[^] # Re: Vérification formelle
Posté par kp . Évalué à 2.
Des gens le font, mais pas gratuitement :
http://www.astree.ens.fr/
https://en.wikipedia.org/wiki/Astr%C3%A9e_(static_analysis)
C'est utilisé dans l'aéronautique (pour éviter les avions ou les fusées qui se crashent à cause d'un dépassement de tampon).
[^] # Re: Vérification formelle
Posté par nonas . Évalué à 5.
Déjà rapporté (voir ma réponse à nono).
# 42^W Réponse bookmark
Posté par Thierry Thomas (site web personnel, Mastodon) . Évalué à 2.
J’arrive un peu tard, mais bon, ça sera pour la postérité : David Wheeler publié une réponse très intéressante qui répond à la question posée.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.