Dans le cadre de mon taf, je fais un peu de veille sur le monde de l'informatique, donc je me dis que je peux aussi en parler ici.

Et on commence par un bug, trouvé il y a quelques heures, qui affecte Firefox, et plus particulièrement le protocole HTTP/3. Si votre navigateur est configuré pour utiliser automatiquement des services en HTTP/3, le bug sera déclenché plus rapidement (par exemple DoH ou la télémétrie). Ce bug fait tourner Firefox en boucle et le rend inutilisable, y compris la partie qui s'occupe d'en faire les mises à jour automatique.

Si vous êtes affecté.e.s, le plus simple est de désactiver HTTP/3 : aller dans about:config, chercher la clé 'network.http.http3.enabled', et la mettre à False.

Bien entendu, les conséquences pour le navigateur risquent d'être gigantesques, sachant qu'il est déjà en perte de vitesse.

Source

S'il y a des gens que ça intéresse, je signale que comme on est en décembre, l'Advent of code a repris.

Voir ici

Il s'agit d'un challenge avec un défi de programmation par jour. Les problèmes sont de difficulté croissante. Généralement, des gens qui débutent peuvent faire les 10 premiers jours sans trop de difficulté (même si des astuces peuvent aider, bien sûr). Les prérequis sont par contre de savoir lire et parser un fichier ou une chaine de caractères.

Allez aujourd'hui je vous parle d'un truc que j'aime bien et qui est très niche dans la galaxie informatique : les méthodes formelles. C'est souvent considéré soit comme un truc très obscur, soit réservé à un nombre très restreint de personnes dans l'industrie, et ça a du sens.

On parle de méthodes formelles pour une manière de programmer pour laquelle on prouve que ce qu'on a programmé correspond bien à ce qu'on veut.

Ça peut sembler un peu superflu parce que "on voit bien ce qu'on écrit quand même" (et si vous faites le concours ci-dessus, par exemple, c'est à peu près clair que vous allez pas vous emmerder à prouver que ce que vous codez est correct), mais c'est bien ça le problème : quand on code, parfois on veut garantir l'absence absolue de bug, et les méthodes classiques de programmation ne permettent pas d'atteindre ça.

Pour prendre un exemple un peu neutre, imaginons que vous écriviez le programme d'un feu rouge, et détaillons les différentes étapes :

A/ Le repli

La première chose à voir, c'est que vous avez un état de repli, c'est-à-dire qu'en cas de problème, basculer vers cet état garantit la sécurité. Dans le cas de votre feu rouge, c'est juste de s'éteindre parce que le code de la route prend alors la relève et donne les priorités sur votre intersection. Avantage : cet état de repli ne nécessite pas d'alimentation électrique non plus, donc pas besoin de la garantir en sécurité. En fonction du logiciel sur lequel vous travaillez, l'état de repli est plus ou moins complexe à atteindre. Un autre exemple simple, c'est un train : l'état de repli c'est de freiner (et si vous mettez un coup de hache dans l'ordi de bord d'un train, il va effectivement se mettre à freiner). Un exemple complexe, c'est un avion : le repli c'est de se poser sur une piste d'aterrissage. Pour ça il faut garantir que les calculateurs de bord soient alimentés électriquement en permanence (pas de manœuvre manuelle possible).

B/ La conception

Quand vous allez programmer votre feu rouge, vous allez décider des cycles, des synchronisations, et des mécanismes d'action quand quelqu'un appuie sur le bouton d'appel piéton. Problème : pourquoi est-ce que ce que vous décrivez est sûr ? N'est-il pas possible que deux routes perpendiculaires aient un feu vert en même temps ? Idéalement, on voudrait à cette étape garantir l'absence d'accident de voiture si tout se passe correctement. Un bon moyen d'éviter une situation, c'est d'écrire directement dans la conception que le système doit passer en repli si une situation anormale est observée.

Ici, les méthodes formelles permettent de prouver la fiabilité d'un système, à condition de le modéliser entièrement (il faut modéliser les humains et leur fonctionnement). Dans le cas d'un feu rouge, on voudra sans doute modéliser le temps maximum que met un.e piéton.ne ou une voiture à libérer la chaussée. Dans le ferroviaire, il faut modéliser les trains, leur vitesse, les procédures que connaissent les conducteurs et les agents de postes d'aiguillages, etc.

La conception prouvée par méthodes formelles est encore à un niveau balbutiant, mais il y a des progrès importants dessus dans l'industrie.

(Je tâcherai de faire plus tard :
C/ Le développement
D/ La compilation
E/ L'exécution
F/ La validation de données)

Allez, je reprends, et ça n'a rien à voir avec le fait que je suis coincé dans un train entre Paris et Lyon…

C/ Le développement

Le développement, ça consiste à créer un logique qui correspond à une spécification donnée. Je vais prendre l'exemple d'une fonction qui trie une liste d'entiers parce que c'est un bon exemple que plein de gens savent faire de plein de manières différentes (voir ici par exemple).

La spécification dans mon exemple, c'est donc qu'on veut une fonction qui va avoir en entrée (d'une manière ou d'une autre) une liste d'entiers, et qui va sortir (d'une manière ou d'une autre) cette liste triée. Ensuite, on programme le tri qu'on veut, et enfin on s'occupe donc de prouver que le programme trie la liste. Ça ressemble à un échange du genre :

- Bonjour, je veux prouver que ce programme trie la liste [x0, ...xn-1] .
- Ok, que veut dire "trier la liste ?"
- Ça veut dire que pour tout i, liste[i] ≤ liste[i+1] sur la liste d'arrivée [#]
- Ok comment veux-tu prouver que pour tout i, liste[i] ≤ liste[i+1] ?
- Je vais commencer par dire qu'à chaque passage dans la boucle, telle nouvelle propriété est vraie (par exemple, après la i-ème passe du tri par insertion, les i premiers éléments sont triés).
- Ok comment veux-tu prouver qu'à chaque passage dans la boucle (...) ?
- Je vais montrer que c'est vrai après le premier passage.
- Après le premier passage, le début de ta liste, c'est [x0, x1, ...] ou [x1, x0, ....]. Ok donc c'est bon dans les deux cas. Supposons que ce soit vrai après le passage i. Comment passes-tu du passage i au passage i+1 ? (ici, il faudrait ajouter une autre propriété sans doute).

[#] : Petit exercice : cette spécification n'est pas du tout suffisante. Comment devrait-on la compléter ?

Une fois qu'on a fini, et que tout est prouvé, on a un tri prouvé formellement.

Au passage, ce n'est pas forcément super difficile, mais c'est très très rébarbatif à faire : il faut maitriser 3 langages (un langage pour spécifier, un langage pour implémenter, un langage pour prouver), les trois doivent interagir de manière plus ou moins complexe. Dans la pratique, je crois que c'est rarement enseigné, plutôt à niveau Bac + 5, et qu'il n'y a pas des millions de personnes qui maitrisent vraiment ces aspects.

Comme je l'avais écrit, de toute façon on fait pas ça pour des programmes sans grand enjeu : on réserve ça pour des programmes avec risques de morts ou des conséquences vraiment graves.

Pour l'anecdote, en 2014 il y avait une équipe de formel qui a travaillé sur des algorithmes de déduction formelle et qui ont essayé de prouver l'algorithme du timsort écrit en java (qui est un portage du même algorithme écrit en C pour Cpython). Ils n'ont pas réussi et ont compris pourquoi : le programme était buggé et pouvait ne pas trier des listes qui étaient vraiment très grande (trop grandes pour envisager que même un supercalculateur soit capable de les contenir). Des infos et/ou des pointeurs ici.


> D/ La compilation
> E/ L'exécution
> F/ La validation de données)

Uncurieux a écrit :



Je ne vois pas en quoi c'est insuffisant.
C'est la définition du tri non?

Je peux voir deux choses, mais ça me semble relever de la pinaillerie.
- Il faut préciser que la relation d'ordre qu'on observe est totale (et transitive?) ? Etant donné que tu utilises "≤", j'imagine que tu prends l'exemple d'une liste d'entiers, pour lequel "≤" a ces propriétés?
- Il faut préciser comment sont gérés les cas d'égalité (e.g le timsort assure que si deux éléments sont égaux, leur ordre dans la liste initiale est conservé dans la liste finale)? Mais comme il y a quand même un sous-entendu que c'est une liste d'entiers, j'ai envie de dire que deux éléments égaux sont indifférenciables, et du coup cette question n'a pas de sens ici?

Ou est-ce qu'on est encore plus loin dans la pinaillerie, à savoir que la liste d'arrivée doit avoir exactement les mêmes éléments que la liste d'arrivée, le même nombre de fois?

Ou encore plus pédant, qu'il s'agit de tout i entier tel que i est compris entre 0 (resp. 1) et n-2 (resp. n-1), où n est le nombre d'élements de la liste, et l'indice du premier élément de la liste est 0 (resp. 1) ?

K a écrit :

> C'est la définition du tri non?

Pas exactement, et typiquement dans un contexte critique c'est super important de le vérifier.

Si tu oublies de demander que la liste de sortie soit en bijection avec la liste d'entrée (ton avant-dernière proposition), alors il pourrait se passer qu'en cas de défaillance d'un composant, la liste de sortie se retrouve vide et que ton test soit validé (sur cet exemple-ci, on se doute qu'on peut l'éviter, mais il faut se souvenir que ce n'est qu'un exemple et qu'on peut imaginer des cas un peu tordus où la provocation d'un cas particulier nécessite des conditions peu probables voire peu imaginables). Ou bien simplement que tes permutations soient mal écrites et écrasent les valeurs. Là pareil, tu ne verras rien.

Note que dans ce cas, le test unitaire peut te sauver : en écrivant des cas simples, tu risques de détecter des erreurs de ce genre. Avec du formel, et en particulier si tu as un prouveur automatique, c'est bien plus inquiétant : si tu n'écris que la croissance dans ta spécification et que ton programme est faux, ce ne sera plus détecté. Bref : il faut une spécification précise et exhaustive.

> - Il faut préciser que la relation d'ordre qu'on observe est totale (et transitive?) ? Etant
> donné que tu utilises "≤", j'imagine que tu prends l'exemple d'une liste d'entiers,
> pour lequel "≤" a ces propriétés?

Oui dans le cas d'une liste d'entiers aucun problème. Pour briller en soirée, sur un tri en général, tu as besoin d'un préordre total (pas besoin de l'antisymétrie), et c'est justement quand tu n'as pas l'antisymétrie que la question suivante prend du sens :
> - Il faut préciser comment sont gérés les cas d'égalité (e.g le timsort assure que si deux
> éléments sont égaux, leur ordre dans la liste initiale est conservé dans la liste finale)?
> Mais comme il y a quand même un sous-entendu que c'est une liste d'entiers, j'ai envie de dire
> que deux éléments égaux sont indifférenciables, et du coup cette question n'a pas de sens ici?

Ceci correspond à la notion de tri stable (et effectivement le timsort est un tri stable). Je ne parlais effectivement pas de ça ici.

> Ou encore plus pédant, qu'il s'agit de tout i entier tel que i est compris entre 0 (resp. 1)
> et n-2 (resp. n-1), où n est le nombre d'élements de la liste, et l'indice du premier élément
> de la liste est 0 (resp. 1) ?

Là ce serait effectivement un peu trop pédant : j'ai raccourci "pour tout i" sans donner l'ensemble, mais le langage formel obligerait sans doute à renseigner l'ensemble (pour les méthodes formelles que je connais).

On continue :

D/ La compilation

Vous avez finalement écrit un programme sans bug. Votre objectif est maintenant de le faire tourner.

Un petit mot d'introduction ce ce qu'est la compilation. Généralement, un processeur dispose d'un jeu d'instructions assez restreint (mettre telle valeur dans tel registre, additionner des valeurs dans des registres et mettre le résultat dans un autre registre, etc.). Il est théoriquement possible de programmer un logiciel sécuritaire directement avec ces instructions, mais presque personne ne le fait pour deux raisons :
1/ c'est extrèmement désagréable de programmer en assembleur : il faut détailler chaque étape de ce qu'on veut faire et la décomposer en plein de sous-instructions. C'est un mode de pensée bien particulier, mais pour prendre un schéma, c'est comme si vous deviez écrire une recette de cuisine en décrivant quels muscles la personne qui cuisine doit contracter plutôt qu'en utilisant un verbe générique (genre "mélanger").
2/ comme avec ma comparaison précédente, impossible d'écrire quelque chose de très générique : les processeurs n'ont pas tous les mêmes jeux d'instructions (et quand on parle d'informatique sécuritaire, souvent on parle de matériel bien spécifique). Si vous programmez en assembleur, le jour où vous changez de carte électronique il faut reprendre le travail, et si les différences sont un peu importantes, ça signifie tout refaire depuis le début.

Bref : en pratique, on passe le programme dans une moulinette informatique qui va transformer le code en "binaire", qui est donc une série d'instructions à destination du processeur, et la question est donc : comment s'assurer que le code binaire correspond à ce qu'on a demandé dans le code ?

La question n'a rien de simple, et il y a des travaux assez importants qui aboutissent en ce moment, donc je ne vais qu'écorcher la surface.

Imaginons que vous écriviez un programme en C. Qu'est-ce qui définit précisément ce que fait une instruction en C ou pas ? Il y a une norme (il y en a plein en fait, la dernière date de 2024…), qui prévoit plein de cas "non définis" (ie si le compilateur détecte cette situation, il peut la convertir en ce qu'il veut ou même planter et refuser de compiler). Même dans les cas définis, il y a des situations tordues (voir par exemple ici si vous aimez ce genre de casse-têtes).

Il y a une équipe qui travaille sur ce problème depuis 2005 (et ce travail vaudra possiblement un prix Turing à l'auteur principal) et a fabriqué un compilateur sûr : CompCert. Le travail a consisté à définir une sémantique formelle sur le langage C, puis à transformer de proche en proche cette sémantique vers des langages intermédiaires jusqu'à arriver à un langage compilé sur un jeu d'instructions particulier. Chacune de ces transformations est prouvée fiable par une preuve formelle vérifiée informatiquement en coq. Le compilateur est du coup plus lent et moins optimisé qu'un compilateur évolué comme gcc, mais il garanti que le binaire fait bien la même chose que le code de départ, ou au moins que ce qu'il devrait faire dans la sémantique définie.

Alors bien sûr, si on considère qu'il s'agit d'un travail réalisé sur plus de 15 ans, avec une sacrée équipe de chercheurs, et que le langage compilé est plutôt de bas niveau, il semble difficile d'avoir demain l'équivalent pour d'autres langages et encore moins pour des langages de haut niveau (C++, Java, Python, Javascript, etc.).

Est-ce qu'hors de C tout est perdu ? Non. En terme sécuritaire, il existe au moins une autre méthode : la redondance. Si vous prenez deux compilateurs écrits de manière complètement indépendante, vous pouvez dans certains cas évaluer la probabilité qu'un bug affecte les deux compilateurs sur le même programme. En général, vous allez aussi essayer d'avoir du code à compiler plutôt simple (par exemple éviter les constructions cheloues comme dans l'exemple ci-dessus, ou plus généralement éviter toutes les allocations dynamiques). Ensuite, vous exécutez les deux programme, et s'ils ne sont pas d'accord, vous passez votre système en état de repli. Cette solution est donc plus acceptable si l'état de repli est simple à obtenir, ce n'est donc pas un hasard si Compcert intéresse beaucoup l'avionique, et pas plus que ça le ferroviaire.