fix many typo
This commit is contained in:
parent
16790cb4b4
commit
689a5bba4f
69
src/main.tex
69
src/main.tex
@ -36,10 +36,10 @@
|
||||
Né en 2017~\cite{HRSTHGWZB17}, devenu une norme du W3C en 2019, WebAssembly (Wasm)
|
||||
est un format d'instructions binaires (bytecode), incluant une représentation
|
||||
textuelle (Wat), à destination d'une machine virtuelle orientée pile.
|
||||
Afin de palier à certains comportements intrinsèques de JavaScript
|
||||
(un temps de parsing non prédictible et des problématiques de sécurité au niveau de la gestion de la mémoire)
|
||||
Afin de pallier certains comportements intrinsèques de JavaScript
|
||||
(perormances non prédictibles, problématiques de sécurité)
|
||||
WebAssembly a été conçu pour collaborer avec celui-ci dans un navigateur
|
||||
au sein d'un environnement d'exécution sécurisé (bac à sable). Dans un second temps,
|
||||
au sein d'un environnement d'exécution sécurisé. Dans un second temps,
|
||||
Wasm pourrait s'exécuter sans cette collaboration, actuellement nécessaire,
|
||||
et se déploie d'ores et déjà en dehors des navigateurs.
|
||||
|
||||
@ -55,9 +55,7 @@
|
||||
faire confiance au programme - notamment des pages web. Cet
|
||||
objectif de sûreté est en tension avec l'autre objectif de Wasm: être
|
||||
un langage bas niveau, efficace et ayant des performances aussi proches
|
||||
que possible de code natif, par exemple en étant une cible de compilation du C.
|
||||
|
||||
% TODO: ERIC: reprise intro générale/contexte + présentation + détaillée qui était dans l'offre de stage}
|
||||
que possible du code natif, par exemple en étant une cible de compilation du C.
|
||||
|
||||
% TODO: ERIC: faut il ajouter ici un exemple de code wasm + les 1ers éléments qui en ressortent ?
|
||||
% cf paragraphe 2.2 "prise en main" de mon rapport de stage
|
||||
@ -66,21 +64,20 @@
|
||||
% nécessaire en amont du paragraphe "génération de module"
|
||||
|
||||
\section{Owi}
|
||||
% TODO: reférence vers OCaml ?
|
||||
Owi\footnote{OCaml WebAssembly Interpreter} est un interpréteur de programmes WebAssembly écrit en OCaml.
|
||||
Son architecture est organisée en passes successives,
|
||||
lesquelles sont brièvement décrites ci-dessous.
|
||||
\paragraph{Analyse lexicale}
|
||||
Un module Wasm doit pouvoir importer et exporter des éléments respectivement depuis et vers le langage hôte.
|
||||
Un module Wasm doit pouvoir importer et exporter des items respectivement depuis et vers le langage hôte.
|
||||
Ce langage est susceptible d'utiliser des identifiants UTF-8. C'est notamment
|
||||
le cas de JavaScript. Pour cette raison, \emph{sedlex} est utilisé à la place du vénérable
|
||||
\emph{ocamllex}, ce dernier fournissant moins de primitives permettant de manipuler agréablement
|
||||
l'UTF-8.
|
||||
\paragraph{Analyse syntaxique}
|
||||
On utilise le générateur de parseurs \emph{menhir}. Le format texte de Wasm (Wat)
|
||||
autorise deux formats distincs. Le premier sous forme de \emph{S-expressions},
|
||||
le second sous forme de séquences d'instructions proche des assembleurs
|
||||
classiques. De plus, il est possible de mélanger les deux formats à certains
|
||||
autorise deux formats distincts. Le premier sous forme de \emph{S-expressions},
|
||||
le second proche des assembleurs classiques sous forme de séquences d'instructions.
|
||||
De plus, il est possible de mélanger les deux formats à certains
|
||||
endroits, ce qui complique l'écriture du parseur.
|
||||
\begin{minted}{wast}
|
||||
;; stack
|
||||
@ -95,7 +92,7 @@
|
||||
Une autre approche est envisagée afin de réduire la complexité induite par
|
||||
la gestion des deux formats. Il s'agit d'utiliser une bibliothèque de
|
||||
combinateurs de parseurs, par exemple \emph{Angstrom}. On peut alors imaginer combiner
|
||||
deux parseurs, un premier traitant uniquement les S-expression et le second les séquences
|
||||
deux parseurs, un premier traitant uniquement les S-expressions et le second les séquences
|
||||
d'instructions.
|
||||
L'analyse syntaxique produit un AST \mintinline{ocaml}{Text.modul}
|
||||
correspondant au format texte.
|
||||
@ -134,16 +131,16 @@
|
||||
Il s'agit de l'exécution du \mintinline{ocaml}{Runnable.modul}.
|
||||
|
||||
\paragraph{Extensions Wasm}
|
||||
Owi gère de nombreuses extensions de Wasm. Certaines faisant déjà partie du standard, à savoir:
|
||||
Owi gère de nombreuses extensions de Wasm dont certaines font déjà partie du standard, à savoir:
|
||||
\emph{Import/Export of Mutable Globals}, \emph{Non-trapping float-to-int conversions},
|
||||
\emph{Sign-extension operators}, \emph{Multi-value}, \emph{Reference Types}, \emph{Bulk memory operations}.
|
||||
Owi gère également certaines extensions encore en cours de développement, à savoir:
|
||||
\emph{Tail call} et \emph{Typed Function References}.
|
||||
La seule extension du standard non gérée est celle des \emph{Fixed-width SIMD}
|
||||
car elle contient beaucoup d'instructions et est laborieuse à implémenter.
|
||||
La majorité de ces extensions contient une importante suite de test qu'Owi
|
||||
La majorité de ces extensions contient une importante suite de tests qu'Owi
|
||||
passe avec succès. Cependant, l'extension qui est actuellement en train d'être ajoutée, à savoir celle
|
||||
portant sur le Garbage Collector, ne possède pour le moment qu'une suite de test minimale. Pour y palier, il a été
|
||||
portant sur le Garbage Collector, ne possède pour le moment qu'une suite de tests minimale. Pour y pallier, il a été
|
||||
décidé de trouver un moyen de tester efficacement l'interprète sans avoir à écrire à la main de nombreux
|
||||
tests unitaires. Notre choix s'est porté sur la technique du fuzzing, que l'on décrit ensuite.
|
||||
|
||||
@ -168,11 +165,12 @@ scruté, on en donne ici un aperçu.
|
||||
\paragraph{Whitebox fuzzing}
|
||||
Le whitebox fuzzing~\cite{GLM08} quant à lui consiste à effectuer une exécution symbolique~\cite{K76} du programme.
|
||||
Un solveur (de contraintes ou bien SMT) est généralement utilisé pour tester l'atteignabilité des différentes branches et produire des vecteurs de test.
|
||||
Cette techniqe est celle qui permet la plus grand couverture de code.
|
||||
Cette technique est celle qui permet la plus grand couverture de code.
|
||||
|
||||
\paragraph{Choix de la méthode de fuzzing et de l'outil}
|
||||
% TODO: ref vers QCheck https://github.com/c-cube/qcheck
|
||||
% TODO: re vers Crowbar https://github.com/stedolan/crowbar
|
||||
% TODO
|
||||
% ref vers QCheck https://github.com/c-cube/qcheck
|
||||
% ref vers Crowbar https://github.com/stedolan/crowbar
|
||||
% ERIC: je n'ai pas trouvé de papier sur qcheck et crowbar - sur les papiers trouvés sur le test citant ces lib, ils donnent les liens web
|
||||
Owi étant écrit en OCaml, seul le blackbox fuzzing ou le greybox fuzzing sont possibles, à travers les bibliothèques QCheck et Crowbar.
|
||||
Il n'existe pas à notre connaissance d'interpréteur symbolique d'OCaml permettant le whitebox fuzzing.
|
||||
@ -185,7 +183,7 @@ scruté, on en donne ici un aperçu.
|
||||
générer des chaînes de caractères aléatoires ne permet d'atteindre certaines passes qu'avec une faible probabilité.
|
||||
En effet, il faudrait pour cela que les chaînes générées arrivent à passer la phase de parsing ainsi que celle de validation.
|
||||
Notre choix a donc été de ne générer que des programmes syntaxiquement valides et correctement typés.
|
||||
Avec Crowbar, cela revient à utiliser les combinateurs fournis par la bibliothèque pour définir un générateur de module.
|
||||
Avec Crowbar, cela revient à utiliser les combinateurs fournis par la bibliothèque pour définir un générateur de modules.
|
||||
|
||||
% TODO: ERIC todo: exemple d'un mini programme avec un bug et mettre en évidence la proba très petite
|
||||
%de le détecter aléatoirement -> mise en évidence que la génération aléatoire de pg wasm syntaxiquement ok
|
||||
@ -243,9 +241,6 @@ scruté, on en donne ici un aperçu.
|
||||
complique le code et mène à des erreurs de type plus compliquées lors de la manipulation
|
||||
des générateurs pour des bénéfices non évidents.
|
||||
|
||||
% TODO: exemple suffisant ? (et valider sa correction ;)
|
||||
% NOTE eric : donner plus de détails sur l'environnement ? (déjà bcp de choses et place limitée ...)
|
||||
|
||||
Lorsque le nombre de générateurs devient important, comme c'est le cas ici\footnote{Notre fuzzer contient 83 appels à \mintinline{ocaml}{Crowbar.map} et 43 appels à \mintinline{ocaml}{Crowbar.dynamic_bind}.},
|
||||
l'imbrication de \mintinline{ocaml}{dynamic_bind} complexifie la lecture et la maintenance.
|
||||
Notre solution a été de définir un module \mintinline{ocaml}{Syntax} contenant des opérateurs monadiques \mintinline{ocaml}{let*},
|
||||
@ -294,14 +289,14 @@ scruté, on en donne ici un aperçu.
|
||||
|
||||
La génération se fait de façon récursive. On cherche à produire une expression de type
|
||||
\mintinline{ocaml}{~block_type} avec une pile de type \mintinline{ocaml}{~stack}.
|
||||
Pour éviter de générer des fonctions contenant trop d'instructions, l'environnement est initialement doté d'un \emph{fuel}.
|
||||
À chaque appel récursif, le fuel est décrémenté.
|
||||
Pour éviter de générer des fonctions contenant trop d'instructions, l'environnement est initialement doté d'un \emph{carburant}\footnote{Fuel.}.
|
||||
À chaque appel récursif, le carburant est décrémenté.
|
||||
Lorsque celui-ci tombe à zéro, on insère l'instruction \mintinline{wast}{drop} autant de fois que nécessaire pour vider la pile.
|
||||
Puis on ajoute des constantes sur la pile afin d'obtenir le type \mintinline{ocaml}{~block_type}.
|
||||
S'il reste du fuel, on sélectionne une instruction parmi celles qui sont compatibles avec le type courant de la pile.
|
||||
S'il reste du carburant, on sélectionne une instruction parmi celles qui sont compatibles avec le type courant de la pile.
|
||||
Puis on s'appelle récursivement avec le nouveau type de pile pour construire la suite de l'expression.
|
||||
|
||||
Dans le cas où le fuel est vide, il est possible de ne pas vider complètement la pile si le type de celle-ci
|
||||
Dans le cas où le carburant est vide, il est possible de ne pas vider complètement la pile si le type de celle-ci
|
||||
correspond partiellement au type que l'on veut obtenir. En effet, on peut réutiliser certains éléments ou bien des instructions
|
||||
qui les consomment pour produire des valeurs du type attendu. Il est prévu d'implémenter cette fonctionnalité à l'avenir.
|
||||
|
||||
@ -350,10 +345,10 @@ scruté, on en donne ici un aperçu.
|
||||
en ne testant que des fonctions individuellement, qui elles peuvent
|
||||
laisser des valeurs sur la pile en sortie.
|
||||
|
||||
Une autre difficulté est la gestion de la non terminaison.
|
||||
Une autre difficulté est la gestion de la non-terminaison.
|
||||
En effet, il est courant de générer des boucles ou des
|
||||
fonctions (mutuellement) récursives qui ne terminent pas.
|
||||
Pour palier à cela, un timeout est ajouté.
|
||||
Pour pallier cela, un timeout est ajouté.
|
||||
Dans le cas où les deux exécutions mènent à un timeout,
|
||||
le test est ignoré. Dans le cas où seulement l'une des deux
|
||||
produit un timeout, une option permet de choisir de signaler
|
||||
@ -392,7 +387,7 @@ scruté, on en donne ici un aperçu.
|
||||
|
||||
Plusieurs bugs ont été trouvés dans la partie d'exécution elle-même, souvent liés à des
|
||||
vérifications d'accès hors des bornes de la mémoire et des tables, à des overflow mal gérés
|
||||
ou encore à des mauvaises interprétations d'entiers signés comme non-signés et inversement.
|
||||
ou encore à de mauvaises interprétations d'entiers signés comme non signés et inversement.
|
||||
|
||||
Plus récemment, une réécriture majeure d'Owi a eu lieu afin de permettre au choix l'exécution
|
||||
concrète ou symbolique de programmes Wasm. Cette réécriture consistait en la "fonctorisation"
|
||||
@ -433,15 +428,15 @@ scruté, on en donne ici un aperçu.
|
||||
|
||||
\paragraph{Fuzzing intensif}
|
||||
Jusqu'à présent, le fuzzing n'a jamais été lancé plus de quelques minutes
|
||||
et avec un fuel minimal. Il est prévu de l'exécuter sur une période
|
||||
beaucoup plus longue et avec des valeurs de fuel plus élevées pour
|
||||
et avec un carburant minimal. Il est prévu de l'exécuter sur une période
|
||||
beaucoup plus longue et avec des valeurs de carburant plus élevées pour
|
||||
tenter de trouver plus de bugs.
|
||||
|
||||
\paragraph{Meilleure génération de module}
|
||||
Certaines limitations sont présentes dans la génération: la taille
|
||||
de la mémoire est limitée pour éviter l'utilisation massive de ressources
|
||||
qui ralentissent considérablement le fuzzing, les expressions
|
||||
sont générées brutalement une fois le fuel épuisé\ldots
|
||||
sont générées brutalement une fois le carburant épuisé\ldots~
|
||||
Corriger ces limitations pourrait permettre de générer une plus grande
|
||||
variété de programmes.
|
||||
|
||||
@ -463,7 +458,7 @@ scruté, on en donne ici un aperçu.
|
||||
Alt-ergo-fuzz~\cite{EBO22}. On y retrouve l'utilisation de Crowbar,
|
||||
d'autres solveurs SMT comme oracles, la génération de code
|
||||
bien typé pour arriver à atteindre les parties intéressantes,
|
||||
la gestion des timeouts\ldots Les principales différences ici sont
|
||||
la gestion des timeouts\ldots~Les principales différences ici sont
|
||||
la méthode utilisée pour la génération de code bien typé, Owi fuzz
|
||||
se base sur le type de la pile, ainsi que l'utilisation
|
||||
des combinateurs de Crowbar directement contre l'utilisation
|
||||
@ -479,20 +474,20 @@ scruté, on en donne ici un aperçu.
|
||||
\paragraph{Stack-driven program generation of WebAssembly}
|
||||
Dans l'article Stack-driven program generation of WebAssembly~\cite{PM20},
|
||||
les auteurs font également du fuzzing d'interprètes Wasm en utilisant
|
||||
des techniques similaires aux notres. La différence principale
|
||||
des techniques similaires aux nôtres. La différence principale
|
||||
étant le type de fuzzing. Les auteurs utilisent une approche en boîte noire
|
||||
qui atteint certains chemins avec une probabilité plus faible.
|
||||
|
||||
\section{Conclusion}
|
||||
L'écriture d'Owi Fuzz a permis de trouver différents bugs dans l'interprète.
|
||||
Au delà de la description des moyens de palier aux difficultés présentées spécifiquement
|
||||
Au-delà de la description des moyens de palier les difficultés présentées spécifiquement
|
||||
par le fuzzing d'interprètes Wasm, une utilisation des opérateurs monadiques associée aux combinateurs
|
||||
de Crowbar a été présentée.
|
||||
Elle permet de grandement faciliter la lecture, l'écriture et la maintenance
|
||||
du fuzzer. Cette contribution est désormais intégrée à Crowbar et nous
|
||||
pensons que sa réutilisation dans d'autres projets peut être bénéfique.
|
||||
Elle permettra aussi de faciliter l'extension de notre fuzzer pour les futures
|
||||
fonctionnalités qui seront ajoutées à Owi.
|
||||
Elle permettra aussi de faciliter l'extension de notre fuzzer pour les
|
||||
fonctionnalités qui seront ajoutées à Owi dans le futur.
|
||||
|
||||
\bibliography{bib}
|
||||
\bibliographystyle{alpha-fr}
|
||||
|
Loading…
x
Reference in New Issue
Block a user