• qui utilise Frama-C ?

    From Basile Starynkevitch@21:1/5 to All on Mon Sep 6 08:30:01 2021
    This is a multi-part message in MIME format.
    Bonjour la liste,


    Qui (parmi les lecteurs de la liste) utilise l'analyseur Frama-C <https://frama-c.com/> (voir https://frama-c.com/ <https://frama-c.com/>
    ...) et pourquoi?

    Merci de me répondre en privé vers basile@starynkevitch.net <mailto:basile@starynkevitch.net>

    PS. Significativement, aucun paquet Debian ne semble avoir été analysé
    par Frama-C. Votre opinion sur le pourquoi est appréciée.

    --
    Basile Starynkevitch <basile@starynkevitch.net>
    (only mine opinions / les opinions sont miennes uniquement)
    92340 Bourg-la-Reine, France
    web page: starynkevitch.net/Basile/


    <html>
    <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
    </head>
    <body>
    <p>Bonjour la liste,</p>
    <p><br>
    </p>
    <p>Qui (parmi les lecteurs de la liste) utilise l'analyseur <a
    moz-do-not-send="true" href="https://frama-c.com/">Frama-C</a>
    (voir <a moz-do-not-send="true" href="https://frama-c.com/">https://frama-c.com/</a>
    ...) et pourquoi?</p>
    <p>Merci de me répondre en privé vers <a moz-do-not-send="true"
    href="mailto:basile@starynkevitch.net"><font face="monospace">basile@starynkevitch.net</font></a></p>
    <p>PS. Significativement, aucun paquet Debian ne semble avoir été
    analysé par Frama-C. Votre opinion sur le pourquoi est appréciée.<br>
    </p>
    <pre class="moz-signature" cols="72">--
    Basile Starynkevitch <a class="moz-txt-link-rfc2396E" href="mailto:basile@starynkevitch.net">&lt;basile@starynkevitch.net&gt;</a>
    (only mine opinions / les opinions sont miennes uniquement)
    92340 Bourg-la-Reine, France
    web page: starynkevitch.net/Basile/

    </pre>
    </body>
    </html>

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Yves Rutschle@21:1/5 to Basile Starynkevitch on Tue Sep 7 12:10:02 2021
    On Mon, Sep 06, 2021 at 08:26:36AM +0200, Basile Starynkevitch wrote:
    Qui (parmi les lecteurs de la liste) utilise l'analyseur Frama-C <https://frama-c.com/> (voir https://frama-c.com/ <https://frama-c.com/>
    ...) et pourquoi?

    Moi, j'essaye, occasionellement. Deux contextes:
    - On a essayé de prouver des propriétés de sécurités dans un
    logiciel. Ça marche pour de trucs très simples, ou en y
    mettant beaucoup d'efforts.
    - Pour essayer d'etre sûr de n'avoir pas de vulnérabilités
    dans un serveur Internet que j'écris. Ça marche pas du
    tout, car le traitement des chaines de caractères se passe
    pas bien.

    Merci de me répondre en privé vers basile@starynkevitch.net

    Bah, pourquoi? :)

    PS. Significativement, aucun paquet Debian ne semble avoir été analysé par Frama-C. Votre opinion sur le pourquoi est appréciée.

    C'est trop lourd, trop compliqué, et encore trop restreint:
    la preuve formelle marche mal avec du code qui travaille sur
    des chaines de caractères, ou du code avec des pointeurs de
    fonctions, ou du code qui utilise beaucoup de librairies
    indépendantes (il faudrait des contrats ACSL pour les
    fonctions de la librairie...), etc.

    Hors domaine spécifique du logiciel critique embarqué, je
    n'ai entendu parler que de l'ANSSI qui a développé un
    validateur de certificats X.509 prouvés (Journey to a
    RTE-free X509 parser, SSTIC 2019).

    A+
    Y.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)