1. Forum
  2. Usenet
  3. LINUX.DEBIAN.USER.FRENCH

  • 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 [email protected] <mailto:[email protected]>

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

    --
    Basile Starynkevitch <[email protected]>
    (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:[email protected]"><font face="monospace">[email protected]</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:[email protected]">&lt;[email protected]&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 [email protected]

    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)