Skip to content
Snippets Groups Projects
Select Git revision
  • main default protected
1 result
Blame Permalink
rapport.md 9.10 KiB

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