Coccinelle (logiciel)

Coccinelle
Image illustrative de l’article Coccinelle (logiciel)
Date de première version 3 octobre 2010 (coccinelle-0.1)
Développeur Equipe Whisper [1]
Dernière version 1.0.8 [2] (le 25 septembre 2019, il y a 5 ans)
Écrit en Langage C, OCaml et Python
Licence GPLv2
Site web coccinelle.lip6.fr
modifier 

Le logiciel Coccinelle, un outil de correspondance et transformation en langage C, a été réalisé en 2008 par l’actuelle équipe de recherche Whisper[1] (Équipe de projet commune entre l’Inria et la Sorbonne Université) pour faciliter les spécifications et automatisations de l'évolution du noyau Linux. La nouvelle contribution de Coccinelle fut d'autoriser les développeurs à écrire des règles de manipulation de code directement dans la structure syntaxique du code, via la généralisation de syntaxe (en) de patch. Au fil des années, l’outil Coccinelle a été largement utilisé dans le développement du noyau Linux, aboutissant à plus de 6000 commits, et a trouvé sa place dans le processus de développement de Linux.

Caractéristiques de l'outil Coccinelle

[modifier | modifier le code]
Coccinelle
Fig. 1 Moteur de transformation Coccinelle

Coccinelle est un programme de correspondance et un outil de transformation pour le code en C. Il est utilisé pour la découverte de bugs dans les évolutions du noyau Linux et développé par Lawall, Muller et coll. depuis 2008[4]. Coccinelle a été à l'origine conçu pour cibler les évolutions collatérales des pilotes de périphériques Linux, où le but était de mettre à jour le code client en réponse à un changement de l'interface d'une bibliothèque[5]. Coccinelle a aussi été largement utilisé pour trouver et fixer des bugs[6],[7]. L'outil coccinelle est conçu pour être facile à utiliser par les développeurs de logiciels, sans exiger d’expertise dans l'analyse de programme, la transformation de programme, ou la conception interne de l'outil lui-même. À cette fin, l’outil de transformation Coccinelle et les règles de découverte de bug sont exprimées en utilisant une syntaxe qui est proche de celle d’un patch. Étant donné que Coccinelle tient compte de la sémantique du langage C, notamment sa structure de contrôle, Lawall et coll. font référence à l’outil de transformation Coccinelle ou à la spécification de recherche de bug comme un patch sémantique (semantic patch). En 2014, presque 2000 patchs acceptés dans le noyau Linux ont été créées en utilisant Coccinelle, y compris environ 700 patchs créés par 90 développeurs n’appartenant pas au groupe de recherche de Coccinelle[8].

Coccinelle est conçu autour d'un langage dédié (en anglais, domain-specific language ou DSL), SmPL (Semantic Patch Language), pour exprimer des changements en termes d'une forme abstraite de patch, mentionné comme un patch sémantique. À la différence d’un patch classique, qui est lié aux lignes et fichiers spécifiques dans le code source, un patch sémantique simple peut mettre à jour tous les emplacements appropriés dans la base de code entière[9].

La figure 1 montre les étapes principales exécutées par le moteur de Coccinelle. Les points clefs dans sa conception sont les stratégies pour (i) faire face au préprocesseur C (cpp), être capables de préserver le style de code original, (ii) faire l’ abstraction de la syntaxe et des variations de structure de contrôle et (iii) appliquer le code de transformation efficacement. Le résultat de correspondance de la formule CTL avec le CFG est une collection de nœuds où une transformation est requise, le fragment du patch sémantique qui correspond à ces nœuds et les liens de métavariable. Le moteur propage alors les - et + des annotations sur le patch sémantique aux tokens (en) correspondants aux nœuds correspondants du CFG, et ensuite à l’arbre de syntaxe abstraite. Le moteur unparse (en) l’arbre de syntaxe abstraite en supprimant n'importe quel token annoté avec - et en ajoutant les + du patch sémantique, comme approprié. N'importe quel métavariables dans l’ajout supplémentaire des + dans le code sont instanciés selon les liens établis par le processus de correspondance CTL[10].

  • Les méthodes utilisées par l'outil Coccinelle:
Isomorphisme
Les isomorphismes assimilent sémantiquement des fragments de code équivalents, pour extraire des variations dans le style de code, et l'utilisation de logique temporelle pour extraire des variations dans les chemins d'exécution spécifiques des périphériques. Le résultat de généricité implique qu’un simple patch sémantique de moins de 50 lignes peut suffire pour mettre à jour plus de 500 fichiers[10].
CTL (Logique du temps arborescent (en))
Le patch sémantique SmPL est compilé dans une formule de logique temporelle (CTL). La correspondance de la formule avec le modèle est alors mise en œuvre utilisant une variante d'un modèle standard vérifiant l'algorithme[11]. Tandis que CTL est probablement peu familier à la plupart des mainteneurs de pilote, il sert seulement comme un langage d’ assembleur, que le mainteneur de pilote ne doit pas lire ou comprendre[10].
CFG (Graphe de flot de contrôle)
Padioleau et coll. utilisent des chemins dans le graphe de flux de contrôle (CFG), comme une approximation du patron d'opérations exécutées au temps d(exécution par un pilote. Ainsi, une séquence de termes dans un patch sémantique SmPL correspond à une séquence de termes du langage C le long d'un chemin dans le CFG[10].
Vérification de modèles
Pour raisonner en graphes de flux de contrôle, Padioleau et coll. ont basé le moteur Coccinelle sur la technologie vérification de modèles, qui est orienté graphe[11]. Dans cette approche, chaque bloc (en) au plus haut niveau de code source C (par exemple, une fonction (en) ou une macro-définition) est traduit dans un graphique de flux de contrôle[10].
Stratégie d'adaptation au préprocesseur C (cpp)
Un analyseur syntaxique qui est capable d’adapter beaucoup d'utilisations des directives du préprocesseur C. Les commentaires et les espaces blancs (en) sont maintenus où c’est possible dans le code transformé pour préserver la capacité de comprendre et maintenir le pilote. Parce que les évolutions collatérales sont justes un pas dans la maintenance en cours d'un pilote de périphérique Linux, le moteur Coccinelle doit générer un code qui est lisible et dans le style du code source original, y compris l'utilisation de constructions cpp. En outre, une évolution collatérale peut impliquer des constructions cpp. Donc, Coccinelle fait l'analyse syntaxique du code C, sans étendre des directives du préprocesseur cpp, pour qu'elles soient préservés tant dans le processus de transformation que dans le code généré[10].

Origines du projet Coccinelle

[modifier | modifier le code]

Dans les systèmes d’exploitation (OS) modernes, les pilotes des périphériques peuvent constituer 70% du code source[12]. Le code du pilote est lui aussi fortement dépendant du reste du code source de l’OS, pour ses fonctions ainsi que la structure de données définie dans le noyau et les bibliothèques de support des pilotes. En conséquence, n’importe quels changements des interfaces du noyau ou des bibliothèques de support des pilotes vont probablement déclencher des modifications dans le code du périphérique pour rétablir son bon fonctionnement. Yoann Padioleau, Julia Lawall et Gilles Muller font référence, en octobre 2006, à ces modifications comme des évolutions collatérales. Elles peuvent entraîner des réorganisations de code substantielles, qui prennent du temps et sont sujettes aux erreurs. Le besoin d'évolutions collatérales peut donc gêner l'évolution de l'OS en pratique. C’est ainsi que Padioleau, Lawall et Muller ont commencé à examiner les problèmes révélés par ces évolutions collatérales dans le contexte de Linux[13].

En janvier 2007, ils ont proposé un langage de transformation déclaratif, SmPL (Semantic Patch Language), pour exprimer précisément les évolutions collatérales des pilotes de périphériques Linux. La communauté des programmeurs Linux est habitués à l'échange, la lecture et la manipulation de patchs qui fournissent un rapport des changements précédemment exécutés. Padioleau et coll. ont ainsi axé la syntaxe de SmPL sur la notation de fichier de patch. À la différence des patchs habituels, qui enregistrent les changements dans des fichiers spécifiques, SmPL peut décrire les transformations génériques qui s'appliquent aux évolutions collatérales multiples. Ce fut une première étape dans le projet de développer l’outil de transformation Coccinelle, fournissant une assistance automatisée pour exécuter des évolutions collatérales. Cette assistance comprend le langage SmPL pour spécifier les évolutions collatérales et un moteur de transformation pour les appliquer au code des pilotes de périphériques[14]. Le projet de développement de Coccinelle est soutenu par le Conseil de Recherche danois (Danish Research Council for Technology and Production) des universités de Copenhague et Aalborg et l’institut national de recherche en sciences et technologies du numérique (Inria) en France[15].

Les évolutions collatérales

[modifier | modifier le code]

Le problème des évolutions collatérales

[modifier | modifier le code]

L’équipe Whisper a évalué les divers aspects du besoin d'évolutions collatérales dans les pilotes de périphériques Linux, utilisant des outils d'extraction de données ad hoc qu’ils ont développé[5]. Ces résultats montrent que les bibliothèques de support des pilotes et les fichiers spécifiques des périphériques qui en dépendent sont nombreux et leurs relations complexes. Yoann Padioleau, René R. Hansen, Julia Lawall et Gilles Muller ont ainsi identifié en 2006, dans la version 2.6.13 du noyau Linux, 150 bibliothèques de support de pilotes et presque 2000 fichiers spécifiques des périphériques. Un fichier spécifique de périphérique peut utiliser jusqu'à 59 fonctions de bibliothèque différentes. Plutôt que de devenir plus stable, cette base de code se développe de plus en plus rapidement[16]. Ils ont constaté que le nombre d'évolutions dans les éléments d'interface croient fortement, avec 300 évolutions probables dans le code de Linux 2.2 et plus de 1200 dans Linux 2.6 jusqu'à Linux 2.6.13. Certaines de ces évolutions déclenchent des évolutions collatérales dans presque 400 fichiers. Entre Linux 2.6.9 et Linux 2.6.10, plus de 10 000 lignes de code périphériques spécifique, affectées par des évolutions collatérales, ont été trouvées[17].

Les divers aspects du processus des évolutions collatérales

[modifier | modifier le code]

Avant l’arrivée de l’outil Coccinelle, ces évolutions suivaient ce procédé typique : Quand un développeur fait un changement dans une bibliothèque Linux interne qui a un impact sur une API, il met manuellement à jour tout le code spécifique du périphérique dans l'arborescence source Linux, basé sur sa compréhension de l'évolution et son approche des pilotes concernés. Ensuite, les mainteneurs des nombreux pilotes extérieurs à l'arborescence source de Linux exécutent l'évolution collatérale dans leurs propres codes. Ces mainteneurs de pilotes n'ont pas la connaissance immédiate de cette évolution et doivent ainsi déduire comment elle s'applique à leurs codes depuis n'importe quels commentaires de code disponibles, de mails informels et de patchs souvent volumineuses. Finalement, des utilisateurs motivés appliquent les évolutions collatérales pour coder ce qui a été omis par le développeur de bibliothèque ou le mainteneur de pilotes. Et ce cas pose problème au mainteneur de pilotes car ces utilisateurs ne peuvent avoir aucune expérience avec l'évolution collatérale ou le code des pilotes[18].

Comme Linux est un OS open source, beaucoup de programmeurs différents contribuent à son développement. En effet, les mainteneurs de pilote ne sont souvent pas des experts du noyau, mais plutôt des experts d’un périphérique donné ou même des utilisateurs ordinaires qui constatent que leur matériel n'est pas correctement supporté. Parce que les développeurs qui mettent à jour le noyau et les bibliothèques de support des pilotes ne partagent pas souvent de langage commun et une expertise avec le mainteneur de périphérique, la documentation d'évolutions collatérales complexes est souvent incomplète[13].

Les précédentes tentatives de résolution

[modifier | modifier le code]

La réutilisation de pilotes de périphériques a été tentée par la restructuration des systèmes d'exploitation utilisant une approche de micro-noyau. Goel et Duchamp[19] ont émulé des pilotes de périphériques de Linux sur un micro-noyau Mach 4.0, avec des résultats de performance décevants . L’architecture Chorus/MiX[20] a aussi essayé de démultiplier des pilotes de périphériques existants en les exécutants comme des entités indépendantes. Cependant, cette solution a fourni une migration moins transparente qu'attendue, et quelques adaptations étaient toujours requises. Une approche semblable avait été entreprise dans le système Minix[21], bien qu’elle soit plus centrée sur la conception de systèmes minimaux pour des objectifs de fiabilité qu'en réutilisant du logiciel hérité[22].

Semantic patches (SmPL)

[modifier | modifier le code]

SmPL est l’acronyme pour “Semantic Patch Language”, il se prononce “simple” en Français[23].

Les buts de ce nouveau langage

[modifier | modifier le code]

La communauté Linux utilise divers outils pour mieux analyser le langage C. Sparse[24] est une bibliothèque qui, comme un compilateur front end, fournit l’accès à l'arbre de syntaxe abstraite et l'information de saisie d'un programme en C. Cette bibliothèque a été utilisée pour implémenter quelques analyses statiques ciblant la détection de bug, construite sur des annotations supplémentaires aux déclarations de variables, dans l'esprit de static et constant. Smatch[25] est un projet semblable qui permet à un développeur d'écrire des scripts en Perl pour analyser du code en C. Ces deux projets ont été inspirés par le travail d'Engler et coll. sur l’automatisation de la recherche de bug dans les codes de systèmes d’exploitation[26]. Ces exemples montrent que la communauté Linux est ouverte à l'utilisation d'outils automatisés pour améliorer la qualité du code, particulièrement quand ces outils sont construits sur les secteurs traditionnels d'expertise des développeurs Linux[27].

Pour être capable de décrire génériquement des évolutions collatérales, en restant cohérent avec le modèle de développement de code du noyau Linux, Padioleau et coll. ont étendu la notation de patch pour inclure les aspects de la sémantique du langage C, et non juste sa syntaxe. Ils font ainsi référence à des patchs sémantiques (semantic patches) pour leurs spécifications. En utilisant ces patchs sémantiques, ils affinent le modèle de patch décrit ci-dessus. Ainsi seul le développeur de bibliothèque applique manuellement l'évolution collatérale à quelques fichiers de pilotes, pour obtenir un sens aux changements qui sont exigés et écrit ensuite des patchs sémantiques qui peuvent être appliquées aux fichiers restants et distribuées à d'autres mainteneurs de pilotes. Le but des patchs sémantiques est de s'appliquer indépendamment du style de code, mais ce n'est pas possible en pratique de prévoir toutes les variations possibles. Ainsi, l'outil devrait non seulement appliquer des patchs sémantiques, mais devrait être aussi capable d'aider le développeur ou le mainteneur de pilote quand une correspondance exacte de la règle avec le code source n'est pas possible[28].

Syntaxe de SmPL

[modifier | modifier le code]

En général, le patch sémantique a la forme d'un patch traditionnel[29], consistant en une séquence de règles dont chacune commence par une information de contexte délimitée par une paire de @@ et spécifie ensuite une transformation appliqué dans ce contexte.

Exemple d'un patch sémantique pour mettre à jour des fonctions SCSI proc_info avec l'outil diff : 

@@
local function proc_info_func;
identifier buffer, start, offset, length, inout, hostno;
identifier hostptr;
@@
proc_info_func (
+ struct Scsi_Host *hostptr,
char *buffer, char **start, off_t offset,
int length, int hostno, int inout) {
 ...
- struct Scsi_Host *hostptr;
 ...
- hostptr = scsi_host_hn_get(hostno);
 ...
- if (!hostptr) { ... return ...; }
 ...
- scsi_host_put(hostptr);
 ...
 }

Dans le cas d’un patch sémantique, l'information de contexte ne déclare pas des numéros de ligne, mais un groupe de métas variables. Un méta variable peut correspondre à n'importe quel terme indiqué dans sa déclaration (identificateur, expression, etc), de telle sorte que toutes les références à un méta variable donné correspondent au même terme. La règle de transformation est spécifiée comme dans un fichier de patch traditionnel, avec un terme ayant la forme du code à être transformé. Ce terme est annoté avec les modificateurs - et + pour indiquer le code qui doit être respectivement supprimé et ajouté. Les lignes 1-5 du patch sémantique du code ci-dessus déclarent une collection de métas variables. La plupart de ces métas variables sont utilisées dans la fonction d’ en-tête aux lignes 6-9 pour spécifier le nom de la fonction qui sert à transformer et les noms de ses paramètres. L’action de spécifier la fonction d'en-tête en termes de métas variables identifie efficacement la fonction qui sert à transformer en des termes de son prototype. Ce qui est défini par la bibliothèque SCSI et est ainsi commun à toutes les fonctions proc_info. A noter que quand une définition de fonction est transformée, le prototype correspondant est aussi transformé automatiquement de la même manière ; il n'est donc pas nécessaire de spécifier explicitement la transformation d'un prototype de patch sémantique. Le reste du code spécifie le déplacement des fragments de code divers décrits au-dessus du corps de la fonction. Comme le code à supprimer n'est pas nécessairement contigu, ces fragments sont séparés par l'opérateur SmPL "...", qui correspond à n'importe quel ordre d'instructions. La pièce sémantique spécifie aussi qu'une ligne devrait être ajoutée : la déclaration indiquée à la ligne 11 pour être enlevé du corps de fonction est spécifiée pour être ajouté à la liste de paramètre à la ligne 7 par une référence répétée au méta variable hostptr. En général, la règle s'applique indépendamment des espacements, des sauts de ligne et des commentaires. De plus, le moteur de transformation est paramétré par une collection d'isomorphismes spécifiant les ensembles des équivalences qui sont prises compte en appliquant la règle de transformation[30].

L’équipe Whisper commençait à concevoir les prémices d’une structure, Coccinelle, qui inclut un langage, SmPL dans lequel s’expriment les patchs sémantiques qui décrivent des évolutions collatérales et un outil de transformation pour appliquer ces patchs sémantiques au code spécifique des périphériques. Pour s’adapter aux habitudes des développeurs Linux et fournir une syntaxe lisible, SmPL est basé sur le format de patch standard[31].

Exemple d’autres structures de transformation de programmes

[modifier | modifier le code]

D’autres structures de transformation de programme ont été proposées, s’appuyant sur des langages comme C et Java. CIL (en)[32] et XTC[33] sont essentiellement des analyseurs syntaxiques qui fournissent un support pour mettre en œuvre des parcours d'arbres de syntaxes abstraites. CIL gère aussi le code source du langage C en termes de représentation intermédiaire plus simple. Réécrire des règles doit être exprimé en termes de cette représentation plutôt qu'en termes de code trouvé dans le pilote approprié. Stratego est un langage dédié qui sert à écrire des transformations de programme[34]. Un filtrage par motif correct et des stratégies de gestion de règle y sont intégrés et impliquent que le développeur peut spécifier les transformations devant arriver sans encombrer le code avec la mise en œuvre de mécanismes de transformation. Néanmoins, seulement quelques analyses de programme sont fournies. Les autres analyses qui sont exigées, comme l'analyse de flux de contrôle, doivent être mises en œuvre dans le langage Stratego. D’après Padioleau et coll., cela mène à des règles qui sont très complexes pour exprimer des évolutions collatérales même simples[27].

Évolutions de l'outil Coccinelle

[modifier | modifier le code]

Introduction des langages de script

[modifier | modifier le code]

L'interface de langage de script a été initialement motivée dans le but d'utiliser Coccinelle pour trouver des bugs[35]. Les bugs qui dépendent principalement de la structure du code, comme la vulnérabilité use-after-free(oubli par un développeur de réinitialiser un pointeur après une libération de la mémoire)[36], pourraient être trouvés; alors que le filtrage par motif des fonctionnalités de Coccinelle n'était pas suffisant pour détecter des bugs comme le dépassement de tampon qui exige le raisonnement des variables d’environnement. Pour permettre le raisonnement de l'information arbitraire, un support a été ajouté en 2008 pour les règles de langage de script. Le premier langage supporté était Python, qui était attendu comme familier aux développeurs Linux. Coccinelle est implémenté dans OCaml, et le script OCaml a été ajouté en 2010, pour la commodité des développeurs Coccinelle. Les scripts ont été à l'origine conçus pour filtrer les ensembles de métas variables établies selon les règles précédentes.

Le code ci-dessous montre un exemple de suppression d’un point-virgule après un en-tête « if » si l’ expression de sous-suite est désignée, suggérant que la dernière expression soit indentée pour être dans le branchement « if ». Une règle de script compare l' indentation des deux expressions (ligne 11) et annule le méta variable des environnements de liaisons (ligne 12) dans lequel l’ instruction conditionnelle est alignée avec ou à droite de l’expression de sous-suite. 

@r@                           
expression E; statement S; 
position p1,p2;
@@
if@p1 (E);
    S@p2

@script:python@
p1 << r.p1; p2 << r.p2;
@@
if (p1[0].col >= p2[0].col):
   cocci.include_match(False)

@@
expression E; statement S;
position r.p1;
@@
if@p1 (E)
- ;
S

Finalement, la motivation première pour le script, c'est-à-dire trouver des bugs comme le dépassement de tampon, n'était pas couronné de succès. En effet, les modèles de code étaient petits et génériques et les scénarios implémentant les analyses exigées étaient complexes. Cependant, le script a été un bond en avant pour l'expressivité de Coccinelle et des nouvelles fonctionnalités de script ont été ajoutées comme de nouveaux besoins ont émergé. Dès le début, les bibliothèques ont été ajoutées pour produire des messages d'erreur formatés. En 2009, les scripts initialize et finalize (en) ont été introduits pour permettre de définir l'état global du traitement de tous les fichiers, faciliter la collection de statistiques. En 2010, les scripts sont devenus capables de créer des nouveaux fragments de code pouvant être stockés dans des métas variables et hérités selon des règles de sous-suite. En 2016, pour améliorer la performance et réduire la taille du patch sémantique, il est devenu possible d'ajouter du code de script aux déclarations de méta variable, pour définir les prédicats qui annulent les liaisons de métas variable au début du processus de comparaison. Finalement, le script autorise l'itération, qui permet à un patch sémantique de soumettre de nouveaux jobs au moteur de Coccinelle, pour exécuter l'analyse à travers de multiples fichiers[37].

Sécurité et détection de vulnérabilités par Coccinelle

[modifier | modifier le code]

OpenSSL

[modifier | modifier le code]

Dans ce projet, Lawall et coll. ont utilisé Coccinelle sur un type de bug qui a été précédemment mis en évidence dans le code d'OpenSSL selon le rapport CVE-2008-5077[38] de vulnérabilité de sécurité à la suggestion de Ben Laurie, qui est un expert OpenSSL. Cette vulnérabilité est basée sur l'observation que beaucoup de fonctions dans OpenSSL retournent des entiers faux-positifs pour indiquer les divers types d'erreurs. Néanmoins, le code callsite (en) errorchecking considère souvent seulement le 0 comme une erreur et toute autre valeur comme réussie. Ce modèle n'existe pas dans Linux et la connaissance spécifique de OpenSSL est nécessaire. Lawall et coll. ont détecté environ 30 bugs dans un snapshot d'OpenSSL (openssl-1.0.0-stable-snap-20090911). Dans des nombreux cas, ils étaient capables d'utiliser les capacités de transformation de programme du moteur Coccinelle pour corriger automatiquement ces bugs. La plupart des patchs de correction de ces bugs ont été soumis aux développeurs OpenSSL et tous ces patchs correctifs ont été acceptés. Le tableau 1 présente les rapports donnés par les règles du patch sémantique qui détecte des tests directs et le tableau 2 présente les rapports donnés par les règles du patch sémantique qui détecte des tests sur des valeurs stockées. Acc. (Accepté) indique le nombre de bugs pour lesquels les patchs ont été soumis et acceptées par les développeurs OpenSSL. FP indique le nombre de faux positif. Unk. (Inconnu) indique des rapports dont Lawall et coll. n’étaient pas capables de classifier comme des bugs ou des faux positifs. En général, le taux de faux positif est aux alentours de 50 %. Ce taux est haut, mais le nombre complet de rapports est peu élevé. Ils s’attendent à ce que cela puisse être fait plus rapidement par un expert de OpenSSL[39].

Tableau 1
Bugs Acc. FP Unk. Files
ASN1_item _ex _d2i 0 0 1 0 1
BIO_ctrl 1 0 0 0 1
BIO_write 6 6 0 0 3
BN_exp 1 1 0 0 1
CMS_get1_ReceiptRequest 2 2 0 0 1
ENGINE_ctrl 4 4 1 0 2
EVP_PKEY_cmp_parameters 0 0 1 0 1
EVP_PKEY_sign 1 1 0 0 1
OPENSSL_isservice 1 1 2 0 3
RAND_bytes 4 3 0 0 4
RAND_pseudo_bytes 2 0 0 0 1
UI_ctrl 0 0 2 0 2
X509_STORE_get_by_subject 0 0 0 2 1
X509_check_purpose 0 0 0 1 1
asn1_cb 0 0 10 0 3
asn1_check_tlen 0 0 2 0 1
i2a_ASN1_INTEGER 1 1 0 0 1
i2a_ASN1_OBJECT 1 1 0 0 1
sk_num 0 0 3 0 1
TOTAL 26 20 20 3 30
Tableau 2
Bugs Acc. FP Unk. Files
ASN1_INTEGER_get 0 0 2 0 2
BIO_ctrl 1 1 0 0 1
EVP_DigestVerifyFinal 1 1 0 0 1
EVP_SealInit 1 1 0 0 1
RAND_bytes 1 1 0 0 1
SSLStateMachine_read_extract 0 0 1 0 1
UI_UTIL_read_pw 0 0 1 0 1
X509_check_purpose 0 0 1 1 2
asn1_cb 0 0 4 0 2
asn1_check_tlen 0 0 2 0 1
asn1_template_noexp_d2i 0 0 1 0 1
dtls1_retrieve_buffered_fragment 0 0 0 1 1
get_cert_chain 0 0 1 0 1
i2b_PVK_bio 2 2 0 0 2
ocsp_check_issuer 0 0 1 0 1
TOTAL 6 6 14 2 19

Dans un autre projet, Lawall et coll. ont développé un outil, Herodotos[40], qui suit à la trace l'histoire des fragments de code qui correspondent à un patch sémantique donné sur les versions multiples d'un projet de logiciel. Ils ont appliqué Herodotos aux versions OpenSSL 0.9.8a par 0.9.8j, sortis entre 2005 et 2008, et aux semantic pachs définis dans les tableaux 1 et 2, pour obtenir un historique d'erreurs traitant des bugs. Ils ont constaté que presque tous les bugs trouvés ont été présents depuis au moins la version 0.9.8a, avec une poignée introduit à une date ultérieure, en raison d'un certain changement du code ou l'introduction d'un nouveau fichier[39].

Jana et coll. ont aussi cherché des contrôles d'erreur dans OpenSSL avec leur outil EPEx, en s’assurant en plus que l'erreur soit correctement traitée. Cela leur a permis de trouver une classe significativement plus grande de traitements des erreurs. Aussi, avec leur approche, ils ont un taux peu élevé de faux positif[41].

CERT C Secure Coding Standard

[modifier | modifier le code]

Olesen et coll. ont adapté l’outil Coccinelle dans un outil, Clang, pour analyser et certifier des programmes en C, en accord avec le CERT C Secure Coding Standard et le standard MISRA (the Motor Industry Software Reliability Association) C. Ils soutiennent qu'un tel outil doit être fortement adaptable et customisable à chaque projet de logiciel aussi bien qu'aux règles de certification exigées par une norme donnée[42].

Recherche de vulnérabilités sur Android

[modifier | modifier le code]

Lu et coll. ont expérimenté le langage SmPL de Coccinelle pour évaluer les différentes éditions d'Android. Ils ciblent principalement trois types d’utilisations défectueuses des pointeurs.

Memory not released (Mémoire (en) non libérée)
Si la mémoire dynamique pointée par le pointeur n'est pas libérée après utilisation, alors il y a une fuite de mémoire.
Null pointer reference (Référence de pointeur nul (en))
Si un pointeur ne se déclare pas avant qu'il soit utilisé ou un pointeur nul est utilisé comme un objet, il y aura quelques fautes d’utilisations des pointeurs qui peuvent être des vulnérabilités.
Usage of float pointer (Utilisation de pointeur avec virgule flottante)
Lorsque la mémoire ciblée par le pointeur est utilisée et libérée, la mémoire ciblée par le pointeur retourne au système d'exploitation. L'indicateur devient une virgule flottante à 1. S'il n'est pas traité correctement, il y aura une faute (en) de référence du pointeur.

Pour leurs expérimentations, Lu et coll. ont utilisé trois éditions différentes d'Android, 2.1, 3.0 et 4.0 pour trouver les possibilités de fautes dans les codes. Ils ont obtenu 48 fautes avec Android 2.1, dont il y a 9 vulnérabilités confirmées. La raison des faux positifs est que Coccinelle n'a pas la capacité de faire l’analyse de flux de données (en) et ne peut pas couper les branchements qui ne sont pas accessibles[43].

Resultat Android 2.1
Type de Faute Faute Erreur Total
NUM NUM NUM
Mémoire non libérée 5 22 25
Référence de pointeur nul 3 11 24
Utilisation de pointeur avec virgule flottante 1 8 9
Resultat Android 3.0
Type de Faute Faute Erreur Total
NUM NUM NUM
Mémoire non libérée 9 49 51
Référence de pointeur nul 2 11 13
Utilisation de pointeur avec virgule flottante 2 12 14
Resultat Android 4.0
Type de Faute Faute Erreur Total
NUM NUM NUM
Mémoire non libérée 7 36 40
Référence de pointeur nul 2 21 23
Utilisation de pointeur avec virgule flottante 1 9 10

Évolutions des performances

[modifier | modifier le code]

Une des premières observations de Lawall et coll. était que la performance pourrait être améliorée en ne faisant pas l'analyse syntaxique des fichiers qui ne correspondent pas à un patch sémantique. En effet, beaucoup de patchs sémantiques contiennent des mots-clés comme les noms des fonctions d'API qui doivent les assister pour correspondre et cela arrive peu souvent dans le noyau Linux. Coccinelle a initialement utilisé la commande Unix grep pour trouver les fichiers contenant ces mots-clés, mais avec des lenteurs, étant donné la grande taille de code [44].

Le moteur Coccinelle utilise alors grep, ou l'indexation de texte intégral et d'outil de recherche glimpse[45] si cette option a été activée par l'utilisateur, pour identifier les fichiers qui contiennent au moins un de ces mots clefs[46].

Cette deuxième approche d'utiliser glimpse pour préparer un index d'avance et ensuite seulement traiter les fichiers indiqués par l'index. Comme l'index est plus petit que le code source du noyau et est organisé efficacement, l'utilisation de glimpse améliore considérablement la performance, particulièrement pour les patchs sémantiques qui impliquent des fonctions d'API du noyau. Néanmoins, glimpse était à l'origine seulement disponible librement aux utilisateurs universitaires, il a dû être manuellement installé et la création d'un index sur chaque mise à jour de noyau est chronophage. En 2010, Coccinelle a été complété par le support de id-utils[47], qui fait partie de nombreuses distributions Linux et pour lequel la création d'index est beaucoup plus rapide. En 2013, le support pour les utilisateurs qui n'ont pas d'index disponible a été réécrit pour essentiellement ré implémenter la commande grep dans OCaml, réduisant les appels de système et de mieux tenir compte des besoins spécifiques de Coccinelle[44].

Impact sur Linux

[modifier | modifier le code]

Augmentation des commits Coccinelle

[modifier | modifier le code]

Le sous-système le plus affecté est celui des drivers (pilotes), avec 57 882 lignes supprimées et 77 306 lignes rajoutées, suivies par les sous-systèmes arch, fs, net, sound, et include, qui sont tous affectés par des milliers de lignes supprimées ou rajoutées. La prédominance de drivers n'est pas surprenante, étant donné qu’ils composent 67 % du code source du noyau Linux 4.15. Le sous-système drivers a aussi été expérimenté par d'autres outils de découverte de bugs et de fiabilité de code[48],[49],[50],[51],[52]. Le taux de lignes changées par Coccinelle pour le sous-système drivers reste élevé, mais les résultats montrent l'applicabilité de Coccinelle à travers le noyau[53].

Catégories d'utilisateurs

[modifier | modifier le code]

Différents types de développeurs contribuent au noyau Linux, en soumettant des patchs. Parmi ceux qui mentionnent Coccinelle dans leur historiques de commit, Lawall et coll. distinguent six catégories d'utilisateurs Coccinelle :

Les développeurs Coccinelle
Ce sont les membres de l'équipe de développement Coccinelle et des personnes employées par l'équipe pour disséminer Coccinelle.
Les stagiaires Outreachy
Le noyau Linux participe au programme de stage[54] de Outreachy et les stagiaires peuvent utiliser Coccinelle dans le processus d'application ou le programme de stage.
Utilisateur dédié
C'est un développeur qui utilise Coccinelle dans le noyau pour une petite collection de simples changements largement appropriés.
0-day
C'est un service de test automatisé Intel qui construit et démarre le noyau Linux pour de multiples configurations de noyau, sur chaque commit pour les centaines d’arbres de git. Ce service de test dirige aussi un certain nombre d'outils d'analyse statiques, y compris Coccinelle, sur le résultat de chaque commit.
Les mainteneurs de noyau
Ce sont les développeurs de noyau qui reçoivent et commit les patchs, et sont généralement responsables de quelques sous-systèmes. Lawall et coll. ont identifié les mainteneurs comme les développeurs qui sont nommés dans le fichier MAINTENERS de Linux 4.15 (1170 développeurs).
Les autres contributeurs
Ces contributeurs peuvent être fréquents ou occasionnels[53].

Références

[modifier | modifier le code]
  1. ↑ a et b whisper
  2. ↑ coccinelle
  3. ↑ « https://gitlab.inria.fr/coccinelle/coccinelle/-/tags/1.3.0 », (consulté le )
  4. ↑ Lawall 2008
  5. ↑ a et b Padioleau 2006
  6. ↑ Lawall 2013
  7. ↑ Palix 2011
  8. ↑ Lawall 2014, p. 5
  9. ↑ Lawall 2018, p. 601
  10. ↑ a b c d e et f Padioleau 2008, p. 248-252
  11. ↑ a et b Huth 2000
  12. ↑ Chou 2006, p. 74
  13. ↑ a et b Padioleau 2006, p. 59
  14. ↑ Padioleau 2007, p. 48
  15. ↑ Lawall 2010, p. 54
  16. ↑ Godfrey 2000
  17. ↑ Padioleau 2006, p. 11-12
  18. ↑ Padioleau 2008, p. 248
  19. ↑ Goel 1996
  20. ↑ Armand 1991
  21. ↑ Herder 2006
  22. ↑ Armand 2008, p. 13
  23. ↑ Muller 2006, p. 91
  24. ↑ Searls 2003
  25. ↑ smatch 2002
  26. ↑ Engler 2000
  27. ↑ a et b Padioleau 2007, p. 57
  28. ↑ Padioleau 2006, p. 11
  29. ↑ MacKenzie 2003
  30. ↑ Padioleau 2006, p. 12
  31. ↑ Padioleau 2006, p. 91
  32. ↑ Necula 2002
  33. ↑ Pottier 2019
  34. ↑ Visser 2003
  35. ↑ Stuart 2007
  36. ↑ Lobo 2019
  37. ↑ Lawall 2018, p. 604
  38. ↑ Rievers 2009, p. 4
  39. ↑ a et b Lawall 2009, p. 191
  40. ↑ Palix 2010
  41. ↑ Jana 2016, p. 358
  42. ↑ Olesen 2014, p. 141
  43. ↑ Lu 2016, p. 498-499
  44. ↑ a et b Lawall 2018, p. 605-606
  45. ↑ Manber 1994, p. 1-10
  46. ↑ Padioleau 2008, p. 252
  47. ↑ idutils 2012
  48. ↑ Machiry 2017, p. 1007-1024
  49. ↑ Mérillon 2000
  50. ↑ Renzelmann 2012, p. 279-282
  51. ↑ Ryzhnyk 2011, p. 133
  52. ↑ Swift 2017, p. 1007-1024
  53. ↑ a et b Lawall 2018, p. 607-608
  54. ↑ outreachy

Bibliographie

[modifier | modifier le code]

Recherches sur l’outil Coccinelle

[modifier | modifier le code]
  • (en) Yoann Padioleau, Julia Lawall et Gilles Muller, « Understanding collateral evolution in Linux device drivers », ACM SIGOPS Operating Systems Review, vol. 40, no 4,‎ , p. 59-71 (ISSN 0163-5980, DOI 10.1145/1218063.1217942)
  • (en) Julia Lawall et Gilles Muller, « Coccinelle: 10 years of Automated Evolution in the Linux Kernel », Proceedings of the 2018 USENIX Annual Technical Conference (USENIX ATC ’18),‎ , p. 601-613 (ISBN 9781931971447)
  • (en) Julia Lawall, « Coccinelle: reducing the barriers to modularization in a large C code base », Proceedings of the companion publication of the 13th international conference on Modularity,‎ , p. 5-6 (ISBN 9781450327732, DOI 10.1145/2584469.2584661)
  • (en) Luis R. Rodriguez et Julia Lawall, « Increasing Automation in the Backporting of Linux Drivers Using Coccinelle », 2015 11th European Dependable Computing Conference (EDCC),‎ , p. 132-143 (ISBN 9781467392891, DOI 10.1109/EDCC.2015.23)
  • (en) Julia Lawall, Ben Laurie, René Rydhof Hansen, Nicolas Palix et Gilles Muller, « Finding Error Handling Bugs in OpenSSL Using Coccinelle », 2010 European Dependable Computing Conference,‎ , p. 191-196 (ISBN 9781424465941, DOI 10.1109/EDCC.2010.31)
  • (en) Yoann Padioleau, Julia Lawall, René Rydhof Hansen et Gilles Muller, « Documenting and automating collateral evolutions in linux device drivers », Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on computer systems 2008,‎ , p. 247-260 (ISBN 9781605580135, DOI 10.1145/1352592.1352618)
  • (en) Julia Lawall, Julien Brunel, Nicolas Palix, René Rydhof Hansen, Henrik Stuart et Gilles Muller, « WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code », 2009 IEEE/IFIP International Conference on Dependable Systems & Networks,‎ , p. 43-52 (ISBN 9781424444229, DOI 10.1109/DSN.2009.5270354)
  • (en) Julia Lawall, Julien Brunel, Nicolas Palix, René Rydhof Hansen, Henrik Stuart et Gilles Muller, « WYSIWIB: exploiting fine‐grained program structure in a scriptable API‐usage protocol‐finding process », Software: Practice and Experience, vol. 43, no 1,‎ , p. 67-92 (ISSN 0038-0644, DOI 10.1002/spe.2102)
  • (en) Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia Lawall et Gilles Muller, « A foundation for flow-based program matching: using temporal logic and model checking », POPL '09 Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages,‎ , p. 114-126 (ISBN 9781605583792, DOI 10.1145/1480881.1480897)
  • (en) Gilles Muller, Yoann Padioleau, Julia Lawall et René Hansen, « Semantic patches considered helpful », ACM SIGOPS Operating Systems Review, vol. 40, no 3,‎ , p. 90-92 (ISSN 0163-5980, DOI 10.1145/1151374.1151392)
  • (en) Julia Lawall, Gilles Muller et Nicolas Palix, « Enforcing the use of API functions in linux code », Proceedings of the 8th workshop on aspects, components, and patterns for infrastructure software,‎ , p. 7-12 (ISBN 9781605584508, DOI 10.1145/1509276.1509279)
  • (en) Henrik Stuart, René Rydhof Hansen, Julia Lawall, Jesper Andersen, Yoann Padioleau et Gilles Muller, « Towards easing the diagnosis of bugs in OS code », Proceedings of the 4th workshop on programming languages and operating systems,‎ , p. 1-5 (ISBN 9781595939227, DOI 10.1145/1376789.1376792)
  • (en) Yoann Padioleau, René Rydhof Hansen, Julia Lawall et Gilles Muller, « Semantic patches for documenting and automating collateral evolutions in Linux device driver », Proceedings of the 3rd workshop on programming languages and operating systems,‎ , p. 10-es (ISBN 1595935770, DOI 10.1145/1215995.1216005)
  • (en) Nicolas Palix, Julia Lawall et Gilles Muller, « Tracking code patterns over multiple software versions with Herodotos », Proceedings of the 9th International Conference on aspect-oriented software development,‎ , p. 169-180 (ISBN 9781605589589, DOI 10.1145/1739230.1739250)
  • (en) Suman Saha, Julia Lawall et Gilles Muller, « Finding resource-release omission faults in Linux », ACM SIGOPS Operating Systems Review, vol. 45, no 3,‎ , p. 5-9 (ISSN 0163-5980, DOI 10.1145/2094091.2094094)
  • (en) Peter Senna Tschudin, Laurent Réveillère, Lingxiao Jiang, David Lo, Julia Lawall et Gilles Muller, « Understanding the genetic makeup of Linux device drivers », Proceedings of the Seventh Workshop on programming languages and operating systems,‎ , p. 1-6 (ISBN 9781450324601, DOI 10.1145/2525528.2525536)
  • (en) Julia Lawall et David Lo, « An automated approach for finding variable-constant pairing bugs », Proceedings of the IEEE/ACM international conference on automated software engineering,‎ , p. 103-112 (ISBN 9781450301169, DOI 10.1145/1858996.1859014)
  • (en) Tegawendé Bissyandé, Laurent Réveillère, Julia Lawall et Gilles Muller, « Ahead of time static analysis for automatic generation of debugging interfaces to the Linux kernel », Automated Software Engineering, vol. 23, no 1,‎ , p. 3-41 (ISSN 1573-7535, DOI 10.1007/s10515-014-0152-4)
  • (en) Mads Chr Olesen, René Rydhof Hansen, Julia Lawall et Nicolas Palix, « Coccinelle: Tool support for automated CERT C Secure Coding Standard certification », Science of Computer Programming, vol. 91,‎ , p. 141-160 (ISSN 0167-6423, DOI 10.1016/j.scico.2012.10.011)
  • (en) Julia Lawall, René Rydhof Hansen, Nicolas Palix et Gilles Muller, « Improving the Security of Infrastructure Software using Coccinelle », ERCIM News, vol. 83,‎ , p. 54 (ISSN 0926-4981)
  • (en) Jesper Andersen, Anh Cuong Nguyen, David Lo, Julia Lawall et Siau-Cheng Khoo, « Semantic patch inference », Proceedings of the 27th IEEE/ACM International Conference on automated software engineering,‎ , p. 382-385 (ISBN 9781450312042)
  • (en) Nicolas Palix, Gaël Thomas, Suman Saha, Christophe Calvès, Julia Lawall et Gilles Muller, « Faults in linux: ten years later », ACM SIGPLAN Notices, vol. 46, no 3,‎ , p. 305-318 (ISSN 1558-1160, DOI 10.1145/1961296.1950401)

Les autres outils de transformation de programmes

[modifier | modifier le code]
  • (en) Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk et Yanjin Zhu, « Automatic verification of active device drivers », ACM SIGOPS Operating Systems Review, vol. 48, no 1,‎ , p. 106-118 (ISSN 0163-5980, DOI 10.1145/2626401.2626424)
  • (en) Jörg Liebig, Andreas Janker, Florian Garbe, Sven Apel et Christian Lengauer, « Morpheus: variability-aware refactoring in the wild », Proceedings of the 37th International Conference on software engineering, vol. 1,‎ , p. 380-391 (ISBN 9781479919345)
  • (en) M.M Gallardo, C. Joubert, P. Merino et D. Sanán, « A model-extraction approach to verifying concurrent C programs with CADP », Science of Computer Programming, vol. 77, no 3,‎ , p. 375-392 (ISSN 0167-6423, DOI 10.1016/j.scico.2011.10.003)
  • (en) Christos Kartsaklis et Oscar Hernandez, « HERCULES/PL: the pattern language of HERCULES », Proceedings of the 1st Workshop on programming language evolution,‎ , p. 5-10 (ISBN 9781450328876, DOI 10.1145/2717124.2717127)
  • (en) Jonathan Anderson, Robert Watson, David Chisnall, Khilan Gudka, Ilias Marinos et Brooks Davis, « TESLA: temporally enhanced system logic assertions », Proceedings of the Ninth European Conference on computer systems,‎ , p. 1-14 (ISBN 9781450327046, DOI 10.1145/2592798.2592801)
  • (en) Martin Monperrus, « Automatic Software Repair: A Bibliography », ACM Computing Surveys (CSUR), vol. 51, no 1,‎ , p. 1-24 (ISSN 1557-7341, DOI 10.1145/3105906)
  • (en) Jean-Rémy Falleri, Floréal Morandat, Xavier Blanc, Matias Martinez et Martin Monperrus, « Fine-grained and accurate source code differencing », Proceedings of the 29th ACM/IEEE international conference on automated software engineering,‎ , p. 313-324 (ISBN 9781450330138, DOI 10.1145/2642937.2642982)
  • (en) Benjamin Benni, Sébastien Mosser, Naouel Moha et Michel Riveill, « A delta-oriented approach to support the safe reuse of black-box code rewriters », Journal Of Software-Evolution and Process, vol. 31, no 8,‎ , p. 1-18 (ISSN 2047-7473, DOI 10.1002/smr.2208)

Autres sources scientifiques

[modifier | modifier le code]
  • (en) Andreas Ziegler, Valentin Rothberg et Daniel Lohmann, « Analyzing the Impact of Feature Changes in Linux », Proceedings of the Tenth International Workshop on variability modelling of software-intensive systems,‎ , p. 25-32 (ISBN 9781450340199, DOI 10.1145/2866614.2866618)
  • (en) François Armand, Michel Gien, Gilles Maigné et Gregory Mardinian, « Shared device driver model for virtualized mobile handsets », Proceedings of the First Workshop on virtualization in mobile computing,‎ , p. 12-16 (ISBN 9781605583280, DOI 10.1145/1622103.1622104)
  • (en) Michael Abd-El-Malek, Matthew Wachs, James Cipar, Karan Sanghi, Gregory R. Ganger, Garth A. Gibson et Michael K. Reiter, « File system virtual appliances: Portable file system implementations », ACM Transactions on Storage (TOS), vol. 8, no 3,‎ , p. 1-26 (ISSN 1553-3093, DOI 10.1145/2339118.2339120)
  • (en) Kai Lu, Peng-Fei Wang, Gen Li et Xu Zhou, « Untrusted Hardware Causes Double-Fetch Problems in the I/O Memory », Journal of Computer Science and Technology, vol. 33, no 3,‎ , p. 587-602 (ISSN 1000-9000, DOI 10.1007/s11390-018-1842-3)
  • (en) Wanja Hofer, Christoph Elsner, Frank Blendinger, Wolfgang Shröder-Preikschat et Daniel Lohmann, « Toolchain-independent variant management with the Leviathan filesystem », Proceedings of the 2nd International Workshop on feature-oriented software development,‎ , p. 18-24 (ISBN 9781450302081, DOI 10.1145/1868688.1868692)
  • (en) Vitaly Chipounov et George Candea, « Reverse engineering of binary device drivers with RevNIC », Proceedings of the 5th European conference on computer systems,‎ , p. 167-180 (ISBN 9781605585772, DOI 10.1145/1755913.1755932)
  • (en) Jia-Ju Bai, Yu-Ping Wang, Hu-Qiu Liu et Shi-Min Hu, « Mining and checking paired functions in device drivers using characteristic fault injection », Information and Software Technology, vol. 73,‎ , p. 122-133 (ISSN 0950-5849, DOI 10.1016/j.infsof.2016.01.018)
  • (en) Yanjie Zhen, Wei Zhang, Zhenyang Dai, Junjie Mao et Yu Chen, « Is It Possible to Automatically Port Kernel Modules? », Proceedings of the 9th Asia-Pacific Workshop on systems,‎ , p. 1-8 (ISBN 9781450360067, DOI 10.1145/3265723.3265732)
  • (en) Daniel Chavarría-Miranda, Ajay Panyala, Wenjing Ma, Adrian Prantl et Sriram Krishnamoorthy, « Global transformations for legacy parallel applications via structural analysis and rewriting », Parallel Computing, vol. 43,‎ , p. 1-26 (ISSN 0167-8191, DOI 10.1016/j.parco.2015.01.001)
  • (en) Yangyang Zhao, Hareton Leung, Yibiao Yang, Yuming Zhou et Baowen Xu, « Towards an understanding of change types in bug fixing code », Information and Software Technology, vol. 86,‎ , p. 37-53 (ISSN 0950-5849, DOI 10.1016/j.infsof.2017.02.003)
  • (en) Hua Yan, Yulei Sui, Shiping Chen et Jingling Xue, « Spatio-temporal context reduction: a pointer-analysis-based static approach for detecting use-after-free vulnerabilities », Proceedings of the 40th International Conference on software engineering,‎ , p. 327-337 (ISBN 9781450356381, DOI 10.1145/3180155.3180178)
  • (en) Hu-Qiu Liu, Yu-Ping Wang, jia-Ju Bai et Shi-Min Hu, « PF-Miner: A practical paired functions mining method for Android kernel in error paths », The Journal of Systems & Software, vol. 121,‎ , p. 234-246 (ISSN 0164-1212, DOI 10.1016/j.jss.2016.02.007)
  • (en) Yu Lu, Shen Yi et Pan Zulie, « Research on Android Vulnerability Mining Technology Based on Control Flow Analysis », 2016 Sixth International Conference on Instrumentation & Measurement, Computer, Communication and Control (IMCCC),‎ , p. 496-499 (ISBN 9781509011957, DOI 10.1109/IMCCC.2016.20)
  • (en) Laurent Burgy, Marc E. Fiuczynski, Marco Yuen et Robert Grimm, « On reconciling patches and aspects », Proceedings of the 8th workshop on aspects, components, and patterns for infrastructure software,‎ , p. 1-6 (ISBN 9781605584508, DOI 10.1145/1509276.1509278)
  • (en) Paul E. McKenney, « Beyond expert-only parallel programming? », Proceedings of the 2012 ACM workshop on relaxing synchronization for multicore and manycore scalability,‎ , p. 25-32 (ISBN 9781450316323, DOI 10.1145/2414729.2414734)
  • (en) A. Chou, J. Yang, B. Chelf, S. Hallem et D. Engler, « An empirical study of operating systems errors », Operating Systems Review (ACM), vol. 35, no 5,‎ , p. 73-88 (ISSN 0163-5980, DOI 10.1145/502059.502042)
  • (en) Michael Godfrey et Qiang Tu, « Evolution in open source software: a case study », Proceedings 2000 International Conference on Software Maintenance,‎ , p. 131-142 (ISBN 0769507530, DOI 10.1109/ICSM.2000.883030)
  • (en) Shantanu Goel et Dan Duchamp, « Linux Device Driver Emulation in Mach », Proceedings of the USENIX 1996 Annual Technical Conference,‎ , p. 65-74
  • (en) François Armand, « Give a Process to your Drivers! », Proceedings of the EurOpen Autumn 1991 Conference,‎
  • (en) Jorrit N. Herder, Herbert Bos et Andrew S. Tanenbaum, « A Lightweight Method for Building Reliable Operating Systems Despite Unreliable Device Drivers », Technical Report IR-CS-018,‎
  • (en) Dawson Engler, Benjamin Chelf, Andy Chou et Seth Hallem, « Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions », Proceedings of the Fourth USENIX Symposium on Operating Systems Design and Implementation (OSDI),‎ , p. 1-16
  • (en) G.C. Necula, S. McPeak, S.P. Rahul et W. Weimer, « CIL: Intermediate language and tools for analysis and transformation of C programs », 11th International Conference on Compiler Construction, Proceedings, vol. 2304,‎ , p. 213-228 (ISSN 0302-9743)
  • (en) E. Visser, « Program transformation with Stratego/XT rules, strategies, tools, and systems in Stratego/XT 0.9 », Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, vol. 3016,‎ , p. 216-238 (ISBN 3540221190)
  • (en) Suman Jana, Yuan Kang, Samuel Roth et Baishakhi Ray, « Automatically Detecting Error Handling Bugs Using Error Specifications », Proceedings of the 25th USENIX Security Symposium,‎ , p. 345-362 (ISBN 978-1-931971-32-4)
  • (en) Udi Manber et Sun Wu, « GLIMPSE: A Tool to Search Through Entire File Systems », Proceedings of the 1994 Winter USENIX Technical Conference,‎ , p. 1-10
  • (en) Aravind Machiry, Chad Spensky, Jake Corina, Nick Stephens, Christopher Kruegel et Giovanni Vigna, « DR. CHECKER: A soundy analysis for Linux kernel drivers », USENIX Security,‎ , p. 1007-1024 (ISBN 978-1-931971-40-9)
  • (en) Fabrice Mérillon, Laurent Réveillère, Charles Consel, Renaud Marlet et Gilles Muller, « Devil : An IDL for Hardware Programming », Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, vol. 4, no 2,‎
  • (en) Matthew J. Renzelmann, Asim Kadav et Michael M. Swift, « Symdrive: Testing drivers without devices », 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’12), vol. 4, no 2,‎ , p. 279-292 (ISBN 978-1-931971-96-6)
  • (en) Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij et Gernot Heiser, « Improved device driver reliability through hardware verification reuse », ACM SIGARCH Computer Architecture News, vol. 47, no 4,‎ , p. 133 (ISSN 0163-5964, DOI 10.1145/1961295.1950383)
  • (en) Michael Swift, Muthukaruppan Annamalai, Brian Bershad et Henry Levy, « Recovering device drivers », ACM Transactions on Computer Systems (TOCS), vol. 24, no 4,‎ , p. 333-360 (ISSN 1557-7333, DOI 10.1145/1189256.1189257)
  • (en) Michael R. A. Huth et Mark D. Ryan, « Logic in Computer Science: Modelling and reasoning about systems », Cambridge University Press,‎ , p. 1-3 (ISBN 0521652006)

Liens externes

[modifier | modifier le code]