Extrapol, première partie : de C aux effets

June 9, 2008 § Leave a comment

Après un billet dans la langue de Turing, voici une présentation d’Extrapol en version française. En quelques mots, le projet Extrapol (pour Extraction de Politiques de Sécurité) vise à combler un vide dans le jeu d’outils dont dispose l’administrateur pour maintenir un système dans un état sûr.

Ainsi, il existe un grand nombre de logiciels qui permettent de surveiller un processus durant son exécution (analyse dynamique) ou après son exécution (analyse de traces) afin de comprendre le comportement de programme et ainsi de vérifier que la politique de sécurité en vigueur sur le système est bien respectée. À l’inverse, les outils d’analyse statique disponibles cherchent généralement à répondre à des questions sans rapport direct avec la sécurité système, telles que “ai-je écrit une bêtise ?” ou “puis-je prouver que mon programme fonctionne ?”

Que fait ce programme ?

Les outils d’analyse dynamique, qu’il s’agisse de SELinux, de la protection mémoire Unix, de la gestion des privilèges Windows ou des autorisations Java ou .Net, visent tous à répondre à deux questions :

  1. Qu’est en train de faire ce programme ?
  2. Est-ce légal ?

La réponse à la deuxième question est donnée par une notion de politique de sécurité, qui se réduit généralement à un ensemble d’autorisations de la forme “le sujet S a le droit d’entreprendre l’action A sur l’objet O”. Pour répondre à la première question, la technique générale consiste à intercaler entre le programme et les APIs concernées par la surveillance une couche dont le seul rôle est de prendre en compte les appels. Sans entrer dans les détails, les outils d’analyse de trace posent des questions similaires en s’appuyant sur des notions et des techniques comparables.

Logiquement, nous avons décidé de suivre le même chemin pour Extrapol :

  1. Que va faire ce programme ?
  2. Puis-je savoir dès maintenant si c’est légal ?

Pour répondre à la deuxième question, nous nous proposons d’utiliser exactement la même notion de politique de sécurité que celle qui est employée dans les systèmes d’exploitation actuels — plus précisément, à terme, nous nous proposons de permettre à Extrapol d’utiliser directement les fichiers de configurations de SELinux ou d’AppArmor. Quant à la première question, nous allons en chercher la réponse par des techniques d’analyse de types sur les programmes écrits en C. Voyons cela sur un exemple :

void* read_some_stuff()
{
   FILE* file = fopen("/home/foo/bar.log", "r");
   void* buf  = malloc(1024*sizeof(int));
   fread(buf , sizeof(int), 1024, file);
   return buf;
}

Que fait donc cette fonction ? Sans nous attacher à la qualité du code — une pléthore d’outils existe déjà pour essayer de vérifier celle-ci — nous pouvons déterminer aisément que

  • il s’agit d’une fonction appelée read_some_stuff
  • si cette fonction est appelée, elle ouvrira en lecture le fichier nommé /home/foo/bar.log
  • si cette fonction est appelée, elle consultera une partie du fichier nommé
    /home/foo/bar.log
  • si cette fonction est appelée, elle renverra une information tirée du fichier nommé
    /home/foo/bar.log

En termes de sécurité, ce programme ne doit donc être accepté que dans un contexte dans lequel la politique de sécurité en vigueur sur le système autorise la consultation du fichier /home/foo/bar.log. Regardons ce que nous dit Extrapol au sujet de ce programme :

read_some_stuff: Function
        effect                 : "open" (Constant "/home/foo/bar.log" , Constant "r" )
        effect                 : "read" (Constant "/home/foo/bar.log" )
        return                 : "data read from file" (Constant "/home/foo/bar.log" )
End

Soit, en français,

  • read_some_stuff est une fonction
  • cette fonction ne prend aucun argument
  • cette fonction a pour effet d’ouvrir le fichier nommé
    "/home/foo/bar.log" pour consultation
  • cette fonction a pour effet de consulter des informations depuis le fichier nommé "/home/foo/bar.log"
  • le résultat de cette fonction est un ensemble d’informations provenant du fichier nommé "/home/foo/bar.log".

Pour cet exemple, la réponse d’Extrapol est plus longue que le programme original et probablement pas beaucoup plus lisible. Regardons le résultat sur un extrait un peu plus complexe :

#include <stdio.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>

int do_open(char* file_name)
{
  int fd = (int)fopen(file_name, O_RDONLY);
  return fd;
}

int do_read(int fd)
{
  char* buf;
  buf    = (char*)malloc(1024*sizeof(char));
  int rd = 0;
  for(int i = 0; i < 1024; ++i)
    rd = rd + fread(buf, i, 1, fd);

  return buf;
}
&#91;/sourcecode&#93;

Sans surprise, Extrapol analysera les deux fonctions et présentera un bilan pour chacune.
<ul>
	<li>L'analyse de <code>do_open</code> produira : 
do_open: Function
        input arg file_name    : Bottom
        effect                 : "open" (Identifier "file_name", Constant "0" )
        return                 : "FILE" (Identifier "file_name" )
End

c’est-à-dire,

  • do_open est une fonction
  • do_open accepte un argument, ici file_name
  • le contenu de cet argument ne sera pas modifié
  • le contenu de cet argument n’a pas besoin d’avoir une structure particulière
  • appeler cette fonction aura un effet sur le système : ouvrir ouvrir pour consultation le fichier dont le nom a été donné dans file_name
  • la fonction renvoie une information abstraite, dans ce cas un fichier dont le nom a été donné dans file_name.
  • L’analyse de do_read produira :
    do_read: Function
            input arg fd           : "FILE" (Identifier "extrapol_generated_699 (formerly <anonymous> ) " )
            effect                 : "read" (Identifier "extrapol_generated_699 (formerly <anonymous> ) " )
            return                 : "data read from file" (Identifier "extrapol_generated_699 (formerly <anonymous> ) " )
    End

    c’est-à-dire,

    • do_read est une fonction
    • do_read accepte un argument, ici fd
    • le contenu de cet argument ne sera pas modifié
    • cet argument doit être une structure abstraite, dans ce cas précis un fichier
    • pour le reste de la fonction, nous appellerons le nom du fichier extrapol_generated_699 (formerly <anonymous>)" — Extrapol a été obligé d’inventer cette appellation pas très attrayante pour désigner le nom du fichier
    • cette fonction a un effet sur le système : consulter le fichier dont le nom est représenté par extrapol_generated_699 (formerly <anonymous> )
    • cette fonction renvoie une information abstraite, dans ce cas quelque chose qui a été lu depuis le fichier dont le nom est représenté par extrapol_generated_699 (formerly <anonymous> )
  • Maintenant, ces fonctions peuvent être utilisées et leur usage peut être analysé de la même manière que si elles avaient fait partie de la libc. Ainsi, complétons notre extrait par la fonction main suivante :

    int main(int argc, char **argv) {
      assert(argc >= 1);
      int   fd  = do_open(argv[0]);
      char* buf = do_read(fd);
      free(buf);
      return 0;
    }
    

    En retour, Extrapol nous répondra :

    main: Function
            input arg argc         : "command-line argument" ()
            input arg argv         : "command-line argument" ()
            input vararg           : "command-line argument" ()
            effect                 : "read" (Identifier "argv" )
            effect                 : "open" (Identifier "argv", Constant "0" )
            return                 : Constant "0"
    End

    En d’autres termes, le programme aura pour effet d’ouvrir puis de lire un fichier dont le nom est passé en ligne de commande.

    Comment ça marche ?

    Pour ce billet, je ferai semblant de comprendre cette question comme « comment utiliser Extrapol ? » La réponse est simple. Extrapol prend en entrée un ou plusieurs fichiers source C (passés ou non par le préprocesseur) et une base de connaissances sur les fonctions considérées comme primitives. Cette base de connaissance est un fichier ASCII dans le même format que les sorties d’Extrapol. Ainsi, malloc sera décrit par

    malloc: Function
      input arg size: Bottom
      return: Bottom
    End
    

    En d’autres termes, malloc est une fonction qui accepte un argument (“size“) quelconque et renvoie une valeur dont il est possible de faire n’importe quoi. Une fonction telle que fread sera un peu plus compliquée. Commençons par regarder le manuel de cette fonction :

    size_t fread(void *ptr, size_t size, size_t nmemb, FILE *stream);
    

    Pour Extrapol, il s’agit d’une fonction à 4 arguments et une valeur de retour. Commençons par la fin.

    • La valeur de retour peut être n’importe quoi, nous n’allons faire aucune garantie. En Extrapol, c’est ce que nous notons Top — par opposition à Bottom, qui signifierait au contraire qu’il n’y a aucune contrainte sur la valeur. Si nécessaire, nous pourrions raffiner ceci.
    • Le dernier argument est un fichier. Nous avons vu un peu plus tôt comment représenter les fichiers : ce sont des structures abstraites que nous avons décidé, par convention, d’appeler FILE, comme dans la bibliothèque standard de C. Plus précisément, nous avons décidé de les noter "FILE" (toto)toto permet de déterminer le nom du fichier. Nous appelons "FILE" un constructor, au sens de la réécriture ou de la programmation fonctionnelle. Il s’agit en tout et pour tout d’une chaîne de caractères dont nous nous servons pour différencier les valeurs abstraites. Le toto correspondant est l’argument donné au constructeur.
    • L’avant-dernier paramètre de la fonction est le nombre de blocs à lire. Nous allons juste l’ignorer, c’est-à-dire ne mettre aucune contrainte, c’est-à-dire Bottom.
    • Le deuxième argument est une taille, que nous allons aussi ignorer, c’est-à-dire de nouveau Bottom.
    • Enfin, le premier paramètre est utilisé en sortie — fonctionnellement, c’est une forme spéciale de return. Nous allons donc le marquer output. Nous pourrions nous arrêter là et ne mettre aucune garantie sur le contenu de ce paramètre, mais ici nous allons légèrement raffiner et spécifier qu’il s’agit d’informations certes inconnues, mais lues depuis un fichier. Comme précédemment, il s’agit d’une structure abstraite, donc d’un constructeur, que nous allons appeler "data read from file". Comme argument, nous allons passer le nom du fichier d’où viennent les informations. Nous obtenons donc "data read from file"(toto). La valeur de toto sera déterminée lors de l’invocation de la fonction grâce à la valeur du dernier argument.
    • Oh, et avant d’oublier, cette fonction a un effet sur le système : elle lit quelque chose depuis toto. Appelons cet effet "read"(toto)

    Ou, en Extrapol dans le texte :

    fread: Function
       output arg ptr: "data read from file" ( Identifier "path" )
       input arg size : Bottom
       input arg nmemb: Bottom
       input arg stream: "FILE" ( Identifier "path" )
       return: Top
       effect: "read" ( Identifier "path" )
    End
    

    Une fois données cette base de connaissances et des fichiers C, Extrapol va passer les fichiers au pré-processeur, analyser lexicalement et syntaxiquement le contenu des fichiers, puis procéder par déductions successives à partir de la structure du programme et de la base de connaissances. Chaque fonction analysée est ajoutée à la base de connaissances pour pouvoir être réutilisée dans la suite du programme. Extrapol continue soit jusqu’à avoir tout analysé, soit jusqu’à un problème interne (typiquement une fonction avec le mauvais nombre d’arguments ou une fonction utilisée sans avoir été définie).Enfin, Extrapol affiche le résultat de ses déductions, à un format ré-utilisable pour réinjection dans la base de connaissances.

    Si vous êtes curieux, les principes derrière Extrapol sont

    • le lambda-calcul et, plus généralement, la programmation fonctionnelle
    • les systèmes de types avec effets
    • les systèmes de types dépendants
    • l’inférence de types à la Hindley-Milner .

    Tout ceci sera détaillé dans un ou plusieurs autres billets — et dans un article de journal scientifique que je viens de commencer.

    Est-ce que ça marche ?

    La réponse à cette question est un clair et franc “oui, non et peut-être” :

    • Tout n’est pas implanté. En particulier, pour le moment, Extrapol n’est pas capable de déduire quoi que ce soit d’intéressant sur les variables globales. De même, Extrapol n’aboutira pour le moment que si les fonctions sont introduites dans l’ordre dans lequel elles sont utilisées. Rien de terriblement difficile à ajouter à Extrapol, cela n’a juste pas été prioritaire jusqu’à présent.
    • Extrapol n’est capable de gérer ni la récursivité ni les pointeurs sur fonctions. Pour le moment, la théorie derrière Extrapol ne prend pas en compte ces aspects du langage C.
    • Tous les exemples cités ci-dessus fonctionnent, ainsi que quelques dizaines d’autres.
    • Nous n’avons pas encore confronté Extrapol avec des logiciels complets. Le jour où Extrapol comprendra, mettons tar ou ls, nous déboucherons le champagne.

    Comment est-ce écrit ?

    Il y a actuellement deux versions d’Extrapol :

    • Extrapol/Java, version implantée en Java par Bastien Jansen, Steve-William Kissi et David Teller. Environ 18.000 lignes de code.
    • Extrapol/ML, version expérimentale, implantée en OCaml par David Teller. Environ 4.000 lignes de code.

    Les deux versions seront libérées sous peu (normalement d’ici la mi-juin), dès que nous serons arrivés à régler des problèmes techniques dans notre serveur de projet et dès que nous aurons fini par décider d’une licence. A priori, ce sera probablement Cecill B pour Extrapol/Java et LGPL pour Extrapol/ML.

    Tagged: , , , , , , , , , , , , , , , ,

    Leave a Reply

    Fill in your details below or click an icon to log in:

    WordPress.com Logo

    You are commenting using your WordPress.com account. Log Out / Change )

    Twitter picture

    You are commenting using your Twitter account. Log Out / Change )

    Facebook photo

    You are commenting using your Facebook account. Log Out / Change )

    Google+ photo

    You are commenting using your Google+ account. Log Out / Change )

    Connecting to %s

    What’s this?

    You are currently reading Extrapol, première partie : de C aux effets at Il y a du thé renversé au bord de la table.

    meta

    %d bloggers like this: