Journal Idée stupide sur la sécurité du code

Posté par . Licence CC by-sa
Tags : aucun
19
17
avr.
2014

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 (page perso) . É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 (page perso) . Évalué à 5.

    • [^] # Re: Coverity

      Posté par . É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 (page perso) . Évalué à 10. Dernière modification le 18/04/14 à 10:28.

        C'est quoi exactement leur but?

        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 (page perso) . É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 (page perso) . É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 . É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 . Évalué à 2.

          Encore un coup des chinois du FBI

        • [^] # Re: Coverity

          Posté par (page perso) . É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 (page perso) . Évalué à 6.

            Ainsi que la cabale DLFP.

            pertinent adj. Approprié : qui se rapporte exactement à ce dont il est question.

  • # quitte à crowdsourcer

    Posté par (page perso) . É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 (page perso) . É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…

  • # Ça existe ou ça a existé :

    Posté par . É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 . 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 . É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 (page perso) . É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 (page perso) . Évalué à 6.

      J'imagine et j'espère que d'autres distributions essayent de faire des choses similaires.

      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 (page perso) . É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 (page perso) . É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 . É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 . Évalué à 6. Dernière modification le 18/04/14 à 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 (page perso) . É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 (page perso) . É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 (page perso) . Évalué à -2. Dernière modification le 23/04/14 à 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 (page perso) . Évalué à 2.

              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).

              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 (page perso) . Évalué à 2.

                Elle corrige quand même un certain nombre d’anomalies et supprime pas mal d’exceptions.

                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 (page perso) . É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 (page perso) . Évalué à 2.

                    s/quelques pars/quelques part/

                    C'est pas «quelque part»?

                    Reste à enlever les verbes irréguliers en anglais

                    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 (page perso) . Évalué à 6.

              Edit: il n'y a pas «linuxfr» dans le dictionnaire de linuxfr.

              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 . Évalué à 4.

        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 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 . É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 . Évalué à 4. Dernière modification le 18/04/14 à 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 . É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 ?

        • [^] # Re: Les analyseurs ne sont pas non plus une panacee

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

          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 ?

          Avec Ada, plusieurs possibilités :
          - utilisation de tableau contraint : détection à la compilation
          - utilisation de tableau non contraint : détection à l'exécution

          Utilisation de pointeur : c'est tellement "lourd" syntaxiquement parlant qu'en général, on évite sauf si on est vraiment obligé. Et là encore, le langage met pas mal de gardes fou (qui ne font pas tout, certes, mais par exemple, il n'est pas possible d'avoir un pointeur sur une variable sans avoir déclarée explicitement que cette variable pouvait être pointée).

          Maintenant, si on voit une portion de code en Ada avec de l'arithmétique de pointeur, c'est un signe que c'est une portion à relire et à surveiller, car il existe des mécanismes permettant de s'en passer à bien des égards. Par contre, en C, l'arithmétique de pointeur est une chose "banale"…

          Donc, à mon avis, l'utilisation d'un langage comme Ada aurait très certainement pu permettre d'éviter ou de détecter le bug plus tôt.

        • [^] # Re: Les analyseurs ne sont pas non plus une panacee

          Posté par (page perso) . É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 . Évalué à 3.

        Il faut te sortir de cette ambiguïté.

  • # Coccinelle

    Posté par (page perso) . É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 . É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 . É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 . É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 . É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 (page perso) . É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 . Évalué à 6. Dernière modification le 18/04/14 à 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 (page perso) . Évalué à 2. Dernière modification le 18/04/14 à 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 . Évalué à 2.

            Sans compter les techniques d'interprétations abstraite qui peuvent prouver certains trucs aussi.

          • [^] # Re: Vérification formelle

            Posté par . Évalué à 1.

            Connais-tu des tutos pour appliquer ces méthodes à du code C ?

            • [^] # Re: Vérification formelle

              Posté par (page perso) . É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 . Évalué à 4.

                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,

                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 . É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 (page perso) . Évalué à 4. Dernière modification le 24/04/14 à 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 . É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 . É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 . Évalué à 5.

          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.

          Déjà rapporté (voir ma réponse à nono).

  • # 42^W Réponse bookmark

    Posté par (page perso) . É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 à ceux qui les ont postés. Nous n'en sommes pas responsables.