Le pouvoir des dix règles pour le développement de codes critiques pour la sécurité

Par Gerard J. Holzmann du Laboratoire pour les logiciels fiables NASA/JPL

Le pouvoir des dix règles pour le développement de codes critiques pour la sécurité, par Gerard J. Holzmann du Laboratoire pour les logiciels fiables NASA/JPL

Le Pouvoir des Dix - Règles pour le développement de codes critiques pour la sécurité

La plupart des projets sérieux de développement de logiciels utilisent des règles de codage. Ces lignes directrices sont censées énoncer les règles de base du logiciel à écrire : comment il doit être structuré et quelles caractéristiques du langage doivent ou ne doivent pas être utilisées. Curieusement, il n'y a guère de consensus sur ce qu'est une bonne norme de codage. Parmi les nombreux documents qui ont été rédigés, il y a peu de modèles remarquables à discerner, si ce n'est que chaque nouveau document a tendance à être plus long que le précédent. Il en résulte que la plupart des lignes directrices existantes contiennent plus d'une centaine de règles, dont la justification est parfois discutable. Certaines règles, en particulier celles qui tentent de stipuler l'utilisation d'espaces blancs dans les programmes, peuvent avoir été introduites par préférence personnelle ; d'autres sont destinées à prévenir des types d'erreurs très spécifiques et improbables provenant d'efforts de codage antérieurs au sein de la même organisation. Il n'est pas surprenant que les directives de codage existantes aient tendance à avoir peu d'effet sur ce que font réellement les développeurs lorsqu'ils écrivent du code. L'aspect le plus inquiétant de bon nombre de ces lignes directrices est qu'elles ne permettent que rarement des contrôles de conformité complets à l'aide d'outils. Ces contrôles sont importants, car il est souvent impossible d'examiner manuellement les centaines de milliers de lignes de code écrites pour les grandes applications.

Les avantages des directives de codage existantes sont donc souvent limités, même pour les applications critiques. Un ensemble vérifiable de règles de codage bien choisies pourrait cependant rendre les composants logiciels critiques plus analysables, pour des propriétés qui vont au-delà du respect de l'ensemble de règles lui-même. Pour être efficace, cependant, l'ensemble de règles doit être restreint et suffisamment clair pour être facilement compris et mémorisé. Les règles devront être suffisamment précises pour pouvoir être vérifiées mécaniquement. Pour fixer facilement une limite supérieure au nombre de règles nécessaires à l'élaboration d'une ligne directrice efficace, je dirai qu'il est possible d'obtenir des avantages significatifs en se limitant à dix règles au maximum. Un ensemble aussi restreint ne peut évidemment pas être exhaustif, mais il peut nous permettre d'obtenir des effets mesurables sur la fiabilité et la vérifiabilité des logiciels. Pour soutenir une vérification rigoureuse, les règles sont quelque peu strictes - on pourrait même dire draconiennes. Le compromis, cependant, devrait être clair. Lorsque cela compte vraiment, en particulier lors du développement de codes critiques pour la sécurité, cela peut valoir la peine de faire un effort supplémentaire et de vivre dans des limites plus strictes que ce qui est souhaitable. En retour, nous devrions être en mesure de démontrer de manière plus convaincante que les logiciels critiques fonctionneront comme prévu.

Dix règles pour le codage critique pour la sécurité

Le choix du langage pour un code de sécurité critique est en soi une considération essentielle, mais nous n'en débattrons pas beaucoup ici. Dans de nombreuses organisations, y compris au JPL, le code critique est écrit en C. Grâce à sa longue histoire, ce langage bénéficie d'un vaste support d'outils, notamment de puissants analyseurs de code source, d'extracteurs de modèles logiques, d'outils de mesure, de débogueurs, d'outils d'aide aux tests et d'un choix de compilateurs matures et stables. C'est pourquoi le langage C est également la cible de la majorité des directives de codage qui ont été élaborées. Pour des raisons assez pragmatiques, nos règles de codage ciblent donc principalement le C et tentent d'optimiser notre capacité à vérifier de manière plus approfondie la fiabilité des applications critiques écrites en C.

Les règles suivantes peuvent être utiles, surtout si leur faible nombre signifie que les développeurs les respecteront effectivement. Chaque règle est suivie d'une brève justification de son inclusion.

1. Règle : Limiter tout le code à des constructions de flux de contrôle très simples - ne pas utiliser d'instructions goto, de constructions setjmp ou longjmp, ni de récursion directe ou indirecte.
   
   Justification : Un flux de contrôle plus simple se traduit par de meilleures capacités de vérification et améliore souvent la clarté du code. Le bannissement de la récursivité est peut-être la plus grande surprise. Sans récursion, cependant, nous sommes assurés d'avoir un graphe d'appels de fonctions acyclique, qui peut être exploité par les analyseurs de code, et peut directement aider à prouver que toutes les exécutions qui devraient être bornées le sont en fait. (Il convient de noter que cette règle n'exige pas que toutes les fonctions aient un seul point de retour, même si cela simplifie souvent le flux de contrôle. Il y a suffisamment de cas, cependant, où un retour d'erreur précoce est la solution la plus simple).
2. Règle : Toutes les boucles doivent avoir une limite supérieure fixe. Il doit être trivialement possible pour un outil de vérification de prouver statiquement qu'une limite supérieure prédéfinie sur le nombre d'itérations d'une boucle ne peut pas être dépassée. Si la limite de la boucle ne peut être prouvée statiquement, la règle est considérée comme violée.
   
   Justification : l'absence de récursivité et la présence de limites de boucle empêchent l'emballement du code. Cette règle ne s'applique évidemment pas aux itérations qui sont censées ne pas se terminer (par exemple, dans un planificateur de processus). Dans ces cas particuliers, la règle inverse est appliquée : il doit être possible de prouver statiquement que l'itération ne peut pas se terminer. Une façon de soutenir cette règle est d'ajouter une borne supérieure explicite à toutes les boucles qui ont un nombre variable d'itérations (par exemple, le code qui parcourt une liste chaînée). Lorsque la borne supérieure est dépassée, une assertion d'échec est déclenchée et la fonction contenant l'itération défaillante renvoie une erreur. (Voir la règle 5 sur l'utilisation des assertions).
3. Règle : Ne pas utiliser l'allocation dynamique de la mémoire après l'initialisation.
   
   Justification : Cette règle est courante pour les logiciels critiques en termes de sécurité et figure dans la plupart des directives de codage. La raison en est simple : les allocateurs de mémoire, tels que malloc, et les ramasses-miettes ont souvent un comportement imprévisible qui peut avoir un impact significatif sur les performances. Une catégorie notable d'erreurs de codage provient également d'une mauvaise manipulation des routines d'allocation et de libération de la mémoire : oubli de libérer la mémoire ou poursuite de l'utilisation de la mémoire après qu'elle a été libérée, tentative d'allouer plus de mémoire que celle physiquement disponible, dépassement des limites de la mémoire allouée, etc. Le fait de forcer toutes les applications à vivre dans une zone de mémoire fixe, pré-allouée, peut éliminer bon nombre de ces problèmes et faciliter la vérification de l'utilisation de la mémoire. Notez que la seule façon de réclamer dynamiquement de la mémoire en l'absence d'allocation de mémoire à partir du tas est d'utiliser la mémoire de la pile. En l'absence de récursivité (règle 1), une limite supérieure sur l'utilisation de la mémoire de pile peut être dérivée statiquement, ce qui permet de prouver qu'une application vivra toujours dans les limites de sa mémoire pré-allouée.
4. Règle : Aucune fonction ne doit être plus longue que ce qui peut être imprimé sur une seule feuille de papier dans un format de référence standard avec une ligne par instruction et une ligne par déclaration. En règle générale, cela signifie qu'il ne faut pas dépasser 60 lignes de code par fonction.
   
   Justification : Chaque fonction doit être une unité logique dans le code, compréhensible et vérifiable en tant qu'unité. Il est beaucoup plus difficile de comprendre une unité logique qui s'étend sur plusieurs écrans d'un ordinateur ou sur plusieurs pages lorsqu'elle est imprimée. Des fonctions excessivement longues sont souvent le signe d'un code mal structuré.
5. Règle : La densité d'assertions du code doit être au minimum de deux assertions par fonction. Les assertions sont utilisées pour vérifier des conditions anormales qui ne devraient jamais se produire dans des exécutions réelles. Les assertions doivent toujours être exemptes d'effets secondaires et doivent être définies comme des tests booléens. Lorsqu'une assertion échoue, une action de récupération explicite doit être entreprise, par exemple en renvoyant une condition d'erreur à l'appelant de la fonction qui exécute l'assertion défaillante. Toute assertion pour laquelle un outil de vérification statique peut prouver qu'elle ne peut jamais échouer ou se maintenir viole cette règle. (Il n'est pas possible de satisfaire à cette règle en ajoutant des déclarations « assert(true) » peu utiles).
   
   Justification : les statistiques relatives aux efforts de codage industriel indiquent que les tests unitaires trouvent souvent au moins un défaut pour 10 à 100 lignes de code écrites. Les chances d'intercepter des défauts augmentent avec la densité des assertions. L'utilisation d'assertions est souvent recommandée dans le cadre d'une stratégie de codage défensive solide. Les assertions peuvent être utilisées pour vérifier les conditions préalables et postérieures des fonctions, les valeurs des paramètres, les valeurs de retour des fonctions et les invariants de boucle. Les assertions n'ayant pas d'effets secondaires, elles peuvent être désactivées de manière sélective après avoir été testées dans un code dont les performances sont critiques.
   
   Une utilisation typique d'une assertion serait la suivante :
   
   

   Code :

   Sélectionner tout

   1
   2
   3
   if (!c_assert(p >= 0) == true) {
    return ERROR;
    }

   
   
   avec l'assertion définie comme suit :
   
   

   Code :

   Sélectionner tout

   1
   2
   3
   #define c_assert(e) ((e) ? (true) : \
    tst_debugging(”%s,%d: assertion ’%s’ failed\n”, \
    __FILE__, __LINE__, #e), false)

   
   
   Dans cette définition, __FILE__ et __LINE__ sont prédéfinis par le préprocesseur de macros pour produire le nom de fichier et le numéro de ligne de l'assertion défaillante. La syntaxe #e transforme la condition d'assertion e en une chaîne de caractères qui est imprimée dans le cadre du message d'erreur. Dans le code destiné à un processeur embarqué, il n'y a bien sûr aucun endroit pour imprimer le message d'erreur lui-même - dans ce cas, l'appel à tst_debugging est transformé en un no-op, et l'assertion se transforme en un test booléen pur qui permet la récupération d'erreurs à partir d'un comportement anormal.
6. Règle : Les objets de données doivent être déclarés au plus petit niveau de portée possible.
   
   Justification : Cette règle soutient un principe fondamental de dissimulation des données. Il est clair que si un objet n'est pas dans la portée, sa valeur ne peut pas être référencée ou corrompue. De même, si une valeur erronée d'un objet doit être diagnostiquée, moins il y a de déclarations où la valeur aurait pu être attribuée, plus il est facile de diagnostiquer le problème. La règle décourage la réutilisation de variables à des fins multiples et incompatibles, ce qui peut compliquer le diagnostic des erreurs.
7. Règle : La valeur de retour des fonctions non vides doit être vérifiée par chaque fonction appelante, et la validité des paramètres doit être vérifiée à l'intérieur de chaque fonction.
   
   Justification : Il s'agit probablement de la règle la plus fréquemment violée, et donc Un peu plus suspecte en tant que règle générale. Dans sa forme la plus stricte, cette règle signifie que même la valeur de retour des instructions printf et des instructions de fermeture de fichier doit être vérifiée. On peut cependant considérer que si la réponse à une erreur n'est pas différente de la réponse à un succès, il n'y a pas lieu de vérifier explicitement la valeur de retour. C'est souvent le cas avec les appels à printf et close. Dans de tels cas, il peut être acceptable de transformer explicitement la valeur de retour de la fonction en (void) - indiquant ainsi que le programmeur a explicitement et non accidentellement décidé d'ignorer une valeur de retour. Dans les cas plus douteux, un commentaire doit être présent pour expliquer pourquoi une valeur de retour n'est pas pertinente. Dans la plupart des cas, cependant, la valeur de retour d'une fonction ne doit pas être ignorée, en particulier si les valeurs de retour d'erreur doivent être propagées dans la chaîne d'appel de la fonction. Les bibliothèques standard enfreignent souvent cette règle, avec des conséquences potentiellement graves. Voyez, par exemple, ce qui se passe si vous exécutez accidentellement strlen(0) ou strcat(s1, s2, -1) avec la bibliothèque standard de chaînes de caractères C - ce n'est pas beau à voir. En conservant la règle générale, nous nous assurons que les exceptions doivent être justifiées et que des vérificateurs mécaniques signalent les violations. Souvent, il sera plus facile de se conformer à la règle que d'expliquer pourquoi la non-conformité pourrait être acceptable.
8. Règle : L'utilisation du préprocesseur doit être limitée à l'inclusion de fichiers d'en-tête et à de simples définitions de macros. Le collage de jetons, les listes d'arguments variables (ellipses) et les appels récursifs de macros ne sont pas autorisés. Toutes les macros doivent se développer en unités syntaxiques complètes. L'utilisation de directives de compilation conditionnelle est souvent douteuse, mais ne peut pas toujours être évitée. Cela signifie qu'il devrait rarement y avoir une justification pour plus d'une ou deux directives de compilation conditionnelle, même dans les grands efforts de développement de logiciels, au-delà du modèle standard qui évite l'inclusion multiple du même fichier d'en-tête. Chaque utilisation de ce type doit être signalée par un outil de vérification et justifiée dans le code.
   
   Justification : Le préprocesseur C est un puissant outil d'obscurcissement qui peut détruire la clarté du code et déconcerter de nombreux vérificateurs basés sur le texte. L'effet des constructions dans un code préprocesseur non restreint peut être extrêmement difficile à déchiffrer, même avec une définition formelle du langage en main. Dans une nouvelle implémentation du préprocesseur C, les développeurs doivent souvent recourir à des implémentations antérieures pour interpréter le langage de définition complexe de la norme C. La justification de la mise en garde contre la compilation conditionnelle est tout aussi importante. Notez qu'avec seulement dix directives de compilation conditionnelle, il pourrait y avoir jusqu'à 2¹⁰ versions possibles du code, chacune d'entre elles devant être testée, ce qui entraînerait une augmentation considérable de l'effort de test requis.
9. Règle : L'utilisation de pointeurs doit être limitée. Plus précisément, il n'est pas permis d'effectuer plus d'un niveau de déréférencement. Les opérations de déréférencement de pointeurs ne peuvent pas être cachées dans les définitions de macros ou dans les déclarations typedef. Les pointeurs de fonction ne sont pas autorisés.
   
   Justification : Les pointeurs sont facilement mal utilisés, même par des programmeurs expérimentés. Ils peuvent rendre difficile le suivi ou l'analyse du flux de données dans un programme, en particulier par les outils d'analyse statique. De même, les pointeurs de fonction peuvent sérieusement restreindre les types de contrôles pouvant être effectués par les analyseurs statiques et ne devraient être utilisés que si leur utilisation est fortement justifiée et si, idéalement, d'autres moyens sont fournis pour aider les contrôleurs basés sur des outils à déterminer le flux de contrôle et les hiérarchies d'appels de fonction. Par exemple, si des pointeurs de fonction sont utilisés, il peut devenir impossible pour un outil de prouver l'absence de récursivité, de sorte que d'autres garanties devraient être fournies pour compenser cette perte de capacités d'analyse.
10. Règle : Tout le code doit être compilé, dès le premier jour de développement, avec tous les avertissements du compilateur activés au niveau le plus pédant du compilateur. Tout le code doit être compilé avec ces paramètres sans aucun avertissement. Tout le code doit être vérifié quotidiennement avec au moins un, mais de préférence plus d'un, analyseur statique de code source à la pointe de la technologie et doit passer les analyses avec zéro avertissement.
    
    Justification : Il existe aujourd'hui sur le marché plusieurs analyseurs statiques de code source très efficaces, ainsi qu'un grand nombre d'outils gratuits. Il n'y a tout simplement aucune excuse pour qu'un effort de développement de logiciel n'utilise pas cette technologie facilement disponible. Elle devrait être considérée comme une pratique de routine, même pour le développement de codes non critiques. La règle du zéro avertissement s'applique même dans les cas où le compilateur ou l'analyseur statique émet un avertissement erroné : si le compilateur ou l'analyseur statique s'embrouille, le code à l'origine de l'embrouille doit être réécrit de manière à ce qu'il devienne plus trivialement valide. De nombreux développeurs ont été pris au piège en pensant qu'un avertissement était certainement invalide, avant de se rendre compte bien plus tard que le message était en fait valide pour des raisons moins évidentes. Les analyseurs statiques ont une mauvaise réputation en raison de leurs premiers prédécesseurs, tels que lint, qui produisaient principalement des messages non valides, mais ce n'est plus le cas aujourd'hui. Les meilleurs analyseurs statiques actuels sont rapides et produisent des messages sélectifs et précis. Leur utilisation ne devrait pas être négociable dans tout projet logiciel sérieux.

Les deux premières règles garantissent la création d'une structure de flux de contrôle claire et transparente, plus facile à construire, à tester et à analyser. L'absence d'allocation dynamique de mémoire, stipulée par la troisième règle, élimine une série de problèmes liés à l'allocation et à la libération de la mémoire, à l'utilisation de pointeurs errants, etc. Les quelques règles suivantes (4 à 7) sont assez largement acceptées comme normes d'un bon style de codage. Certains avantages d'autres styles de codage avancés pour les systèmes de sécurité critiques, par exemple la discipline de la « conception par contrat », se retrouvent en partie dans les règles 5 à 7.

Ces dix règles sont utilisées à titre expérimental au JPL dans l'écriture de logiciels critiques, avec des résultats encourageants. Après avoir surmonté une saine réticence initiale à vivre dans des limites aussi strictes, les développeurs constatent souvent que le respect des règles a tendance à favoriser la clarté, l'analysabilité et la sécurité du code. Les règles allègent le fardeau du développeur et du testeur qui doivent établir les propriétés clés du code (par exemple, la terminaison ou la limitation, l'utilisation sûre de la mémoire et de la pile, etc. Si les règles semblent draconiennes au premier abord, il faut garder à l'esprit qu'elles sont destinées à permettre de vérifier un code dont l'exactitude peut littéralement dépendre de votre vie : le code utilisé pour contrôler l'avion que vous pilotez, la centrale nucléaire située à quelques kilomètres de votre domicile ou le vaisseau spatial qui transporte les astronautes en orbite. Les règles agissent comme la ceinture de sécurité de votre voiture : au début, elles sont peut-être un peu inconfortables, mais après un certain temps, leur utilisation devient une seconde nature et ne pas les utiliser devient inimaginable.

Source : The Power of Ten – Rules for Developing Safety Critical Code

Et vous ?

Pensez-vous que ces règles sont crédibles ou pertinentes ?
Quel est votre avis sur le sujet ?

Voir aussi :

Le Manifeste anti-héritage : Écrire du code qui dure, par Mensur Durakovic

Retour aux éléments de base : un chemin vers des logiciels sûrs et mesurables, un rapport de la Maison Blanche sur la sécurité de la mémoire et sur la qualité de la cybersécurité