Vérifier l'intégrité d'un compilateur

Introduction: le problème de la poule et l’œuf de l'intégrité du compilateur.

Dans un papier devenu classique, Ken Thompson, pour  sa leçon du Prix Turing en 1984 (!) a indiqué une difficulté fondamentale dans la vérification du code d'un compilateur.  Effectivement, il y a un problème de la poule et l’œuf avec un compilateur.  Même si on a écrit un compilateur en code source, pour en faire un programme exécutable, il faut bien utiliser un (autre) compilateur.  Thompson, dans sa leçon, démontre que même si le code source d'un compilateur est parfaitement "propre", un compilateur corrompu qui compile ce code, fabriquera un compilateur corrompu du même genre.  La corruption peut être un cheval de Troie qui propagera dans tout code le cheval de Troie avait comme cible dont, bien sûr, toutes les variantes du compilateur même.  Thompson indique que aucune analyse du code source de tout un système ne peut indiquer cette corruption car dans le code source il n'y en a rien. Il indique à quel point une telle attaque est difficile (il veut peut-être dire "impossible") à déceler, sauf en étudiant le code exécutable même.  Mais les compilateurs sont actuellement des systèmes très complexes dont l'étude intégrale du code binaire n'est pas envisageable.  Un cheval de Troie bien caché pourrait ne jamais être découvert, et implanter des portes dérobées un peu partout.

Contrer l'attaque: la compilation double diverse.

Une stratégie pour tester un compilateur corrompu a été mise au point par  David A. Wheeler dans son papier de thèse.  L'idée est la suivante: un "bon" exécutable fait exactement ce que décrit le code source (et la définition du language source), indépendant par quel moyen cet exécutable binaire a été fabriqué.  Un compilateur est un logiciel particulier qui prend comme entrée: du code source, et qui produit comme sortie: un exécutable construit comme le code source du compilateur le décrit.  La relation entre le code source d'entrée et l'exécutable binaire est donc parfaitement décrit par le code source du compilateur. 

Nous avons la relation:

(code source A) -> [ compilateur binaire X] -> (exécutable XA)

et cette relation est parfaitement décrite par le code source de X qui dit ce que le code binaire X est sensé de faire.

Si nous avons un autre compilateur (Y), bien sûr le même code source donnera un autre binaire:

(code source A) -> [compilateur binaire Y] -> (exécutable YA)

Il n'y a aucune raison de supposer que les binaires XA et YA se ressemblent.  Les codes sources X et Y décrivent des façons différentes de fabriquer des exécutables, mais dans la mesure où X et Y sont tous les deux des compilateurs du même language L, les exécutables XA et YA doivent se comporter de façon identique.

Deux compilateurs A et B peuvent générer du code binaire différent pour le code source suivant:

#include <stdio.h>
 
int main()
{
  printf("Hello world\n");
  return 0;
}

Mais les deux exécutables doivent tous les deux imprimer "Hello world", si les deux compilateurs sont des implémentations correctes du langage C.  Il ne faut pas qu'il y ait un exécutable qui ajoute un retour de ligne et l'autre, non, dans la sortie: le code source et la définition du langage C fixent jusqu'au dernier caractère la sortie du programme.  Maintenant, un compilateur est un logiciel comme un autre: il prend une entrée (ici, en forme de texte, du texte qui représente du code source) et il produit une sortie (ici, un fichier binaire qui est aussi par hasard un exécutable). 

Nous avons deux compilateurs, X et Y.

(code source de X) -> [exécutable binaire du compilateur X] -> (fichier binaire exécutable XX) qui est donc un compilateur X.

(code source de X) -> [exécutable binaire du compilateur Y] -> (fichier binaire exécutable YX) qui est donc aussi un compilateur X.

Les fichiers binaires YX et XX sont des fichiers binaires différents car fabriqués avec des compilateurs différents (à savoir X et Y), mais ce sont deux exécutables qui mettent en oeuvre le code source X.  Ainsi, si nous compilons un code source A avec YX et avec XX, nous devrions obtenir les mêmes sorties binaires, car les deux compilateurs XX et YX doivent traiter l'entrée A selon le code source X, pour produire une sortie bien spécifique, de la même façon que les deux binaires de notre exemple avaient la même sortie "Hello world".

(code source A) -> [compilateur XX] -> (exécutable XXA)

(code source A) -> [compilateur YX] -> (exécutable YXA)

Les deux exécutables binaires XXA et YXA doivent être identiques, pas seulement dans leur opération, mais le code binaire même doit être, octet par octet, le même entre XXA et YXA.

Si nous remplaçons maintenant le code source arbitraire A par le code source X du compilateur X, nous obtenons:

(code source X) -> [compilateur XX] -> (exécutable XXX)

(code source X) -> [compilateur YX] -> (exécutable YXX)

 doivent être identique.

Comment ce test peut-il déceler un cheval de Troie dans le compilateur binaire X ou Y du départ ?  Il faut se rendre compte que l'hypothèse était que le compilateur binaire contenant le cheval de Troie allait fabriquer un compilateur binaire à partir d'un code source qui contient lui-même ce même cheval de Troie (sinon, le problème du compilateur corrompu qui se propage n'est pas présent).  Imaginons maintenant que nous avions un binaire corrompu H qui prétend être une version de X.  L'hypothèse de la propagation est:

(code source de X) -> [compilateur binaire H] -> (compilateur exécutable H)

Imaginons maintenant que notre compilateur Y n'était pas corrompu.

(code source de X) -> [compilateur Y binaire] -> (compilateur YX) comme avant.

mais par contre, nous avons:

(code source de X) -> [compilateur H] -> (H qui prétend être XX)

(code source de X) -> [exécutable que nous pensons être XX mais qui est H] -> (H qui prétend être XXX)

D'un autre coté:

(code source X) -> [compilateur binaire YX correct] -> (binaire YXX)

H prétendent être XXX ne peut pas en même temps contenir un cheval de Troie et être identique, octet par octet, à YXX.  Si nous constatons que YXX et XXX sont différents, nous savons qu'il y ait un cheval de Troie quelque part (ici, dans le binaire H).  Cela vient en fait à dire que H n'implémente pas de façon identique le langage du compilateur comme Y.  C'est la contribution essentielle de Wheeler.

Mais comment nous savons que le compilateur binaire de Y est correct ?  Si nous le savions, nous n'avions pas besoin du binaire de X.  Le point que fait comprendre Wheeler, est que le test indique un problème, même si Y contient aussi un cheval de Troie, du moment où ce n'est pas exactement le même.  Imaginons effectivement que le compilateur binaire Y du départ est aussi corrompu.  Nous l'appelons G.

Nous avons alors:

(code source de Y) -> [compilateur binaire corrompu G] -> exécutable G.

Mais, si les constructions de X et Y sont radicalement différentes, alors:

(code source X) -> [compilateur binaire corrompu G] peut:

  1. G peut ne pas reconnaître X comme compilateur, et donc ne pas insérer un cheval de Troie "compilateur" dans le résultat, alors le résultat sera YX
  2. Même si G reconnaît X comme compilateur, il sera très difficile d'insérer dans le code binaire de X un cheval de Troie qui fonctionnera bien, puisque X fonctionne de façon totalement différente que Y pour lequel le cheval de Troie était conçu.

Il faudrait effectivement que le concepteur du cheval de Troie dans G prévoit comment le compilateur qu'il ne connaît pas, X, fonctionnera, pour pouvoir le modifier de telle façon qu'il produira du code équivalent en fonction à G, mais totalement différent en structure.

Ainsi, on peut espérer que:

(code source X) -> [compilateur corrompu G] -> G' X  avec G' égal à Y, ou erroné.

Laisser agir G'X sur le code source de X:

(code source X) -> [compilateur (fonctionnel ou non) G' X] -> G"X

Il est très improbable que cela soit identique à H.

Ainsi, même avec deux compilateurs différents corrompus, il est difficile de s'imaginer que le test passe.  Pour cela, il faudrait vraiment que le concepteur de G ait prévu le compilateur X et son cheval de Troie H.

Démonstration avec le compilateur Tiny-C.

Nous pouvons utiliser la machine virtuelle du serveur ubuntu 13.10 que nous avons utilisé pour illustrer la vulnérabilité Shell Shock, ou nous pouvons installer un autre serveur.  J'ai fait le test sur beaucoup de systèmes différents et le premier système ubuntu sur lequel tout fonctionne est Dapper Drake (de 2006).  On peut télécharger Dapper Drake  ici.  Il est préférable d'installer la version serveur (beaucoup plus légère).  Il est judicieux de prendre un vieux compilateur.  Il est peu probable qu'un compilateur de 2006 contienne déjà un cheval de Troie qui sait comment s'insérer dans un autre compilateur qui est écrit en 2009...

Il faut installer Dapper Drake de la même façon que dans le tutoriel de Shell Shock jusqu'à la modification du fichier /etc/apt/sources.list (le changement des anciens dépositoires).

Il peut être nécessaire de modifier les configurations de stockage dans Virtual Box de SATA en IDE (il faut enlever les drives SATA, ajouter un nouveau drive IDE), si pendant l'installation, on n'arrive pas a partitionner le disque virtuel.

Cette fois, nous n'avons pas besoin d'un serveur web.  Par contre, nous avons besoin d'installer le compilateur gcc et texinfo.  Il faut exécuter les commandes suivantes:

sudo apt-get install gcc
sudo apt-get install build-essential
sudo apt-get install texinfo
sudo apt-get install wget

Si la connection internet marche, et les noms des dépôts sont modifiés, alors ces instructions devraient fonctionner.

Nous allons créer un dossier tcc.d pour faire le travail.  Dans ce dossier, nous allons importer le code source du compilateur tcc avec la commande suivante:

wget http://download.savannah.gnu.org/releases/tinycc/tcc-0.9.26.tar.bz2

Il faut dépaqueter cet ensemble:

bzip2 -kd tcc-0.9.26.tar.bz2
tar xvf tcc-0.9.26.tar

Dans le dossier on compile tcc avec les instructions suivantes:

./configure
make

Ceci compile le code source du compilateur tcc avec l'exécutable de gcc.  Sur mon installation 32 bits de Dapper, l'exécutable de tcc ainsi obtenue, a une longueur de  385632 octets.

Nous pouvons tester la fonctionalité du nouveau compilateur binaire tcc:

make test

et finalement, nous allons installer le compilateur tcc dans le système:

make install

Ceci met l'exécutable et la librairie libtcc1.a dans le système (et aussi la documentation de tcc).

Nous pouvons nettoyer le dossier:

make clean

ce qui efface tous les fichiers générés afin de pouvoir recommencer avec une feuille blanche (sauf que tcc est maintenant installé dans le système).

On va re-fabriquer tcc, mais cette fois, nous n'allons pas utiliser le compilateur gcc, mais le tcc que nous venons de fabriquer:

./configure --cc=tcc
make

Cette fois, nous fabriquons tcc, mais avec le compilateur tcc dans le système.  Il en résulte, pour moi, un exécutable de 489020 octets.

make test

vérifie que nous avons bien un compilateur exécutable fonctionnel.

Si maintenant, nous installons cette version de tcc dans le système:

sudo make install

nous avons remplacé le tcc fabriqué avec gcc par le tcc fabriqué par tcc.

Nous entamons un autre cycle:

make clean
./configure --cc=tcc
make

et... PAR TOUS LES DIABLES DE L'ENFER !  L'exécutable n'a que 486564 bytes !

Le test de Wheeler vient de rater !

Nous sommes effectivement en train de comparer YXX avec YXXX (tcc compilé avec tcc compilé avec gcc avec  tcc compilé avec tcc compilé avec tcc compilé avec gcc) et donc YXX avec XXX.  Le compilateur gcc est donc corrompu depuis 2006 !...

Pas si vite.

Il y a eu un problème avec la façon dont tcc fonctionne comme chargeur.  Effectivement, nous appelons tcc et gcc des compilateurs, mais c'est aussi des chargeurs.  Comme chargeur, tcc injecte en partie une copie du code binaire dans la librairie libtcc1.a dans l'exécutable qu'il est en train de construire.  Mais ce code binaire, dans le cas YXX, était encore construit avec gcc - tout le reste l'était avec tcc, car généré de nouveau, mais libtcc1.a était du code installé dans le système "le tour avant".  Le code avec les 489020 octets consiste donc essentiellement de code fabriqué avec tcc, mais une petite partie (celle copie directement de libtcc1.a) encore fabriquée avec gcc.  Il ne faut donc pas être surpris de la différence.  L'hypothèse de Wheeler était que tout le nouveau code était produit par tcc.

On refait le test, mais on adapte la librairie.

On re-fabrique le code avec gcc:

make clean
./configure
make
sudo make install

Nous avons installé tcc fabriqué avec gcc dans le système (y compris la librairie).

Maintenant, nous re-compilons tcc avec cette version de tcc:

make clean
./configure --cc=tcc
make

Notre exécutable a donc 489020 octets, comme avant, et contient une partie de code venant de gcc (via la librairie).

Mais maintenant nous allons seulement copier la librarie libtcc1.a (de 29670 octets) dans le système, et nous allons laisser en place tcc qui est fabriqué avec gcc:

sudo cp libtcc1.a /usr/local/lib/tcc

Nous allons re-compiler le code source de tcc, avec le compilateur tcc fait avec gcc, mais avec une librairie qui est du code fait avec tcc:

make clean
./configure --cc=tcc
make

Cette fois, nous remarquons que tcc a une longueur de 486564 octets, et la nouvelle version de la librairie libtcc1.a garde ces 29670 octets.

Gardons une copie de cet exécutable (qui est donc YXX):

cp tcc tccB

et installons cette version de tcc dans le système:

sudo make install

Quand nous repassons dans un cycle

make clean
./configure --cc=tcc
make

nous avons fabriqué la version XXX.  Quand on compare, octet par octet, avec le test suivant:

diff tcc tccB

nous constatons, cette fois, que XXX et YXX sont bien identiques.

Le compilateur binaire, fabriqué avec tcc fait avec gcc (YXX) est identique au compilateur binaire, fabriqué avec tcc qui est fait avec tcc (XXX).

Conclusion

Que pouvons-nous conclure ?

Le compilateur "de démarrage" binaire que nous avons utilisé est celui de gcc.  Nous n'avons pas importé un compilateur binaire "indépendant" tcc, nous l'avons fabriqué avec gcc.  Notre test n'est donc que partiel.  Nous n'avons pas compilé gcc avec tcc (en principe une bonne idée, mais gcc est un compilateur très complexe qui dépend de beaucoup d'outils).  Nous n'avons pas appliqué le test de Wheeler sur gcc, mais seulement sur notre propre version de tcc.  Il y a donc 3 possibilités:

  1. gcc contient un cheval de Troie qui sait parfaitement comment installer un cheval de Troie opérationnel et auto-copiant dans le fonctionnement d'un autre compilateur (ici, tcc), de telle façon que le binaire de tcc corrompu va générer exactement le même cheval de Troie quand il compile son propre code source.
  2. gcc contient un cheval de Troie mais il ne se rendait pas compte que tcc était un compilateur, et le cheval de Troie dans gcc ne s'est pas activé (en d'autres termes, le gcc supposé corrompu a fonctionné comme un bon compilateur dans ce cas-ci)
  3. gcc ne contient pas de cheval de Troie.

La première option semble improbable étant donné que nous utilisons un gcc de 2006, et que le code de tcc est de 2009.  Il est vrai que la 2ième option est possible.  Ainsi, nous ne pouvons pas dire grand-chose sur gcc.  Par contre, nous pouvons conclure que le code binaire de tcc est propre.  Nous avons donc un compilateur propre: tcc.  Pour conclure cela de gcc, il faudrait compiler gcc avec tcc.

Ceci n'était qu'un exercice de sensibilisation au problème potentiel du compilateur corrompu.  L'attaque "compilateur contenant cheval de Troie" est extrèmement puissante parce que c'est une attaque qui peut marcher dans le long terme, en plaçant des portes dérobés dans beaucoup d'applications d'origine fiable, s'ils sont fabriqués (à l'insu des développeurs) avec un compilateur corrompu.

Nous avons vu que pour pouvoir tester la fiabilité d'un compilateur, il faut avoir le code source de celui-ci.   Il ne suffit pas que le code source soit propre (c'est justement la difficulté).  Mais comme le seul test connu est le test de Wheeler, et pour cela il faut recompiler le code source avec un autre compilateur, il faut bien avoir accès au code source en premier lieu ! 

L'open source n'est pas une garantie de sécurité, mais absence d'open source est une garantie de vulnérabilité potentielle non-vérifiable.