Représentation intermédiaire de l’assembleur asm

Télécharger le fichier pdf d’un mémoire de fin d’études

Rencontre avec l’assembleur embarqué

Les processeurs de nos matériels informatiques ne sont que des interpréteurs d’un jeu d’instructions dont les variantes les plus répandues aujourd’hui sont les familles x86 (ordinateur) et ARM (ordinateur, smartphone, objet connecté). Une procédure algorithmique se compose d’une série d’instructions encodée sous la forme d’une chaîne de bits dans la mémoire. Manipuler manuellement cette représentation binaire dans l’optique de programmer un processeur est une tâche particulièrement laborieuse. Les langages de programmation permettent de s’abstraire de cette tâche en délégant une partie de la complexité à des outils automatisés. Les algorithmes écrits dans ces langages peuvent être :
Interprétés. le processeur exécute un programme qui va lire le code source ou une de ses représentations dérivées et en exécuter l’algorithme ;
Compilés. le programme est encodé dans le jeu d’instructions du processeur qui exécutera directement le code produit.
Orthogonalement, l’algorithme peut être transformé à différents degrés pour en réduire sa complexité et ainsi réduire sa taille et/ou sa durée d’exécution.
Le langage C. Le langage C est généralement utilisé dans un contexte où les performances sont prioritaires. C’est un langage de bas niveau ayant pour vocation d’être transformé en assembleur (compilation) puis en code exécutable natif (as-semblage). Le cycle de compilation standard d’un programme C est illustré dans la őgure 2.1.
Les compilateurs de C sont réputés pour favoriser les optimisations. À titre d’exemple, Pereira et al. [PCR+17] ont mesuré des différences signiőcatives dans l’utilisation des ressources en temps et en espace pour différents langages. Un pro-gramme écrit en C était ainsi en moyenne 2 à 3 fois plus rapide que le même pro-gramme écrit en OCaml. Un facteur 70 a même été observé entre C et Python.
Les compilateurs restent toutefois limités et font de leur mieux (best effort) pour que le programme s’exécute le plus efficacement. Il existe donc des situations dans lesquelles un expert est capable de proposer une version du code directement écrite en assembleur plus efficace que celles provenant de la compilation d’un code C.
Nous allons illustrer cette situation avec un exemple inspiré d’une fonction de l’outil FFMPEG : mid_pred qui retourne la valeur centrale entre 3 entiers. Cette fonction est utilisée dans l’encodage de vidéo selon le standard H.263 où elle est appelée à répétition sur des ŕux de données. L’efficacité de cette fonction apparaît donc primordiale pour les performances générales de l’application et nous pensons que cela a justiőé qu’elle soit optimisée avec de l’assembleur embarqué x86.
Naïvement, cette fonction pourrait s’écrire très simplement en C comme suit 😐
int mid_pred (int a, int b, int c)
{ if ((a <= b) && (b <= c)) return b;
if ((b <= a) && (a <= c)) return a; return c; }
Cette première version présente l’inconvénient d’utiliser des sauts conditionnels. Les processeurs de la famille x86 sont conçus pour travailler de façon optimale en séquentiel (pipeline) et l’imprédictibilité des sauts conditionnels détériore la vitesse d’exécution.

Problèmes de compilation

L’assembleur embarqué est plus ŕexible et, en donnant plus de liberté au compi-lateur, potentiellement plus efficace que l’assembleur classique. Cette fonctionnalité est toutefois à réserver aux experts. Il est en effet très facile de se tromper en écrivant l’interface entre le langage C et l’assembleur. Le compilateur se reposant entièrement sur les déclarations de l’utilisateur, il n’offre ainsi aucun őlet de sécurité. La com-plexité de cette nouvelle syntaxe s’ajoute donc à la complexité déjà élevée d’écrire de l’assembleur. Plus préoccupant, un bloc assembleur incorrectement déclaré peut,
à l’instar des comportements indéőnis du C, fonctionner parfaitement pendant de longues années avant de provoquer un bug. Ces changements peuvent survenir sans qu’aucune modiőcation ne soit faite sur le bloc lui-même. Aussi, mettre à jour le compilateur ou changer une option de compilation peut devenir un élément déclen-cheur de bugs et il est alors très difficile d’en retracer l’origine.
Nous allons illustrer ces problèmes avec deux exemples issus de codes réels :
1. la librairie libatomic_ops qui fournit des accès aux primitives matérielles d’opé-rations atomiques. Elle a été utilisée dans le développement de programmes concurrents (multithreads). On lui préférera les types atomiques standards à partir de C11 ;
2. la librairie standard libc qui fournit la majorité des fonctionnalités nécessaires aux programmes écrits en C. En particulier, les primitives sur les chaînes de caractères sont optimisées à l’aide d’assembleur embarqué jusqu’à la version 2.19 (őn de vie en juin 2020).
Ces deux exemples historiques montrent des problèmes entre le code assembleur et son interface. Ces problèmes peuvent mener à des bugs et ont été corrigés dans les versions actuelles. Nous verrons en section 5.5 que ce ne sont malheureusement pas des exemples isolés, et qu’un ensemble conséquent (environ 10%) des blocs rencontrés dans le code de la distribution Debian souffrent d’erreurs similaires.

Oubli d’un effet de bord dans libatomic_ops

L’extrait de code de la őgure 2.3 est tiré du code source de libatomic_ops datant de őn 2005 (révision 178cc98). L’interface qui lie l’assembleur au C omet de déclarer un effet de bord sur un des registres d’entrée. Bénin à première vue, nous allons nous pencher sur un contexte d’utilisation où ce problème peut provoquer un blocage complet (deadlock ). Le bloc a été corrigé dans la révision 03e48c1 en 2010, soit 4 années après avoir été introduit.
124 AO_compare_and_swap_full(volatile AO_t *addr,
125 AO_t old, AO_t new_val)
127 char result;
128 __asm__ __volatile__(« lock; cmpxchgl %3, %0; setz %1 »
129 : « =m »(*addr), « =q »(result)
130 : « m »(*addr), « r » (new_val), « a »(old) : « memory »);
131 return (int) result; 132 }
En quoi consiste le code. La fonction AO_compare_and_swap_full implémente la primitive atomique standard d’ń échange si inchangé ż (Compare and Swap). Cette opération permet, dans un contexte concurrent, de mettre à jour une valeur uniquement si on a la main. Fonctionnellement, AO_compare_and_swap_full équi-vaut à : if (*addr == old) *addr = new_val;

Méthodes formelles et analyse de programmes

Présentation générale

Les méthodes formelles visent à raisonner, sur la base des mathématiques, sur des propriétés de programmes. On retrouve parmi les précurseurs des méthodes formelles Floyd [Flo67], Hoare [Hoa69], Dijkstra [Dij76], Cousot [CC77] ou encore Clark [CE81]. Les approches peuvent différer sensiblement mais toutes reposent sur trois éléments clés :
Ð la sémantique formelle M des comportements possibles du programme (géné-ralement une sémantique opérationnelle) ;
Ð la spéciőcation φ des comportements correctes (généralement une formule lo-gique) ;
Ð une (semi-)procédure de décision pour vériőer que les comportements possibles du programme sont corrects, noté M ⊧ φ.
Au vu de la complexité des programmes réels, le problème auquel s’attaquent les méthodes formelles est généralement indécidable. En d’autres termes, il n’est pas possible d’écrire un algorithme capable de répondre avec certitude à la question ń le comportement du programme est-il toujours correct ? ż pour tout programme.
Les années 2000 marquent, pourtant, le début de formidables avancées dans le domaine avec l’arrivée de techniques s’appliquant avec succès sur du code réel [HJMS03, VPK04, BCLR04, GKS05, CCF+05, KT14, KKP+15]. Les outils déve-loppés font ń de leur mieux ż pour répondre aux questions posées en se servant de sur-approximations ou de sous-approximations.
Sur-approximation. Les sur-approximations sont utilisées lorsque l’on souhaite prouver avec certitude l’absence de comportements indésirables dans un programme.
L’idée est de représenter les comportements du programme sous une forme plus simple à calculer que la forme réelle. L’approximation doit garantir que la forme simpliőée inclut tous les comportements réels du programme. Dans l’exemple de la őgure 3.1, le cercle S’ est bien une sur-approximation de la patatoïde S.
Puisqu’il n’y a pas d’intersection avec la zone délimitée par la propriété P1, il est possible de conclure que S’, et par conséquent S, vériőent P1. En revanche, il y a une intersection entre la zone délimitée par la propriété P2 et S’. Dans ce cas, il n’est pas possible de conclure quoi que ce soit sur S. Il s’agit alors d’un faux positif, c’est à dire qu’une violation est détectée sur l’approximation alors que le système réel vériőe la propriété.
La vériőcation automatique de programme telle que l’interprétation abstraite [CCF+05] utilise les sur-approximations pour prouver plus facilement les propriétés étudiées. En pratique, la vériőcation déductive assistée telle que le calcul de plus faible précondition (Weakest precondition calculus) [CdSSPT14] fait aussi usage de sur-approximation et demande des hypothèses conservatrices sur les contrats et invariants de boucle (Calcul de plus faible précondition, page 30).
Sous-approximation. À l’inverse, les sous-approximations sont utilisées pour montrer avec certitude la présence de comportements indésirables dans un pro-gramme.
L’approximation doit ici garantir que la forme simpliőée est entièrement incluse dans les comportements réels du programme. Dans l’exemple de la őgure 3.2, le losange S’ est bien une sous-approximation de la patatoïde S.
Sachant qu’il y a une intersection avec la zone délimitée par la propriété P2, il est possible de conclure que S’, et par conséquent S, violent P2. En revanche, l’absence d’intersection entre la zone délimitée par P1 et S’ ne signiőe pas que S respecte P1. Il s’agit dans ce cas d’un faux négatif, c’est à dire qu’une violation n’est pas détectée par l’abstraction alors que le système réel ne respecte pas la propriété.
On retrouve les techniques de sous-approximation dans les analyses de détection de bugs et de vulnérabilités telles que l’exécution symbolique [CDE08, BGM13] ou la vériőcation de modèle bornée (bounded model checking) [CKOS04].
Lien avec cette thèse. Nous cherchons dans cette thèse à étendre les techniques de vériőcation formelle de programmes C au cas de code mixte contenant de l’assem-bleur embarqué qui n’est actuellement pas géré par les méthodes usuelles se plaçant au niveau du C-ANSI. Nous proposons notamment une traduction de l’assembleur embarqué vers le C, validée et optimisée pour faciliter la vériőcation par les outils de vériőcation niveau C existants. Nous montrerons l’efficacité de notre approche de traduction (section 6.5) sur trois des techniques les plus employées :
Interprétation abstraite L’interprétation abstraite est une théorie d’approxima-tion de la sémantique des programmes introduite par Cousot et Cousot [CC77]. Elle sacriőe une part plus ou moins importante de précision pour gagner en calculabilité. La sémantique abstraite peut jouer sur deux niveaux pour ap-procher la sémantique concrète :
Ð la représentation des données en omettant des informations non essen-tielles ś par exemple, ne garder que l’information sur l’initialisation des variables, sans tenir compte de la valeur ;
Ð la réduction du nombre d’états en agrégeant plusieurs états ensemble ś par exemple, ne garder qu’un seul état abstrait par point de programme.
L’abstraction choisie dépendra de la propriété que l’on cherche à démontrer. Dans la pratique, l’interprétation abstraite est un processus itératif sur le graphe de ŕot de contrôle qui évalue la valeur des variables dans un domaine abstrait particulier pouvant représenter des ensembles de valeurs (énuméra-tion, intervalles, congruentes, etc.) ou des relations (égalités de valeurs, équa-tions linéaires, etc.). Chaque domaine abstrait déőnit un treillis de valeur (ensemble d’éléments partiellement ordonnés qui admet une borne supérieure et inférieure) et la sémantique des différents opérateurs sur ce treillis.
Calcul de plus faible précondition La vériőcation déductive permet de vériőer un contrat sur une portion de code, typiquement une fonction (par exemple, que la fonction sort renvoie un tableau trié). Le contrat se compose d’une précondition et d’une postcondition, l’objectif étant de montrer que la précon-dition est suffisante pour garantir la postcondition. Pour ce faire, le calcul de plus faible précondition raisonne en arrière pour déterminer quelle est la pré-condition nécessaire pour que l’exécution du code garantisse la postcondition, puis vériőe que la précondition du contrat implique la précondition minimale inférée. L’analyse génère des obligations de preuve en logique du 1er ordre, pouvant être résolues à l’aide de solveurs de contraintes SMT [LQ08], ou en logique du 2nd ordre, nécessitant un assistant de preuve [NPW02, PM12]. Il est généralement nécessaire d’annoter manuellement les cycles du graphe de ŕot de contrôle par un résumé logique. Ces annotations appelées invariants de boucle sur-approximent usuellement le comportement du corps de la boucle.
Exécution symbolique L’exécution symbolique permet d’obtenir la relation entre les données d’entrée (arguments de fonction, entrées utilisateur, etc.) et un che-min emprunté par le programme. L’analyse permet de calculer un prédicat de chemin (sous la forme d’une formule logique sans quantiőcateur) qui doit être satisfait aőn que ce chemin soit emprunté. L’exécution symbolique est notam-ment utilisée pour la génération efficace de tests de couverture de programmes [CS13]. Les analyseurs utilisent les solveurs de contraintes SMT pour vériőer la satisfaisabilité du prédicat de chemin et générer un jeu d’entrées concrètes permettant d’exécuter ce chemin. L’exécution symbolique repose fondamenta-lement sur l’énumération des chemins d’exécution du programme. En pratique, cette méthode ne sera donc pas toujours à même de compléter un parcours exhaustif de tous ces chemins d’exécution, notamment en présence de boucles non bornées.

Influence du langage de programmation

Les principes généraux des différentes analyses présentées en section 3.1.1 s’ap-pliquent quel que soit le langage étudié. En pratique toutefois, les techniques sont dépendantes des structures du langage et on préférera analyser un code au niveau source plutôt qu’au niveau binaire. En effet, les propriétés que l’on souhaite vériőer sont souvent plus simples à exprimer dans un langage de haut niveau, et paral-lèlement, ces langages offrent souvent plus de garanties. Nous présentons ici deux différences qui impactent sensiblement le processus de vériőcation.
Gestion de la mémoire et typage. Les vériőcations sur la gestion mémoire ne sont pas abordées de la même façon en Java, en C ou en assembleur. Dans le premier cas, il s’agira de vériőer que le pointeur n’est pas nul alors qu’il faudra s’assurer de la bonne allocation, initialisation et déallocation des blocs mémoire en C. En Java, la taille des objets est connue à l’exécution, évitant par exemple de faire un débordement de tableau (le programme lève une exception). En C, les informations de types peuvent aider à vériőer statiquement l’absence de débordement mémoire. Par ailleurs, des pointeurs de types incompatibles ne peuvent pas s’aliaser en Java et il en est de même en C lorsque la règle d’aliasing strict (strict aliasing) est appliquée. En assembleur et en binaire, il n’existe pas nativement de notion de types ni de séparation de mémoires. Aussi, une imprécision dans l’adresse d’une écriture ou d’une lecture en mémoire peut impacter des éléments complètement indépendants (par exemple, les variables locales dans la pile). Pour pallier ce problème, il existe des techniques pour tenter de retrouver ou de créer des types à partir des opérations réalisées dans le code [LAB11, RKS16].
Reconstruction du graphe de flot de contrôle. Le graphe de ŕot de contrôle d’un langage source est en règle générale facilement approximé par sa structure : fonctions, boucles, etc. Le code binaire présente en revanche un déő de taille pour les analyseurs [BR10, BHV11, MM16]. En effet, la macro-structure du code est perdue lors de la compilation. En absence d’éléments structurants, la découverte du graphe de ŕot de contrôle devient particulièrement difficile en présence de ń sauts dynamiques ż (branchements dont la cible de saut dépend de valeurs calculées à l’exécution). Les analyseurs de code binaire souffrent ainsi d’un problème d’amorce : les analyses ont besoin d’une bonne approximation du graphe de ŕot de contrôle qui a lui-même besoin des résultats des analyses pour être reconstruit, la perte de précision d’un côté impactant négativement la précision de l’autre. Ainsi, dans le cadre de l’interprétation abstraite, la sur-approximation d’une cible de saut peut entraîner l’interprétation d’une partie du programme normalement inatteignable qui pourra elle-même dégrader la précision de l’analyse de valeurs. Le problème est d’autant plus important pour le jeu d’instructions x86 dont l’encodage est très dense (n’importe quelle suite d’octets ressemble à une instruction valide) et les contraintes d’alignement sont faibles (n’importe quelle adresse est une cible de saut valide).
Les analyseurs de niveau source sont plus matures et rencontrent moins de diffi-cultés à être utilisés. Cependant, le code source n’est pas toujours disponible (code propriétaire, code hérité, etc.) et les compilateurs ne sont pas forcément őables. Ces raisons [BR10] ont motivé la communauté scientiőque à étudier la vériőcation de code binaire, avec le développement de plusieurs plateformes d’analyse de code [BJAS11, DB15, SWS+16].

Analyse de flot de données

Nous utilisons l’analyse de ŕot de données à plusieurs reprises pour la vériőcation de la conformité à l’interface (section 5.2.1) ainsi que dans les passes d’optimisation de la traduction (section 6.3.4). Cette section sert à introduire les notions principales utiles à ces analyses.
L’analyse de ŕot de données joue un rôle important dans le domaine de l’analyse statique. Elle est largement utilisée dans les compilateurs [Kil73] à des őns d’optimi-sation. Elle consiste à calculer des faits (dataflow fact) sur le programme en chacun des nœuds de son graphe de ŕot de contrôle. Le ŕot de données peut être vue comme un système d’équations qui relie les nœuds du graphe de ŕot de contrôle et dont la forme générale est :
Outn = Transfern(Inn)
Inn = Join(Outn′ )
n′∈ incomings(n)
La fonction Transfern déőnit la transformation qu’opère le noeud n sur le fait Inn donné en entrée, ce dernier étant calculé comme l’agglomération Join de tous les faits Outn′ des noeuds n’ arrivants sur n.
Les équations sont résolues de manière itérative jusqu’à ce que le calcul converge. L’état stable du système est appelé point fixe. Dans la pratique, la convergence vers le point őxe est garantie grâce à deux hypothèses :
Ð le domaine de valeurs des faits est assimilable à un treillis de hauteur őnie ;
Ð les fonctions Transfer et Join sont monotones sur ce treillis.
Ainsi, la sortie ne pouvant que croître ou rester la même et, la croissance étant limitée par la hauteur du treillis, le système se stabilise nécessairement dans un état pour lequel la sortie est la même d’une itération à l’autre.
L’analyse est dite ń en avant ż (forward ) lorsque les équations d’un nœud dé-pendent uniquement de celles de ses prédécesseurs. À l’inverse, elle est dite ń en arrière ż (backward ) lorsque les équations d’un nœud dépendent de celles de ses successeurs.
L’algorithme de résolution de l’analyse de ŕot de données à l’aide d’une liste de travail (worklist) est illustré dans le pseudo-code 1. L’algorithme est paramétré par le type abstrait des faits calculés (data) et par les deux opérations Transfer et Join. Le sens de l’analyse (backward ou forward ) est conőguré par les fonctions FirstNode et NextEdges qui peuvent prendre respectivement les valeurs entryNode et forwardEdges ou exitNode et backwardEdges. La fonction Init donne l’approxi-mation initiale des valeurs de chaque nœud du graphe de ŕot de contrôle.

Table des matières

Abstract
Résumé
Remerciements
1 Introduction 
2 Exemples et motivations 
2.1 Rencontre avec l’assembleur embarqué
2.2 Problèmes de compilation
2.2.1 Oubli d’un effet de bord dans libatomic_ops
2.2.2 Mauvaise allocation de registres dans la libc
2.3 Difficultés avec les analyseurs de niveau C
2.3.1 Utilisation de KLEE
2.3.2 Utilisation de Frama-C
2.4 Ce que propose cette thèse
3 Contexte et connaissances essentielles 
3.1 Méthodes formelles et analyse de programmes
3.1.1 Présentation générale
3.1.2 Inŕuence du langage de programmation
3.1.3 Analyse de ŕot de données
3.2 Assembleur embarqué dans du C
3.2.1 Syntaxe de Microsoft
3.2.2 Syntaxe de GNU
3.2.3 Caractéristiques de l’assembleur étudié
4 Sémantique de l’assembleur embarqué 
4.1 Présentation générale
4.2 Représentation et sémantique de l’assembleur
4.2.1 Représentation intermédiaire de l’assembleur asm
4.2.2 Sémantique opérationnelle de l’assembleur asm
4.3 Spéciőcités de l’assembleur embarqué
4.3.1 Formalisation des patrons C et des jetons t
4.3.2 Modélisation de l’interface formelle I
4.3.3 De la syntaxe concrète GNU à notre formalisme
4.3.4 Sémantique opérationnelle de l’assembleur embarqué asm⬩
4.4 TInA : obtenir la représentation intermédiaire
4.4.1 Architecture générale
4.4.2 Identiőcation de jetons
4.4.3 Analyseur de contraintes
4.4.4 Évaluation expérimentale
4.5 Discussion
4.5.1 Représentativité du corpus d’exemple
4.5.2 Limitations
4.6 Comparaison à l’état de l’art
4.7 Conclusion
5 RUSTInA : conformité à l’interface 63
5.1 Déőnition formelle
5.1.1 Équivalence observationnelle
5.1.2 Respect du cadre (framing condition)
5.1.3 Condition d’unicité
5.2 Méthode de vériőcation
5.2.1 Respect du cadre
5.2.2 Condition d’unicité
5.3 Correction automatique des erreurs de conformité
5.3.1 Correctifs pour le respect du cadre
5.3.2 Correctifs pour la condition d’unicité
5.4 Raffinement automatique de l’interface
5.5 Evaluation expérimentale de RUSTInA
5.5.1 Détection de problèmes de conformité (RQ1, RQ2, RQ3) . . 78
5.5.2 Génération de correctifs (RQ4)
5.5.3 Raffinement d’interface (RQ6)
5.5.4 Impact sur la communauté des développeurs (RQ7)
5.6 Étude qualitative des problèmes de conformité
5.6.1 Motifs récurrents d’interfaces mal formées (RQ8)
5.6.2 ń Protections ż historiques implicites de ces motifs (RQ9) . . 86
5.6.3 Robustesse des ń protections implicites ż (RQ10)
5.7 Discussion
5.7.1 Validité des expérimentations
5.7.2 Limitations
5.7.3 Syntaxe Microsoft
5.8 Comparaison à l’état de l’art
5.9 Conclusion
6 TInA : portage vers le C 95
6.1 Architecture générale de l’approche
6.2 Première traduction
6.3 Simpliőcations au service de la vériőcation
6.3.1 Propagation de types
6.3.2 Reconstruction de prédicats de haut niveau
6.3.3 Séparation de variables groupées (unpacking)
6.3.4 Propagation d’expressions symboliques
6.3.5 Normalisation de compteurs de boucle
6.4 Validation automatique
Table des matières vii
6.4.1 Isomorphisme de graphe de ŕot de contrôle
6.4.2 Équivalence de blocs de base
6.5 Evaluation expérimentale de TInA
6.5.1 Traduction et validation (RQ11, RQ12)
6.5.2 Adéquation aux outils de vériőcation formelle (RQ13, RQ14) 111
6.6 Discussion
6.6.1 Validité des résultats
6.6.2 Limitations
6.7 Comparaison à l’état de l’art
6.8 Conclusion
7 Conclusion et perspectives
7.1 Bilan
7.2 Perspectives
Annexes 127
A Exemple et motivation – codes complets 129
A.1 Main KLEE
A.2 Main EVA
A.3 Annotations de WP
B Règles de réécriture syntaxiques 135
Bibliographie

Télécharger le rapport complet