Re: qui utilise Frama-C ?
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.
Reply to: