La mémoire tampon est une zone de stockage temporaire dans la mémoire vive, qu'un programme réserve pour y placer les données du programme. Cependant, comme le tampon n'est qu'une zone de la mémoire, il est tout à fait possible de s'en échapper, notamment en remplissant entièrement la taille du tampon allouée.

Cet article a pour objectif de définir précisément le mécanisme de dépassement de tampon, d'en expliquer les failles de sécurité liées, et de présenter les contributions de Sagar Chaki et Scott Hissam dans leur article Certifying the Absence of Buffer Overflows publié en 2006, dans lequel ils proposent une méthode de vérification formelle qui permet de certifier l'absence de dépassement de tampon pour un programme.

1 Le dépassement de tampon

Le dépassement de tampon, ou buffer overflow en anglais, est une vulnérabilité permettant d'écrire en dehors de la zone mémoire allouée pour le programme. Cela peut entraîner l'écrasement des zones mémoires adjacentes, car en dehors du tampon, il y a le reste de la mémoire de la machine. Les informations y sont peu ordonnées, l'ordinateur se souvient qui est où grâce à des pointeurs. Ainsi, au-delà du tampon, il est possible d'écraser aussi bien des informations peu importantes que des informations nécessaires au fonctionnement de la machine. La vulnérabilité du dépassement de tampon tire parti de l'organisation de la mémoire lors de l'exécution d'un programme. Lorsqu'une fonction est appelée, le système empile sur la pile d'instructions le tampon de taille n, quelques variables, puis l'adresse de retour. Cette adresse de retour indique au processeur vers quelle instruction reprendre après l'exécution du programme donné. Un dépassement de tampon suffisamment large permet d'écraser cette adresse, ou bien de la contrôler. En effet, il est possible d'introduire des données, et de remplacer la vraie adresse de retour par une malveillante, pointant à un tout autre endroit de la mémoire. Il est par exemple possible d'ouvrir un terminal avec les privilèges nécessaires pour prendre le contrôle de la machine. Par exemple, en 2001, un ver nommé CodeRed s'est propagé dans le monde en exploitant le dépassement de tampon sur un serveur IIS de Microsoft. Grâce à une URL particulière, le ver était capable d'exécuter un code arbitraire sur la machine cible sans authentification nécessaire.

Pour réduire la surface d'attaque, il existe certaines protections. Ci-dessous sont décrites des protections utilisées permettant de restreindre les dépassements de tampons.

Stack canaries. Cette mesure repose sur l'insertion par le compilateur d'une valeur sentinelle, appelée le canari, entre les variables locales et l'adresse retour. Comme l'attaquant est contraint d'écraser tous les octets situés entre le tampon débordé et l'adresse retour, il ne peut éviter de modifier le canari. Avant l'exécution d'une fonction, une copie du canari est placée dans la mémoire. Cette valeur sera comparée à la valeur du canari après l'exécution de la fonction. En cas de divergence, le processus est interrompu. Plusieurs variantes de canari existent, par exemple, le canari aléatoire qui contient une valeur inconnue, le canari terminateur qui contient des caractères qui interrompent la plupart des fonctions de manipulation de chaine, par exemple un octet nul ou un retour à la ligne. Cependant, cette mesure peut quand même permettre un dépassement de tampon, dans le cas où l'attaquant arrive à lire la valeur du canari pour la reproduire à l'identique lors du dépassement.

Address Space Layout Randomization (ASLR). Cette technique a pour objectif de brouiller l'ordre de la mémoire afin d'empêcher l'attaquant de se retrouver de manière fiable dedans. Pour cela, certaines adresses du processus, la pile, le tas, etc. sont aléatoirement mélangées. Sans cette technique, les adresses sont fixes et prévisibles, ce qui permet à l'attaquant de construire son entrée en y inscrivant directement l'adresse vers laquelle rediriger l'exécution. L'attaquant peut essayer de deviner les adresses qui sont modifiées, mais plus le nombre de positions possibles est élevé, plus il est difficile de les prédire.

Bit NX. Cette méthode est une fonctionnalité matérielle du processeur qui permet de distinguer, dans l'adresse mémoire d'un programme, les zones qui sont destinées aux instructions exécutables, et celles destinées aux données. Il est alors possible de marquer certaines régions mémoires comme « non exécutables », ce qui interdit alors au processeur d'interpréter le contenu comme un programme. Ainsi, si l'attaquant injecte du code malveillant grâce au dépassement de tampon et redirige l'exécution vers cette zone, le processeur refusera d'exécuter cette zone, car le bit NX dit de considérer cette région comme une zone de donnée. Cependant, cette technique est limitée parce qu'elle ne protège pas contre les attaques qui ne reposent pas sur l'injection de code.

Cependant, bien que ces protections réduisent la surface d'attaque, principalement lorsqu'elles sont combinées, aucune ne garantit l'absence de vulnérabilité. C'est ce qui a motivé une approche formelle.

2 Certification formelle de l'absence de dépassement de tampon

L'article de Chaki et Hissam datant de 2006 constate que de nombreux systèmes critiques, tels que des systèmes embarqués, des noyaux de systèmes d'exploitation, des infrastructures réseau, etc., sont développés en C ou C++ pour des raisons de performances. Puisque bas-niveaux, aucune vérification des bornes à l'exécution ne sont réalisés. Ces systèmes sont souvent complexes car ils reposent sur des bibliothèques diverses, ainsi que sur des routines unsafe. Cet article s'interroge sur la possibilité de certifier automatiquement, à partir du code source, qu'une opération sur le tampon en C ne provoquera jamais de dépassement lors de l'exécution.

2.1 Techniques employées

La méthode proposée emploie le model checking et le problème de satisfiabilité (souvent abrégé en SAT).

Model checking. Technique de vérification automatique sur les systèmes finis. Le comportement du programme en question est modélisé sous forme d'un automate fini et l'algorithme de model checking explore l'ensemble des états accessibles afin de déterminer si une propriété donnée est satisfaite ou non. Si elle ne l'est pas, un contre-exemple est donné en sortie.

SAT. Problème qui cherche à déterminer s'il existe une combinaison de variables booléennes qui satisfait l'ensemble des contraintes d'une formule de logique propositionnelle. Ce problème est dit NP-complet, ce qui signifie qu'il n'existe pas , à ce jour, d'algorithme capable de le résoudre efficacement dans le cas général. Le temps de résolution croît de manière exponentielle avec la taille de la formule.

2.2 Description de la méthode

La méthode décrite dans le début du papier se décompose en trois phases successives, permettant de transformer le problème de sécurité en un problème de vérification formelle.

1. Instrumentation du programme. Le code source du programme P est instrumenté, afin d'ajouter pour chaque opération sur un tampon une assertion A. Cette dernière est construite de sorte qu'elle échoue si et seulement si l'opération considérée est susceptible de provoquer un dépassement.

2. Vérification par model checking. Le model checker analyse le programme instrumenté pour déterminer si l'assertion A peut parfois être fausse. En cas d'échec, un contre-exemple noté CE est produit. Il décrit la séquence d'exécution qui produit un dépassement. C'est grâce à ce contre-exemple qu'il est plus facile de localiser et de corriger la vulnérabilité. En l'absence d'échec, le model checker produit un invariant INV. Un invariant, c'est une propriété qui est vraie en tout point de l'exécution du programme. Ainsi, INV garantit que l'assertion A ne peut jamais être mise en défaut. Par exemple, un invariant dans ce cas pourrait prendre la forme de « la variable i est toujours comprise dans l'intervalle [0, 7] lors de tout accès au tampon de taille 8 ».

3. Certification.

À partir de l'invariant INV, une condition de vérification notée VC est construite. C'est une formule logique dont la validité garantit formellement la correction de l'invariant et exclut tout scénario d'échec de l'assertion A. La formule VC est alors soumise à un solveur SAT, et si elle est déclarée valide, le certificat Cert est émis. Il constitue une preuve formelle qui atteste l'absence de tout dépassements de tampon pour l'opération considérée.

2.3 Discussion

Ce travail permet d'assurer formellement l'absence de dépassement de tampon. Les auteurs valident leur approche sur un benchmark public de Zitser et al. qui compose une suite de cas de test dérivée de programmes contenant des vulnérabilités de dépassement de tampon connus. Chacun de ses tests a deux versions, l'une est vulnérable, l'autre est corrigée. Les résultats montrent que, pour les cas où un invariant est produit, l'outil détecte systématiquement le dépassement dans la version vulnérable et certifie l'absence de vulnérabilité dans la version corrigée correspondante. La contribution de cet article vise la qualité de la garantie fournie. Si la plupart des outils signalent efficacement les cas suspects, la méthode de Chaki et Hissam produit une preuve formelle de l'absence de vulnérabilité. Cependant cette méthode est limitée lorsqu'il faut passer à grande échelle. En effet, la complexité du model checking croît de manière exponentielle avec la taille de l'automate à visiter entièrement. De plus, certaines vulnérabilités peuvent provenir de bibliothèques tierces, qui ne sont pas couvertes par l'instrumentation.

3 Conclusion

Le dépassement de tampon reste l'une des sources de vulnérabilités les plus exploitées dans des logiciels. Cela s'explique par le vaste usage du langage C, dont les performances justifient l'utilisation dans des systèmes critiques, malgré l'absence de vérification des bornes natives. L'approche de Chaki et Hissam montre qu'il est possible d'utiliser la vérification formelle afin d'assurer la protection à l'exécution. Cette idée pourrait être associée à des contre-mesures existantes comme les canaris de pile, l'ASLR ou bien le bit NX, dans le but de combiner garanties formelles et protections à l'exécution.

Références

1. Chaki, S., & Hissam, S. (2006, September 1). Certifying the Absence of Buffer Overflows. (Technical Note CMU/SEI-2006-TN-030). https://doi.org/10.1184/R1/6572210.v1, https://insights.sei.cmu.edu/documents/2118/2006_004_001_14723.pdf.
2. Wikipedia. Dépassement de tampon. https://fr.wikipedia.org/wiki/D%C3%A9passement_de_tampon.
3. Wikipedia. Model checking. https://en.wikipedia.org/wiki/Model_checking.
4. Wikipedia. Problème SAT. https://fr.wikipedia.org/wiki/Probl%C3%A8me_SAT.
5. Cowan, Crispin & Wagle, F. & Pu, Calton & Beattie, S. & Walpole, J. (2000). Buffer overflows : Attacks and defenses for the vulnerability of the decade. DARPA Information Survivability Conference and Exposition. 2. 119-129 vol.2. 10.1109/DISCEX.2000.821514.
6. G. Lettieri. Stack Canaries. October 2023. https://cseweb.ucsd.edu/~efernandes/teaching/res/how-canaries-work.pdf
7. SANS Institute. Stack Canaries – Gingerly Sidestepping the Cage. February 2021. https://www.sans.org/blog/stack-canaries-gingerly-sidestepping-the-cage
8. CERT-FR. Bulletin d'alerte du CERT-FR, Propagation du ver « Code Red ». Août 2001. https://www.cert.ssi.gouv.fr/alerte/CERTA-2001-ALE-008/
9. Wikipedia. Address space layout randomization. https://en.wikipedia.org/wiki/Address_space_layout_randomization
10. Wikipedia. NX bit. https://en.wikipedia.org/wiki/NX_bit