Journal Analyser la génération de nombre aléatoire du noyau

Posté par  . Licence CC By‑SA.
Étiquettes :
29
26
mar.
2013

Sommaire

Après avoir lu hier un journal décrivant une faille dans le code de génération des nombres aléatoires de NetBSD 6, j'ai décidé de regarder quelques méthodes visant à réduire le risque d'introduire ce genre de bug dans du code "critique".

Disclaimer : je suis novice dans le domaine de la sécurité et de la preuve, et je n'ai jamais suivi de cours sur le sujet, il est fort possible que ce journal soit truffé d'erreurs de méthodes ou d'analyse majeures.

But

Analyse d'un code en C

Il y a trois choses qu'on peut vouloir garantir :

  1. l'algorithme de génération de nombres pseudo aléatoires est correct, c'est à dire que connaissant une suite de nombre générée, on ne peut pas déduire facilement le nombre suivant.
  2. l'implémentation de l'algorithme s'exécute de manière déterministe, sans comportement non spécifié par le standard C, et sans erreurs à l'exécution
  3. l'implémentation de l'algorithme est conforme à l'algorithme

Le génétateur de nombres pseudo aléatoires de DragonFly

Je me suis intéressé au code utilisé par DragonFlyBSD, qui se trouve dans le fichier sys/kern/kern_nrandom.c. DragonFly utilise deux algorithmes :

  • IBAA pour /dev/random
  • L15 pour /dev/urandom, qui est une évolution de l'algorithme ARC4, qui semble être utilisé par openBSD.

La sécurité de ces deux algorithmes est basée sur l'hypothèse qu'un attaquant ne connait pas l'état interne du générateur (qui est donc conservé dans le noyau). Ces deux algorithmes n'ont pas de preuve formelle de sécurité. Il est donc impossible de prouver le premier point. De plus, il est évident que toute méthode garantissant les deux points suivant n'est valide que si l'on considère que le noyau n'a pas de faille et qu'un processus utilisateur ne peux pas accéder à l'état interne du générateur, ce qui est sans doute illusoire.

Méthode

Tests unitaires

Je me suis dans un premier temps uniquement intéressé au 2ème points. La méthode traditionnelle pour éviter ce genre d'erreur est connue de tous, et elle est souvent présentée (à juste titre) comme une bonne pratique de développement. C'est l'écriture de tests, unitaires ou non. Toutefois, les tests ne sont pas exhaustifs, loin de là. Ils ne permettent de tester qu'un sous-ensemble limité de situations : il est impossible d'appeler un test unitaire pour les 232 valeurs d'un entier ! De ce fait, les tests unitaires ne permettent pas de garantir l'absence de certaines erreurs mais seulement d'en réduire la probabilité.

Analyse statique avec Frama-c

Il faut donc se tourner vers l'analyse statique de code. Il existe plusieurs outils disponible pour analyse du code en C. Certains se contentent de chercher des extraits de codes qui pourraient être problèmatiques, comme le font les compilateurs ou des outils comme coccinelle. Je me suis intéressé à un framework d'analyse statique de code en C, frama-c.

Frama-c est un outil opensource en ocaml principalement développé par le CEA qui opére directement sur une représentation du code C équivalente au code original. Il fournit plusieurs plugins permettant d'analyser certaines propiétés du code. J'ai commencé par utiliser le plugin val, qui permet de faire une analyse de valeur pour chaque expression d'un graphe d'appel.

On spécifie un point d'entrée, pour lequel un état initial pour toutes les variables globales est calculé. Puis, chaque expression et statements sont évalués, et les valeurs calculées sont propagées. Ce plugin permet de prouver que des variables sont toujours dans un intervalle donné, ou prennent un ensemble de valeurs connu, du moment que les assertions utilisées sont vérifiées.

Contexte d'analyse

Il faut commencer par extraire le code en question du noyau. Dans un premier temps, il faut construire un contexte d'analyse, dans lequel les génétateurs sont initialisées. C'est la fonction rand_initialize qui s'en charge :

void
rand_initialize(void)
{
  struct timespec now;
  int i;

  spin_init(&rand_spin);

  /* Initialize IBAA. */
  IBAA_Init();

  /* Initialize L15. */
  nanouptime(&now);
  L15((const LByteType *)&now.tv_nsec, sizeof(now.tv_nsec));
  for (i = 0; i < (SIZE / 2); ++i) {
    nanotime(&now);
    IBAA_Seed(now.tv_nsec);
    L15_Vector((const LByteType *)&now.tv_nsec,
         sizeof(now.tv_nsec));
    nanouptime(&now);
    IBAA_Seed(now.tv_nsec);
    L15_Vector((const LByteType *)&now.tv_nsec,
         sizeof(now.tv_nsec));
  }

  /*
   * Warm up the generator to get rid of weak initial states.
   */
  for (i = 0; i < 10; ++i)
    IBAA_Call();
}

On va d'abord modifier un peu cette fonction, en supprimant notament les verrous. De plus, cette fonction utilise l'horloge du système pour initialiser le seed des générateurs. Il nous faut tenir compte de toutes les valeurs que pourraient prendre cette horloge : manifestement, le nombre de nano seconde est compris entre 0 et 109. En utilisant les primitives de frama-c, on obtient :

void
rand_initialize_framac(void)
{
  long now;
  int i;

  /* Initialize IBAA. */
  IBAA_Init();

  /* Initialize L15. */
  now = Frama_C_interval(0, 999999999);
  L15((const LByteType *)&now, sizeof(now));
  for (i = 0; i < (SIZE / 2); ++i) {
    now = Frama_C_interval(0, 999999999);
    IBAA_Seed(now);
    L15_Vector((const LByteType *)&now,
         sizeof(now));
    now = Frama_C_interval(0, 999999999);
    IBAA_Seed(now);
    L15_Vector((const LByteType *)&now,
         sizeof(now));
  }

  /*
   * Warm up the generator to get rid of weak initial states.
   */
  for (i = 0; i < 10; ++i)
    IBAA_Call();
}

On peut alors appeler l'analyse. Frama-c calcule des intervalles de valeurs pour chaque valeur gauche à la sortie de chaque fonction, mais ce n'est pas réellement ce qui nous intéresse. Ce qu'il faut vérifier, c'est l'absence de warnings. Cette absence garranti que les comportements indéfinis vérifiés par frama-c n'auront jamais lieu durant l'exécution de ce code.

Ensuite, on peut vouloir appeler les fonctions de hashage, il suffit de construire une fonction main comme par exemple :

 int main() {


  u_int i;
  u_int nbytes = Frama_C_interval(0, 1000);
  char buf[nbytes];


  rand_initialize_framac();

  for (i = 0; i < nbytes; ++i)
    ((u_char *)buf)[i] = IBAA_Byte();
}

qui va tester la génération d'une séquence de nombres aléatoire entre 0 et 1000 bytes pour le générateur IBAA.

Résultats

L'analyse produit 3 warnings, qui sont a première vue des faux positifs. Il faut maintenant soit essayer d'augmenter la précision de l'analyse, notament en déroulant les boucles, soit prouver que ces cas n'arriveront pas par d'autres moyens.

L'analyse que j'ai réalisée est pour l'instant assez brouillon, et il reste plusieurs problèmes à régler, notament je ne suis pas certain que la fonction FramaC_interval fonctionne correctement dans l'utilisation que j'en fais. Toutefois, il est tout à fait faisable d'extraire certaines parties du code sensible d'un OS pour l'analyser plus en détail avec des outils comme frama-c, en réutilisant le système de build pour gérer les dépendances. Une analyse basique des fonctions présentées prend ~5minutes sur le petit processeur de mon netbook. Même si en l'état cette analyse n'est pas très utile, elle m'a permis de comprendre comment utiliser différentes parties de frama-c, comme le plugin WP, qui permet de faire de la preuve par contrat, et dont je parlerai peut être une autre fois.

  • # Oui ?

    Posté par  . Évalué à 9.

    Question bonus: En quoi ça prouve quoi que ce soit sur la qualité effective d'une source aléatoire ?

    Tu nous parles de comportement indéfini. Mais tu peux très bien avoir un comportement défini et totalement pourri. Si tu remplaces le code réel par le code de rand(3), il passe ton test ou pas ? ;)

    • [^] # Re: Oui ?

      Posté par  . Évalué à 4.

      Bah oui. Comme je l'explique dans le journal, ça ne prouve absolument pas le points 1, mais de toute manière, le points 1 n'est pas prouvable pour ce genre d'algos.

      Il y a des algorithmes qui ont une preuve de qualité, comme par exemple Blum Blum Shub, mais ils sont beaucoup trop lents pour être utilisés dans le cadre de /dev/urandom. Pour évaluer la qualité, il faut se rabattre sur des suites de tests, comme diehard.

      • [^] # Re: Oui ?

        Posté par  . Évalué à 4. Dernière modification le 28 mars 2013 à 08:44.

        Il y a surtout le trou entre l'algorithme est correct et l'implémentation est déterministe. Le trou étant: l'implémentation fait ce que l'algo dit. Tu peux avoir un défaut d'implémentation totallement détermiste, ca va même être générallement le cas en dehors du C.

        Si tu as un peu de temps tu pourrais faire la même chose sur le code troué de NetBSD ? À vue d'oeil en regardant le patch il est pas impossible qu'un analyseur statique ne lève pas grand chose.

  • # Pas bien saisie

    Posté par  . Évalué à 5. Dernière modification le 26 mars 2013 à 23:35.

    l'implémentation de l'algorithme s'exécute de manière déterministe, sans comportement non spécifié par le standard C, et sans erreurs à l'exécution

    Je ne comprends pas bien de quoi tu parle. Tu veux vérifier qu'il n'y a pas de undefine behaviour (tel que décris dans la norme) dans le code ?

    Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

    • [^] # Re: Pas bien saisie

      Posté par  . Évalué à 2.

      D'autant plus qu'il me semblait que certaines implementations s'executant sur plusieurs processeurs se basent justement sur
      du non-determinisme. [pas de lien]

  • # Validation de l'alea

    Posté par  . Évalué à 6.

    Tu parles en effet de preuve de code et non pas preuve de l'alea.
    Le fait de ne pas connaître la graine initiale dans le noyau n'est pas le seul problème. "La sécurité de ces deux algorithmes est basée sur l'hypothèse qu'un attaquant ne connait pas l'état interne du générateur (qui est donc conservé dans le noyau)." Oui, mais l'attaquant peut connaitre une longue suite de valeurs générées.

    Le second problème concerne la distribution de l'alea (et là, je ressors des vieux souvenirs de cours). On sait qu'une distribution aléatoire doit avoir des propriétés. On sait que l'on a:
    La moyenne des valeurs aléatoires générées doit correspondre au milieu de la plage. Si on tire un très grand nombre de valeurs aléatoires entre 0 et 1000, la moyenne doit être autour de 500.
    Problème: la suite suivante répond au critère mais n'est pas aléatoire: 499,501,499,501,499,501,…
    Une autre hypothèse indique que chaque valeur doit avoir une équiprobabilité de sortie. Cela permet de dégager la suite du dessus, mais la suite: 1,2,3,4,5,6,7,…,1000 est parfaitement équiprobable sur 1000 tirages, mais n'est pas aléatoire.
    On peut encore vérifier les écarts entre deux tirages successifs. Etc…

    Au final, on se rend compte qu'on a plusieurs moyens simples d'écarter des mauvaise suites aléatoires ce qui permet de créer des tests de conformités, mais qu'on a pas de moyen sûr de prouver la bonne qualité de l'aléatoire. A l'époque mon prof ne jurait que par les sources hardwares de "bruit" et démontait systématiquement les sources purement logicielles.

    • [^] # Re: Validation de l'alea

      Posté par  . Évalué à 5.

      Pour compléter ce que tu dis, la suite générée devrait aussi satisfaire un théorème central limite (convergence en distribution vers une gaussienne).

      Et d'ailleurs pour répondre au fait que la connaissance d'une suite donnée ne permet pas de deviner le nombre suivant, autrement dit que ce dernier est indépendant du passé, il existe aussi des tests statistiques pour cela.

      Mais je pense que la véritable question est, l'algorithme étant connu, si on observe une longue suite de nombre, est-on capable de déduire la graine (et donc le futur). Et ça, c'est lié à l'entropie du système dynamique sous-jacent. En allant vite, le système dynamique (ie l'algorithme) doit avoir une entropie (un désordre) au moins aussi grand que le shift de Bernoulli associé à la suite qu'on veut modéliser.

      Pareil que l'auteur du journal, certaines grossièretés peuvent s'être glissées dans ce commentaire.

      • [^] # Re: Validation de l'alea

        Posté par  . Évalué à 3.

        Un générateur peuso aléatoire doit avoir une distribution constante (=1/n, n étant la taille de la plage) puisque chaque nombre a la même probabilité de sortir.
        Une distribution gaussienne cela correspond plus à ce que tu obtient en mesurant la taille des individus d'une population en centimètre.

        • [^] # Re: Validation de l'alea

          Posté par  . Évalué à 2.

          La convergence en distribution que j'évoque n'est pas celle de la suite elle-même (celle-ci reste en effet constante) mais plutôt celle d'une fonctionnelle de cette suite. C'est bien à prendre au sens théorème central limite. J'ai voulu ajouter une explication au dernier moment, mais elle s'est avérée ambiguë.

  • # allez à toire

    Posté par  . Évalué à 6.

    http://dilbert.com/strips/comic/2001-10-25/

  • # courage!

    Posté par  . É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).

    • [^] # Re: courage!

      Posté par  . Évalué à 3.

      Bonjour, merci pour les remarques !

      Le soucis avec Frama_C_interval ici c'est que now est un long. Je lance l'analyse avec -machdep x86_64 sur une plateforme ou int est 32bits, donc 109 devrait rentrer dans un int, mais pour un cas plus général, j'ai l'impression qu'il n'y a pas d'équivalent pour les long.

      Quand je dis que la fonction ne semble pas fonctionner correctement, c'est parce qu'à la fin de l'analyse, frama-c affiche que "now ∈ {0}" ce qui semble trés trés louche. J'ai ajouté "now = 4" à divers endroits de la fonction rand_initialize_framac, et à chaque fois l'analyse affiche "now ∈ {4}", ce qui montre bien que now n'est pas réinitialisé à 0 par les fonctions appelées. Je suis quasiment certain que en l'état, l'analyse est incorrecte.

      [value] Values at end of function rand_initialize_framac:
          now ∈ {0}
          i ∈ {10}
          IBAA_memory[0..255] ∈ [--..--]
          IBAA_results[0..255] ∈ [--..--]
          IBAA_aa ∈ [--..--]
          IBAA_bb ∈ [--..--]
          IBAA_counter ∈ [--..--]
          IBAA_byte_index ∈ [--..--]
          memIndex ∈ [-2147483648..--],0%2
          L15_x ∈ [--..--]
          L15_y ∈ [--..--]
          L15_start_x ∈ {0}
          L15_state[0..255] ∈ [--..--]

      • [^] # Re: courage!

        Posté par  . É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);

  • # Bibliothèque Hasard

    Posté par  (site web personnel) . Évalué à 10.

    Salut, j'ai codé une bibliothèque de génération de nombres aléatoires : https://bitbucket.org/haypo/hasard

    Le projet vient avec des outils permettant de stocker la sortie d'un générateur dans un fichier, puis d'analyser les données. Il y a des outils pour générer une image ( c'est rigolo avec des générateurs tout pourri genre celui de PHP sous Windows, http://boallen.com/random-numbers.html ), test de la distribution avec les outils ENT et DieHarder, calcul d'entropie, calcul de la période, etc.

    Hasard vient avec une suite de tests unitaires. Il choisit comme un grand le meilleur générateur et la meilleure source d'entropie (pour initialiser le générateur) selon le profil demandé (vitesse ou sécurité). Hasard réutilise les générateurs existants (API Windows, /dev/urandom, OpenSSL, gcrypt, etc.)

    J'avais remarqué qu'OpenSSL n'injecte pas d'entropie (RAND_add) lors d'un fork. Du coup, deux processus fils ayant le même pid vont générer les même nombres. Ça peut arriver avec un serveur web qui traite plein de requêtes, et on m'a dit sur la liste de discussion OpenSSL que bah ouais, c'est à moi de me taper le boulot d'ajouter de l'entropie. Hasard détecte un fork et réinjecte lui-même de l'entropie.

    Voir le dossier doc/ pour diverses notes sur les générateurs de nombres aléatoires et python/ pour les outils.

    Vieux articles que j'avais écrit.

    http://www.haypocalc.com/blog/index.php/2007/12/02/97-generateurs-nombres-pseudo-aleatoires
    http://www.haypocalc.com/blog/index.php/2007/12/02/96-bugs-generateurs-de-nombres-pseudo-aleatoires
    http://www.haypocalc.com/blog/index.php/2008/08/18/159-attaquer-un-gnrateur-de-nombres-pseudo-alatoires
    http://www.haypocalc.com/blog/index.php/2008/06/09/149-developpement-bibliotheque-hasard

    Voili voulou, bonne lecture.

    PS : Il faudrait que je pense à faire une release d'ailleurs…

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.