TousAntiCovid Verif : vulnérabilité et développement défensif

L’application TousAntiCovid Verif sur Android nous a récemment régalé d’une vulnérabilité permettant d’afficher comme valides des pass sanitaires au format 2D-DOC manifestement invalides. Le bug n’intervient pas dans la vérification cryptographique de l’authenticité du pass sanitaire. Il se situe dans le reste du code métier qui vérifie la validité du pass, ne se déclenche que si l’appareil faisant tourner TousAntiCovid Verif utilise la locale anglaise.

Une vidéo de démonstration a été publiée par l’auteur de cet article. La démonstration a été effectuée avec la version 1.6.1 de TousAntiCovid Verif. La version 1.6.2 publiée le 4 août n’a pas corrigé la vulnérabilité.

Cet article propose d’étudier le bug, ses causes, et comment se protéger de tels bugs lorsqu’on pratique le développement défensif.

La vulnérabilité

Comme le code source de TousAntiCovid Verif n’a été publié que très tardivement, et que la vulnérabilité était présente dès cette publication initiale, il n’est pas possible de déterminer la date d’introduction du bug. En outre, tous les commits étant fusionné sous un unique commit à l’intitulé laconique “initial commit”, il n’est pas possible de faire une revue de code des changements dans le détail et de déterminer si l’auteur de ce bug a également commis d’autres impairs dans le code source de l’application. Bref, nous avons affaire à une parodie de code en sources ouvertes.

Toujours est-il que l’excellent @Gilbsgilbs a détecté, puis identifié la vulnérabilité. Elle se situe à aux lignes suivantes :

(oui, parce que non contents de faire un bug, ils font des copier-coller du bug pour être sûrs de l’avoir dans plusieurs branches de code…)

Au niveau le plus basique de l’analyse, le hic se situe sur le fait que status, en anglais, ne vaut pas Not Valid mais Invalid.

Cette variable est assignée ici : https://gitlab.inria.fr/tousanticovid-verif/tousanticovid-verif-android/-/blob/master/app/src/main/java/com/ingroupe/verify/anticovid/ui/result/ResultScanPresenterImpl.kt#L590

La valeur assignée à cette variable est, elle-même, assignée ici : https://gitlab.inria.fr/tousanticovid-verif/tousanticovid-verif-android/-/blob/master/app/src/main/java/com/ingroupe/verify/anticovid/service/document/StaticDataService.kt#L68

On peut noter que la valeur est issue d’un fichier de traduction : en français ou en anglais.

Le niveau zéro de la correction de cette vulnérabilité serait donc de remplacer Not Valid par Invalid… Mais il y a bien plus d’enseignements à tirer de cette erreur criante. Le reste de cet article s’attache à expliquer les stratégies de développement défensif visant à prévenir de ce genre de bugs.

Tester

Le code de TousAntiCovid Verif ne semble manifestement pas faire l’objet de tests unitaires (à l’exception de trois fichiers). Plusieurs indices le laissent penser. D’une part, il n’y a aucune trace de ces tests dans le dépôt de code source. Pour autant, on trouve des fichiers qui sont peu pertinents comme les fichiers de proguard pour rendre le code compilé moins facilement lisible par rétro-ingénierie. Cela pourrait donc laisser à penser qu’ils ont commité tout ce qu’ils avaient (à l’exception des fichiers exclus par .gitignore, et qui ne font pas mention des tests unitaires).

Ensuite, on peut voir que le code fautif était déjà présent dans le commit initial tandis que le fichier de langue contenant la chaine de caractères a été introduit dans un commit ultérieur. Il est donc probable que le code a été poussé en production, sans même avoir de fichier de langue de test pour vérifier que le code soit fonctionnel.

La première stratégie de développement défensif, qui constitue une bonne pratique standard de l’industrie, est de tester son code.

Utiliser les bons types (booléens) et les bonnes variables

Le code fautif effectue des comparaisons de chaines de caractères pour déterminer le statut de validité de la vérification cryptographique. La comparaison de chaines de caractère est fragile, en cela qu’elle repose sur la comparaison de nombreux octets qui doivent être tous justes pour que le test réussisse. À l’inverse, la comparaison d’une valeur booléenne ou même numérique (nulle ou non nulle, par exemple), aurait permis de discriminer de manière bien moins ambiguë et surtout moins susceptible à des erreurs comme celle vu dans TousAntiCovid Verif.

Le plus navrant avec TousAntiCovid Verif, c’est qu’il y a dans la même structure que celle dont est extraite cette chaine de caractères, un attribut isValid de type booléen et qui aurait pu être avantageusement utilisé pour ce test. C’est à se demander s’il y a eu une revue de code !

Utiliser des symboles plutôt que des littéraux

Comme discuté dans le point précédent, les chaines de caractères sont souvent des ennemis du code rigoureux. En effet, leur usage est bien souvent la cause de bugs lorsqu’elles contiennent de manière aléatoire des coquilles. Il est donc généralement considéré que leur usage sous la forme de valeurs hardcodées est une mauvaise pratique de développement. Il est généralement préférable d’utiliser des symboles de langages, comme des constantes nommées ou des symboles. L’usage de symboles présente l’avantage qu’en cas de coquille dans le nom du symbole : une erreur sera levée au moment de la compilation ou de l’interprétation, suivant le langage, et la coquille ne se traduira pas par une erreur de logique métier. Même Javascript, qui est un langage très souple, a un mode strict pour forcer la déclaration des variables, ce qui permet de détecter des coquilles dans les noms des variables.

Utiliser l’approche liste autorisée (“blanche”), plutôt que liste interdite (“noire”)

L’approche utilisée par le code fautif de TousAntiCovid Verif est celle de la liste interdite. En effet, le test vérifie que le status de validité du pass est “Non valide”. Si ce test échoue, alors le statut du pass est réputé valide. Cette approche a montré ses limites en de multiples occasions lors du développement d’applications sécurisées, car il est en général bien plus difficile d’envisager l’infinité des valeurs susceptibles d’être invalides, alors que les valeurs valides sont bien souvent en quantité très limitée.

Une manière de programmer de manière défensive le test fautif aurait été d’inverser sa nature : plutôt que de tester si le statut du pass est “Non valide”, il aurait été préférable de tester s’il n’était pas “Valide”. Ainsi, en cas d’oubli, de coquille, ou de toute autre raison inattendue, le résultat de la validation aurait été un échec et non un succès.

Émuler le pattern matching complet

Une méthode employée par des langages très rigoureux pour prévenir ce genre de bugs est également de proposer des instructions de contrôles exhaustives.

Par exemple, en Caml ou en Rust (parmi tant d’autres ; je ne fais que citer ceux que j’ai pratiqués), il existe du pattern matching dont l’exhaustivité des cas est vérifiée à la compilation. Si vous ne connaissez pas ce mécanisme, imaginez une sorte d’instruction switch qui refuse de compiler si tous les case possibles n’ont pas été énumérés.

Typiquement, ici, il aurait pu être pertinent d’utiliser une telle instruction de contrôle pour énumérer de façon exhaustive les cas “Valide”, “Non valide”, “Valid” et “Invalid” à l’exclusion de tout autre, sauf à encourir une erreur de compilation.

Même quand le langage ne dispose pas de telles instructions de pattern matching (ou même de switch !), il est possible de l’émuler.

Par exemple, en Python :

  if status in ["Non valide", "Invalid"]:
    handle_invalid_case()
  else if status in ["Valide", "Valid"]:
    handle_valid_case()
  else:
    raise NotImplementedError()

Employer les design patterns lorsqu’ils sont pertinents

Finalement, on peut noter que les développeurs de TousAntiCovid Verif n’ont absolument pas respecté les patrons de conception (“design patterns”) pourtant standard dans l’industrie. Je pense notamment à Model View Controler (MVC), introduit dans les années 80. En effet, les développeurs de TousAntiCovid Verif ont initialisé l’attribut status de type string de la structure DocumentSignatureResult avec le résultat d’une interrogation du module d’internationalisation. Cette initialisation est faite dès l’acquisition du code-barre 2D-DOC. Il s’agit donc d’une violation du patron MVC qui réserve l’affichage (éventuellement internationalisé) à la View, alors que l’initialisation du résultat de l’acquisition du code barre est clairement du code métier, devant être développé dans le Model.

Il est de bon aloi pour tout développeur, débutant ou moins débutant de se familiariser avec les patrons de conception classiques. Il est notamment chaudement recommandé de lire “Design Patterns: Elements of Reusable Object-Oriented Software”.

Conclusion

L’application TousAntiCovid Verif présente de nombreux signes d’une application développée sans respect des bonnes pratiques et des standards de l’industrie. L’absence de tests unitaires, et le manque de vigilance lors des revues de code (s’il y en a eu), indiquent également une très faible qualité code. Il est également permis de douter qu’un tel code ait été validé par l’ANSSI ou ait même subi un audit externe indépendant.

Compte tenu de la criticité de cette application dans la stratégie gouvernementale de déploiement universalisé du pass sanitaire comme panacée contre la COVID-19, et son installation sur les téléphones de centaines de milliers de citoyens/contrôleurs, il est regrettable de constater la faible qualité de son développement et l’incompétence manifeste de ses développeurs.