TP Frama-C

config/cert_exp_33.c

+#include <stddef.h>
+
 void set_flag(int number, int *sign_flag) {
   if (NULL == sign_flag) {
     return;
@@ -8,10 +10,12 @@ void set_flag(int number, int *sign_flag) {
   } else if (number < 0) {
     *sign_flag = -1;
   }
+  Frama_C_show_each_set_flag(number, *sign_flag);
 }
 
 int is_negative(int number) {
   int sign;
   set_flag(number, &sign);
+  Frama_C_show_each_is_negative(number, sign);
   return sign < 0;
 }

config/cert_exp_33_realloc.c

@@ -8,6 +8,7 @@ int *resize_array(int *array, size_t count) {
   }
 
   int *ret = (int *)realloc(array, count * sizeof(int));
+  //@ split ret==0;
   if (!ret) {
     free(array);
     return 0;

config/cwe20.c

@@ -24,10 +24,16 @@ int main () {
     if ( EOF == error ){
     die("No integer passed: Die evil hacker!\n");
     }
+    if (m <= 0 || n <= 0) {
+        die("Dimensions must be positive: Die evil hacker!\n");
+    }
     if ( m > MAX_DIM || n > MAX_DIM ) {
     die("Value too large: Die evil hacker!\n");
     }
     board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
+    if (board == NULL) {
+        return 2;
+    }
     for (int i = 0; i < m; i++) {
         for (int j = 0; j < n; j++) {
             board[n*i+j] = 0;

config/libstring.c

@@ -9,6 +9,7 @@
 #define unlikely(x)    __builtin_expect(!!(x), 0)
 
 #include "libstring.h"
+#include "__fc_builtin.h"
 
 #define BUF_LEN 65536
 #define CAP_DEFAULT 10
@@ -437,3 +438,39 @@ string_t *string_vector_reduce(reducefunc_t func,
 const char *libstring_version() {
   return LIBSTRING_VERSION;
 }
+
+
+int main(void) {
+  char cstr1[256];
+  char cstr2[256];
+
+  for (int i = 0; i < 255; i++) {
+    cstr1[i] = (char) Frama_C_interval(1, 127);
+    cstr2[i] = (char) Frama_C_interval(1, 127);
+  }
+  cstr1[255] = '\0';
+  cstr2[255] = '\0';
+
+  string_t *s1 = string_new(cstr1);
+  string_t *s2 = string_new(cstr2);
+  if (s1 == NULL || s2 == NULL) {
+    printf("Allocation error in string_new\n");
+    return 1;
+  }
+
+  string_t *s_concat = string_concat(s1, s2);
+  if (s_concat == NULL) {
+    printf("Concatenation error\n");
+    free(s1);
+    free(s2);
+    return 1;
+  }
+
+  string_println(s_concat);
+
+  free(s1);
+  free(s2);
+  free(s_concat);
+
+  return 0;
+}
\ No newline at end of file

rapport.md

+# Rapport
+
+## CERT C EXP33-C. Do not read uninitialized memory
+
+### Première exécution de Frama-C
+
+Lorsque je lance la commande `frama-c -eva -main is_negative cert_exp_33.c`, j'obtiens la réponse suivante :
+
+```
+[kernel] Parsing cert_exp_33.c (with preprocessing)
+[eva] Analyzing a complete application starting at is_negative
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] cert_exp_33.c:18: Warning:
+  accessing uninitialized left-value. assert \initialized(&sign);
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function set_flag:
+  sign ∈ {-1; 1} or UNINITIALIZED
+[eva:final-states] Values at end of function is_negative:
+  sign ∈ {-1; 1}
+  __retres ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 9 statements reached (out of 11): 81% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 access to uninitialized left-values
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+```
+
+L'analyseur identifie que la variable `sign` est potentiellement non-initialisée (`sign ∈ {-1; 1} or UNINITIALIZED`), ce qui génère une alarme (`1 alarm generated by the analysis: 1 access to uninitialized left-values`)
+
+Après avoir ajouté les lignes de la forme `Frama_C_show_each_*`, j'obtiens la réponse suivante :
+
+```
+[kernel] Parsing cert_exp_33.c (with preprocessing)
+[eva] Analyzing a complete application starting at is_negative
+[eva:initial-state] Values of globals at initialization
+
+[eva] cert_exp_33.c:13:
+  Frama_C_show_each_set_flag: [-2147483648..2147483647], {-1; 1}
+[eva] cert_exp_33.c:19:
+  Frama_C_show_each_is_negative: [-2147483648..2147483647], {-1; 1}
+[eva:alarm] cert_exp_33.c:20: Warning:
+  accessing uninitialized left-value. assert \initialized(&sign);
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function set_flag:
+  sign ∈ {-1; 1} or UNINITIALIZED
+[eva:final-states] Values at end of function is_negative:
+  sign ∈ {-1; 1}
+  __retres ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 11 statements reached (out of 13): 84% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 access to uninitialized left-values
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+```
+
+### Partitionner les traces
+
+J'ajoute l'option -eva-partition-traces.
+
+Pour n = 1, j'obtiens les résultats suivants :
+
+```
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [-2147483648..0], {-1}
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [1..2147483647], {1}
+[eva] cert_exp_33.c:19:
+  Frama_C_show_each_is_negative: [-2147483648..2147483647], {-1; 1}
+```
+
+Pour n = 2, j'obtiens les résultats suivants :
+
+```
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: {0}, ⊥
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [-2147483648..-1], {-1}
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [1..2147483647], {1}
+[eva] cert_exp_33.c:19:
+  Frama_C_show_each_is_negative: [-2147483648..2147483647], {-1; 1}
+```
+
+Pour n = 3, j'obtiens le même résultat que pour n = 2.
+
+### Partitionnement inter-procédural
+
+Quand j'ajoute l'option `-eva-interprocedural-history`, j'obtiens les résultats suivants :
+
+```
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: {0}, ⊥
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [-2147483648..-1], {-1}
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [1..2147483647], {1}
+[eva] cert_exp_33.c:19: Frama_C_show_each_is_negative: {0}, ⊥
+[eva] cert_exp_33.c:19: Frama_C_show_each_is_negative: [-2147483648..-1], {-1}
+[eva] cert_exp_33.c:19: Frama_C_show_each_is_negative: [1..2147483647], {1}
+[eva:alarm] cert_exp_33.c:20: Warning:
+  accessing uninitialized left-value. assert \initialized(&sign);
+```
+
+On voit apparaître une alarme qui n'était pas présente dans les résultats précédents. Cette alarme apparaît également dans l'interface graphique.
+
+## CERT C EXP33-C bis
+
+### Première analyse
+
+Je choisis de lancer la commande suivante :
+
+```
+frama-c -eva -eva-partition-history 3 -eva-interprocedural-history -main func cert_exp_33_realloc.c
+```
+
+Voici les résultats obtenus :
+
+```
+
+[kernel] Parsing cert_exp_33_realloc.c (with preprocessing)
+[eva] Analyzing a complete application starting at func
+[eva:initial-state] Values of globals at initialization
+
+[eva] cert_exp_33_realloc.c:21: allocating variable **malloc_func_l21
+[eva] cert_exp_33_realloc.c:27: starting to merge loop iterations
+[eva] cert_exp_33_realloc.c:10: allocating variable **realloc_resize_array_l10
+[eva:alarm] cert_exp_33_realloc.c:12: Warning:
+accessing left-value that contains escaping addresses.
+assert ¬\dangling(&array);
+[eva] using specification for function printf_va_1
+[eva:alarm] cert_exp_33_realloc.c:38: Warning:
+accessing uninitialized left-value. assert \initialized(array + i_0);
+[eva] cert_exp_33_realloc.c:37: starting to merge loop iterations
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function resize_array:
+array ∈ {{ &__malloc_func_l21[0] }} or ESCAPINGADDR
+ret ∈ {{ NULL ; &__realloc_resize_array_l10[0] }}
+array ∈ {{ &__malloc_func_l21[0] }} or ESCAPINGADDR
+**retres ∈ {{ NULL ; &**realloc_resize_array_l10[0] }}
+[eva:final-states] Values at end of function func:
+**fc_heap_status ∈ [--..--]
+array ∈ {{ NULL ; &**realloc_resize_array_l10[0] }}
+S**\_fc_stdout[0..1] ∈ [--..--]
+**malloc_func_l21[0] ∈ {0} or UNINITIALIZED
+[1] ∈ {1} or UNINITIALIZED
+[2] ∈ {2} or UNINITIALIZED
+[3..9] ∈ {3; 4; 5; 6; 7; 8; 9} or UNINITIALIZED
+[eva:summary] ====== ANALYSIS SUMMARY ======
+
+---
+
+2 functions analyzed (out of 2): 100% coverage.
+In these functions, 34 statements reached (out of 37): 91% coverage.
+
+---
+
+No errors or warnings raised during the analysis.
+
+---
+
+2 alarms generated by the analysis:
+1 access to uninitialized left-values
+1 escaping address
+
+---
+
+Evaluation of the logical properties reached by the analysis:
+Assertions 0 valid 0 unknown 0 invalid 0 total
+Preconditions 3 valid 0 unknown 0 invalid 3 total
+100% of the logical properties reached have been proven.
+
+---
+
+```
+
+On remarque que deux alarmes ont été générées par l'analyse : une alarme pour un accès à une valeur non-initialisée et une alarme pour un accès à une adresse qui s'échappe.
+
+Je choisis d'exécuter la commande suivante :
+
+```
+frama-c-gui -eva -eva-min-loop-unroll 10 -main func cert_exp_33_realloc.c
+```
+
+Je vois bien apparaître une nouvelle alarme rouge dans l'interface graphique.
+
+### Analyse précise de `realloc`
+
+J'ajoute la ligne `//@ split ret==0;` dans le code : l'alarme disparaît, comme attendu.
+
+## CWE 20
+
+### Première analyse
+
+Les alarmes portent sur deux types de problèmes :
+
+- Débordements entiers sur les expressions m*n et (m-1)*n qui pourraient dépasser la plage des entiers si les valeurs de m et n ne sont pas correctement bornées.
+- Accès mémoire invalides, dont un accès à une case non initialisée lors de la lecture de board[(m-1)*n].
+
+En pratique, si on impose que 0 < m, n ≤ MAX_DIM, ces alarmes sont de faux positifs et le programme se comporte correctement.
+
+### Patch 1
+
+J'ajoute le code suivant :
+
+```
+    if (m <= 0 || n <= 0) {
+        die("Dimensions must be positive: Die evil hacker!\n");
+    }
+```
+
+Les cinq erreurs liées aux débordements entiers disparaissent.
+
+### Patch 2
+
+J'ajoute le code suivant :
+
+```
+if (board == NULL) {
+        return 2;
+    }
+
+```
+
+Mais je ne parviens pas à éliminer les erreurs restantes.
+
+## libstring
+
+### concat
+
+J'ajoute la fonction main suivante à la fin de `libstring.c` :
+
+```
+int main(void) {
+  char cstr1[256];
+  char cstr2[256];
+
+  for (int i = 0; i < 255; i++) {
+    cstr1[i] = (char) Frama_C_interval(1, 127);
+    cstr2[i] = (char) Frama_C_interval(1, 127);
+  }
+  cstr1[255] = '\0';
+  cstr2[255] = '\0';
+
+  string_t *s1 = string_new(cstr1);
+  string_t *s2 = string_new(cstr2);
+  if (s1 == NULL || s2 == NULL) {
+    printf("Allocation error in string_new\n");
+    return 1;
+  }
+
+  string_t *s_concat = string_concat(s1, s2);
+  if (s_concat == NULL) {
+    printf("Concatenation error\n");
+    free(s1);
+    free(s2);
+    return 1;
+  }
+
+  string_println(s_concat);
+
+  free(s1);
+  free(s2);
+  free(s_concat);
+
+  return 0;
+}
+```
+
+J'obtiens pourtant les erreurs suivantes :
+
+```
+3 alarms generated by the analysis:
+       3 accesses to uninitialized left-values
+```