Coccinelle (logiciel)

Coccinelle
Date de première version	3 octobre 2010 (coccinelle-0.1)
Développeur	Equipe Whisper
Dernière version	1.0.8 (le 25 septembre 2019)
Écrit en	Langage C, OCaml et Python
Licence	GPLv2
Site web	coccinelle.lip6.fr

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 (É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

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. 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. Coccinelle a aussi été largement utilisé pour trouver et fixer des bugs. 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.

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.

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.

• 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.

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. 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.

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.

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. 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.

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é.

Origines du projet Coccinelle

Dans les systèmes d’exploitation (OS) modernes, les pilotes des périphériques peuvent constituer 70% du code source. 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.

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. 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.

Les évolutions collatérales

Le problème des évolutions collatérales

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é. 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. 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.

Les divers aspects du processus des évolutions collatérales

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.

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.

Les précédentes tentatives de résolution

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 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 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, 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é.

Semantic patches (SmPL)

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

Les buts de ce nouveau langage

La communauté Linux utilise divers outils pour mieux analyser le langage C. Sparse 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 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. 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.

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.

Syntaxe de SmPL

En général, le patch sémantique a la forme d'un patch traditionnel, 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.

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.

Exemple d’autres structures de transformation de programmes

D’autres structures de transformation de programme ont été proposées, s’appuyant sur des langages comme C et Java. CIL (en) et XTC 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. 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.

Évolutions de l'outil Coccinelle

Introduction des langages de script

L'interface de langage de script a été initialement motivée dans le but d'utiliser Coccinelle pour trouver des bugs. 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), 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.

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

OpenSSL

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 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.

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, 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.

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.

CERT C Secure Coding Standard

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.

Recherche de vulnérabilités sur Android

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.

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

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 .

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

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, 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.

Impact sur Linux

Augmentation des commits Coccinelle

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. 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.

Catégories d'utilisateurs

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 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.

Bibliographie

Recherches sur l’outil Coccinelle

• (en) Yoann Padioleau, Julia Lawall et Gilles Muller, « Understanding collateral evolution in Linux device drivers », ACM SIGOPS Operating Systems Review, vol. 40, n^o 4,‎ octobre 2006, 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),‎ août 2018, 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,‎ avril 2014, 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),‎ septembre 2015, 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,‎ avril 2010, 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,‎ avril 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,‎ juin 2009, 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, n^o 1,‎ janvier 2013, 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,‎ janvier 2009, 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, n^o 3,‎ juillet 2006, p. 90-92 (ISSN 0163-5980, DOI 10.1145/1151374.1151392)

• (en) Nicolas Palix, Gaël Thomas, Suman Sasha, Christophe Calvès, Gilles Muller et Julia Lawall, « Faults in Linux 2.6 », ACM Transactions on Computer Systems (TOCS), vol. 32, n^o 2,‎ juin 2014, p. 1-40 (ISSN 1557-7333, DOI 10.1145/2619090)

• (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,‎ mars 2009, 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,‎ octobre 2007, 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,‎ octobre 2006, 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,‎ mars 2010, p. 169-180 (ISBN 9781605589589, DOI 10.1145/1739230.1739250)

• (en) Yoann Padioleau, Julia Lawall et Gilles Muller, « SmPL: A Domain-Specific Language for Specifying Collateral Evolutions in Linux Device Drivers », Electronic Notes in Theoretical Computer Science, vol. 166,‎ janvier 2007, p. 47-62 (ISSN 1571-0661, DOI 10.1016/j.entcs.2006.07.022)

• (en) Suman Saha, Julia Lawall et Gilles Muller, « Finding resource-release omission faults in Linux », ACM SIGOPS Operating Systems Review, vol. 45, n^o 3,‎ janvier 2012, 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,‎ novembre 2013, 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,‎ septembre 2010, 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, n^o 1,‎ mai 2014, p. 3-41 (ISSN 1573-7535, DOI 10.1007/s10515-014-0152-4)

• (en) Jesper Andersen et Julia Lawall, « Generic patch inference », Automated Software Engineering, vol. 17, n^o 2,‎ février 2010, p. 119-148 (ISSN 1573-7535, DOI 10.1007/s10515-010-0062-z)

• (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,‎ octobre 2014, 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,‎ octobre 2010, 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,‎ septembre 2012, 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, n^o 3,‎ mars 2011, p. 305-318 (ISSN 1558-1160, DOI 10.1145/1961296.1950401)

Les autres outils de transformation de programmes

• (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, n^o 1,‎ mai 2014, 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,‎ mai 2015, 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, n^o 3,‎ mars 2012, 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,‎ juillet 2014, 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,‎ avril 2014, p. 1-14 (ISBN 9781450327046, DOI 10.1145/2592798.2592801)

• (en) Martin Monperrus, « Automatic Software Repair: A Bibliography », ACM Computing Surveys (CSUR), vol. 51, n^o 1,‎ avril 2018, 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,‎ septembre 2014, 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, n^o 8,‎ août 2019, p. 1-18 (ISSN 2047-7473, DOI 10.1002/smr.2208)

Autres sources scientifiques

• (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,‎ janvier 2016, 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,‎ juin 2008, 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, n^o 3,‎ septembre 2012, 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, n^o 3,‎ mai 2018, 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,‎ octobre 2010, 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,‎ avril 2010, 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,‎ mai 2016, 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,‎ août 2018, 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,‎ mars 2015, 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,‎ juin 2017, 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,‎ mai 2018, 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,‎ novembre 2016, 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),‎ juillet 2016, 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,‎ mars 2009, 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,‎ octobre 2012, 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, n^o 5,‎ décembre 2001, 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,‎ octobre 2000, 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,‎ janvier 1996, p. 65-74

• (en) François Armand, « Give a Process to your Drivers! », Proceedings of the EurOpen Autumn 1991 Conference,‎ septembre 1991

• (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,‎ janvier 2006

• (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),‎ octobre 2000, 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,‎ avril 2002, 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,‎ mars 2003, 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,‎ août 2016, 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,‎ janvier 1994, 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,‎ mai 2017, 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, n^o 2,‎ octobre 2000

• (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, n^o 2,‎ octobre 2012, 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, n^o 4,‎ mars 2011, 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, n^o 4,‎ novembre 2006, 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,‎ janvier 2001, p. 1-3 (ISBN 0521652006)

Liens externes

• (en) « Source code of the Coccinelle project » (consulté le 9 janvier 2019)

• (en) « Coccinelle: A program Matching and Transformation Tool for Systems Code » (consulté le 28 décembre 2019)

• (en) Julia Lawall, « Introduction to Coccinelle and its Usage in the Linux Kernel », Conférence MiNET: Les systèmes d'exploitation, mai 2018 (consulté le 28 décembre 2019)

• (en) « Équipe : Whisper - Well Honed Infracstructure Software for Programming Environments and Runtimes » (consulté le 7 janvier 2019)

• (en) Doc Searls, « Sparse, Linus & the Lunatics », novembre 2003 (consulté le 10 janvier 2019)

• (en) « Smatch -- The Source Matcher », juin 2002 (consulté le 10 janvier 2019)

• (en) D. MacKenzie, P. Eggert et R. Stallman, « Comparing and Merging Files With Gnu Diff and Patch », janvier 2003 (consulté le 10 janvier 2019)

• (en) F. Pottier et Y. Régis-Gianas, « Menhir reference manual », septembre 2019

• (en) Savia Lobo, « Linux use-after-free vulnerability found in Linux 2.6 through 4.20.11 », février 2019

• (en) S. Rievers, « Finding Bugs in Open-Source Software using coccinelle », août 2009, p. 4

• (en) « ID Utils », février 2012

• (en) « SLOCCount »

• (en) « Outreachy »