Le comportement pour la variable now est étrange. Serait-il possible d'avoir un cas auto-contenu quelque part ? Par exemple sous forme d'un rapport de bug à http://bts.frama-c.com/bug_report_page.php , ou à n'importe quel autre endroit ; en incluant bien une ligne de commande, le log obtenu, et tous les fichiers nécessaires pour reproduire (“gcc -save-temps” permet d'obtenir des fichiers .i pré-processés, ou alternativement “frama-c -print fichier1.c fichier2.c …” permet d'obtenir un unique fichier C compilable représentant tout le projet)
Maintenant que l'analyse de valeur reconnait les post-conditions “ensures” (dans la limite de ses moyens), il est possible d'avoir facilement la fonction de génération de valeurs inconnues de n'importe quel type :
/*@ ensures mn <= \result <= mx ; */
long my_unknown_long(long mn, long mx);
Bonjour, ici l'auteur initial du plug-in “value analysis” de Frama-C.
Vérifier l'absence de comportements “non définis” est utile dans n'importe quel programme C. Les démons nasaux peuvent venir de partout, et un buffer overflow dans la moindre bibliothèque, la plus anodine soit-elle, peut avoir des répercussions en-dehors de son périmètre. Pour les spécialistes, le vers Stuxnet utilisait entre autres failles un défaut du code d'interprétation des fichiers liens du système visé pour prendre le contrôle dès que la clé USB piégée était insérée, sans qu'il soit nécessaire pour l'utilisateur de lancer un programme : http://www.f-secure.com/v-descs/trojan-dropper_w32_stuxnet.shtml
C'est particulièrement utile dans une bibliothèque de génération de nombres pseudo-aléatoires, parce qu'un comportement non défini ici pourrait avoir des conséquences directes sur la qualité de la cryptographie effectuée sur le système.
Un comportement non défini peut avoir comme conséquence que l'aléa du générateur, vérifié expérimentalement sur un OS A avec un compilateur B, est soudain de mauvaise qualité sur l'OS C ou avec le compilateur D.
Oui, c'est une vérification différente de la vérification mathématique du générateur. Cette dernière est aussi un objectif louable, mais la première reste utile indépendamment de l'existence ou non de la dernière.
Quelques remarques pratiques qui ne sont utiles que pour que celui qui voudrait effectuer ou reproduire cette analyse :
1/ Pour utiliser Frama_C_interval() il faut soit inclure le fichier …./share/builtin.c dans la liste des fichiers analysés, soit lui donner un prototype avec post-condition:
/*@ ensures mn <= \result <= mx ; */
int Frama_C_interval(int mn, int mx);
buf est un “variable-length array”. Ceux-ci ne sont pas bien gérés par l'analyse de valeurs, mais dans le cas présent je recommanderais de toutes façon d'utiliser une macro:
char buf[NBYTES];
et de lancer l'analyse en pré-processant avec "gcc -C -E -I. -DNBYTES=…" depuis un script qui pourra donner chacune des 1000 valeurs intéressantes. Au passage, c'est bien 1000 valeurs intéressantes, car le C standard interdit de déclarer un tableau de taille 0 (même si GCC l'accepte).
[^] # Re: courage!
Posté par pascal_cuoq . En réponse au journal Analyser la génération de nombre aléatoire du noyau. Évalué à 2.
Le comportement pour la variable now est étrange. Serait-il possible d'avoir un cas auto-contenu quelque part ? Par exemple sous forme d'un rapport de bug à http://bts.frama-c.com/bug_report_page.php , ou à n'importe quel autre endroit ; en incluant bien une ligne de commande, le log obtenu, et tous les fichiers nécessaires pour reproduire (“gcc -save-temps” permet d'obtenir des fichiers .i pré-processés, ou alternativement “frama-c -print fichier1.c fichier2.c …” permet d'obtenir un unique fichier C compilable représentant tout le projet)
Maintenant que l'analyse de valeur reconnait les post-conditions “ensures” (dans la limite de ses moyens), il est possible d'avoir facilement la fonction de génération de valeurs inconnues de n'importe quel type :
/*@ ensures mn <= \result <= mx ; */
long my_unknown_long(long mn, long mx);
# courage!
Posté par pascal_cuoq . En réponse au journal Analyser la génération de nombre aléatoire du noyau. Évalué à 10. Dernière modification le 27 mars 2013 à 10:53.
Bonjour, ici l'auteur initial du plug-in “value analysis” de Frama-C.
Vérifier l'absence de comportements “non définis” est utile dans n'importe quel programme C. Les démons nasaux peuvent venir de partout, et un buffer overflow dans la moindre bibliothèque, la plus anodine soit-elle, peut avoir des répercussions en-dehors de son périmètre. Pour les spécialistes, le vers Stuxnet utilisait entre autres failles un défaut du code d'interprétation des fichiers liens du système visé pour prendre le contrôle dès que la clé USB piégée était insérée, sans qu'il soit nécessaire pour l'utilisateur de lancer un programme : http://www.f-secure.com/v-descs/trojan-dropper_w32_stuxnet.shtml
C'est particulièrement utile dans une bibliothèque de génération de nombres pseudo-aléatoires, parce qu'un comportement non défini ici pourrait avoir des conséquences directes sur la qualité de la cryptographie effectuée sur le système.
Un comportement non défini peut avoir comme conséquence que l'aléa du générateur, vérifié expérimentalement sur un OS A avec un compilateur B, est soudain de mauvaise qualité sur l'OS C ou avec le compilateur D.
Oui, c'est une vérification différente de la vérification mathématique du générateur. Cette dernière est aussi un objectif louable, mais la première reste utile indépendamment de l'existence ou non de la dernière.
Quelques remarques pratiques qui ne sont utiles que pour que celui qui voudrait effectuer ou reproduire cette analyse :
1/ Pour utiliser Frama_C_interval() il faut soit inclure le fichier …./share/builtin.c dans la liste des fichiers analysés, soit lui donner un prototype avec post-condition:
/*@ ensures mn <= \result <= mx ; */
int Frama_C_interval(int mn, int mx);
2/ Dans la séquence suivante :
u_int nbytes = Frama_C_interval(0, 1000);
char buf[nbytes];
buf est un “variable-length array”. Ceux-ci ne sont pas bien gérés par l'analyse de valeurs, mais dans le cas présent je recommanderais de toutes façon d'utiliser une macro:
char buf[NBYTES];
et de lancer l'analyse en pré-processant avec "gcc -C -E -I. -DNBYTES=…" depuis un script qui pourra donner chacune des 1000 valeurs intéressantes. Au passage, c'est bien 1000 valeurs intéressantes, car le C standard interdit de déclarer un tableau de taille 0 (même si GCC l'accepte).