patrick_g a écrit 6339 commentaires

Exemple intéressant. Mais est-ce vraiment possible de s'inspirer de ce que fait une cité-état hyper urbanisée dans ce domaine ?

Un autre post très intéressant et détaillé de Brendan sur Hacker News : https://news.ycombinator.com/item?id=16382456

Il explique pourquoi il a quitté illumos (une distribution de Solaris) alors qu'il en était un des fondateurs. Selon lui cela avait du sens en 2010 de miser sur Solaris qui, à l'époque, était en avance dans de nombreux domaines par rapport à Linux.
Depuis 2010 beaucoup d'eau a coulé sous les ponts. Solaris a stagné et Linux a énormément progressé (cf sa liste) au point que, selon lui, cela ne rime plus à rien de miser sur Solaris aujourd'hui.

Soutenez LWN

je serais curieux de savoir si cette discussion a dissipé nos différences de point de vue, ou si tu continues à ne pas être convaincu par l'idée que les assistants de preuve pourraient un jour apporter du confort à la pratique de la recherche en mathématiques.

Honnêtement je ne sais pas. Voevodsky pensait que la complexité de la recherche en géométrie algébrique était devenue telle qu'il fallait absolument changer le paradigme et utiliser ces assistants de preuve pour être certains de ne pas faire d'erreur dans les démonstrations. D'après ce que j'ai lu ses collègues ne semblent pas convaincus et ils continuent de faire leur recherche et de publier leurs démonstrations de façon classique.

Peut-être qu'il faudra attendre que ces assistants deviennent plus puissants, plus simples à utiliser et qu'ils s'appuient sur des bibliothèques bien plus complètes de résultats déjà démontrés.
Ou peut-être qu'il y aura une séparation du travail et qu'on va assister à l'émergence d'une nouvelle classe de mathématiciens. Ces nouveaux chercheurs prendront les résultats démontrés classiquement et feront le travail de vérification formelle. Un peu ce qu'à fait Gonthier avec la vérification du théorème de Feit-Thompson.
Mais ça lui a pris 6 ans, il était entouré d'une équipe de chercheurs et c'était pour prouver un théorème vieux de plus de 50 ans.
Autrement dit c'est pas gagné…

Oui le dernier exemple est tellement gros qu'il va être publié comme une monographie.
Mais je maintiens ce que j'ai dit : en math pures il se publie de très gros articles dans les journaux.
L'exemple 4 des papiers de Scholze a été publié dans Annals of Math (lien).
Regarde aussi celui-ci qui fait 121 pages, également publié dans Annals of Math.
Et pas que Annals, d'autres journaux aussi. Les Publications Mathématiques de l'IHES par exemple sont connues pour accepter de très gros papiers (l'héritage des EGA/SGA de Grothendieck ?). En allant jeter un coup d'oeil rapide je tombe sur cet article qui fait plus de 150 pages.

le chercheur écrit un article à destination d'une conférence où le nombre de pages de chaque publication est limité

Alors ça, il me semble que ces articles à destination des conférences et avec pagination imposée ça se fait plutôt dans le domaine de la recherche en informatique non ?
Ce n'est plus vrai du tout en math pures ou on voit passer des très gros articles et les journaux n'ont pas peur de publier ça (et ne semblent pas limités par la pagination).
Si je regarde sur la page de Peter Scholze (qui a 99,999% de chances de recevoir la médaille Fields cet été) je trouve ça pour les papiers postées ces deux dernières années :

Topological Hochschild homology, and integral p-adic Hodge theory => 84 pages
Étale cohomology of diamonds => 154 pages
Integral p-adic Hodge theory => 118 pages
On the generic part of the cohomology of compact unitary Shimura varieties => 98 pages

Et je ne parle même pas du multiplodocus de Fargues-Fontaine (soumis à Astérisque qui publie des monographies):

Courbes et fibrés vectoriels en théorie de Hodge p-adique => 399 pages

Une preuve formelle permet justement de ne pas avoir besoin de ça.

Une preuve formelle te donne juste un résultat binaire. Oui la démonstration est juste ou bien Non y'a une merde.
Elle ne t'explique pas l'idée clé. Elle ne te fait pas comprendre intuitivement pourquoi la démonstration fonctionne.

Ensuite, si tu veux faire référence à un résultat qui existe déjà, c'est facile d'imaginer des libraries pour ça

Bien entendu. C'est pourquoi j'avais fait référence au boulot de Voevodsky (voir ici). Mais encore une fois cela ne communique pas l'idée de la démonstration.

Aujourd’hui quand quelqu’un annonce un nouveau résultat mathématique, il peut être très difficile de savoir si le résultat est correct ou non ; il sera peut-être un jour réaliste de demander à la personne de fournir une preuve vérifiée par un assistant de preuve, pour accélérer son étude et sa compréhension par les scientifiques du domaine.

Je ne comprends pas du tout cette phrase.
Actuellement quand un résultat de math est démontré par un chercheur (la preuve du dernier théorème de Fermat par Wiles par exemple) alors le chercheur écrit un article à destination de ses collègues pour expliquer sa démonstration.
Les collègues lisent l'article, évaluent la rigueur et la pertinence des arguments et finalement portent un jugement sur la véracité de la démonstration.
Ce qu'il faut bien voir c'est que l'auteur écrit son article pour optimiser la compréhension auprès de ses collègues. Ce sont eux (les pairs) qui vont évaluer son travail.
L'article n'est pas écrit dans un langage formel évaluable par une machine. Il est écrit avec des phrases et des mots.
Certains points, considérés comme de la routine pour les spécialistes du domaine, sont abrégés ou carrément passés sous silence.
Par exemple dans de nombreux articles de géométrie arithmétique ou de géométrie algébrique on peut voir des phrases du style : "Par un argument à la GAGA il est facile de voir que blabla".
Les spécialistes comprennent immédiatement que cela fait référence à l'article ultra-connu de Jean-Pierre Serre intitulé "Géométrie algébrique et géométrie analytique".
Mais une machine ne comprendrait pas ça. Pour une machine tout doit être complètement formalisé.

Donc tout ça pour dire que ta phrase affirmant qu'une démonstration "vérifiée par un assistant de preuve accélérait son étude et sa compréhension par les scientifiques du domaine" ne tient pas debout. Cette preuve serait au contraire illisible par un humain si on la compare aux articles actuels qui, eux, sont écrits pour des humains.
La vérification formelle des démonstrations pourra sans doute être très utile pour avoir la certitude qu'il n'y a pas d'erreurs qui se sont glissés dans le raisonnement. C'était le pari de Voevodsky.
Mais il y a très peu de chance pour que, en soi, cela favorise la compréhension.

Mais ça te permet de télécharger un ePub propre sans DRM ?

Comme j'ai le Epub acheté sur le site de la Fnac et aussi le Epub téléchargé via torrent, je vais essayer de regarder les différences entre les deux.

Dans leur premier émail ils indiquent clairement que tu peux le télécharger sur le site Kobo.fr. Pourquoi ne pas l'avoir fait directement, au lieu d'insister ?

Parce qu'ils disaient explicitement que pour que ça marche il fallait préalablement installer le truc Adobe et associer l'ID. Je ne pouvais pas me douter que ce prérequis était en fait bidon.

Par curiosité comment ça marche techniquement le watermark ? De la stégano dans l'image de la couverture du livre ?

Autre test valable pour plus de distribs

Comment tu sais si tu n'as que le support minimal de retpoline (Vulnerable: Minimal generic ASM retpoline) ou bien le support complet (Mitigation: Full generic retpoline) ?

Kilo Bits, ou Kilo Bytes, du coup?

Kilo-octets. Extrait du papier sur Meltdown :

we can dump kernel and physical memory with up to 503 KB/s. Hence, an enormous number of systems are affected.

Et sur Spectre les chiffres sont plus petits mais ils disent que le code n'est pas optimisé :

The unoptimized code in Appendix A reads approximately 10KB/second on an i7 Surface Pro 3.

Première réaction officielle des devs d'OpenBSD sous la forme d'un mail de Philip Guenther sur la liste de diffusion : https://www.mail-archive.com/tech@openbsd.org/msg43791.html

Donc ça confirme ce qu'on soupçonnait déjà c'est à dire que les devs OpenBSD n'étaient pas dans le secret de l'existence de ces failles, qu'ils n'ont donc pas pu bosser sur un correctif du type KPTI (qui corrige Meltdown). Aucune solution n'est actuellement disponible sous OpenBSD et la faille Meltdown est grande ouverte :-(
Et aucune info n'est donnée dans ce post au sujet de Spectre ou d'une solution type Retpoline ou IBRS.

C'est la méga merde….

Si les devs OpenBSD, lors de la levée de l'embargo, doivent pondre en seulement quelques heures une correction ça risque d'être chaud.

Et ça se confirme : https://www.mail-archive.com/tech@openbsd.org/msg43791.html
Donc pour l'instant la faille Meltdown est béante sous OpenBSD et aucun correctif n'est disponible :-(

Sous Ubuntu 16.04 LTS… rien pour l’instant

Pour Ubuntu ils indiquent qu'ils ont été pris de cours par la divulgation avant la date prévue du 9 janvier :

https://wiki.ubuntu.com/SecurityTeam/KnowledgeBase/SpectreAndMeltdown

The original coordinated disclosure date was planned for January 9 and we have been driving toward that date to release fixes. Due to the early disclosure, we are trying to accelerate the release, but we don't yet have an earlier ETA when the updates will be released.

Pour la nouvelle version du noyau effectivement c'est déjà dispo dans les dépôts Arch.
Après une maj :

[patrick@laptop]: ~>$ uname -a
Linux laptop 4.14.11-1-ARCH #1 SMP PREEMPT Wed Jan 3 07:02:42 UTC 2018 x86_64 GNU/Linux
[patrick@laptop]: ~>$ grep "model name" /proc/cpuinfo | uniq
model name : Intel(R) Core(TM) i7-3540M CPU @ 3.00GHz
[patrick@laptop]: ~>$ grep bugs /proc/cpuinfo | uniq
bugs : cpu_insecure

Il ne semble y avoir aucune solution en vue contre Spectre

Si, si apparemment Google a des patchs sous le coude pour GCC et LLVM afin de contrer Spectre : https://support.google.com/faqs/answer/7625886

Ce sera aussi la faute du user parce qu'il n'avait qu'à acheter un Nexus ?

Je dirais que la faute est partagée. C'est un scandale que les compagnies ne mettent pas à disposition les patchs de sécurité pour leurs produits…mais le user doit également se renseigner un minimum avant d'acheter. Il y a d'innombrables articles qui informent les gens au sujet des compagnies qui maintiennent correctement leurs produits et celles qui ne font rien. Dire que le user n'y est pour rien alors qu'il achète comme un somnambule c'est un peu gros.

Faut se calmer, c'est pas bon pour ta tension cet énervement :-)

Le patch qui désactive KPTI pour les processeurs AMD a été accepté par Linus : https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=00a5ae218d57741088068799b810416ac249a9ce

Le commentaire du patch : "Exclude AMD from the PTI enforcement. Not necessarily a fix, but if AMD is so confident that they are not affected, then we should not burden users with the overhead".

En même temps c'est aussi aux utilisateurs de faire les bons choix dans leur vie numérique.
J'ai un smartphone Nexus 5X et je vais donc recevoir dans les prochains jours le correctif de janvier de Google : je serai protégé.
J'ai un laptop sous Arch et je vais donc recevoir dans les prochains jours le noyau 4.14.11 qui contient KPTI : je serai protégé.

C'est sûr que si le user a un Windows pirate qui ne reçoit aucune maj et un vieux android qui ne reçoit aucune maj ben il est dans la merde : mais c'est en grande partie la faute du user !

Pour Risc-V il y a eu un mail de Christoph Hellwig sur la liste de diffusion afin que les devs de cette architecture tiennent compte de ce besoin d'isolation : https://groups.google.com/a/groups.riscv.org/forum/#!msg/isa-dev/JU0M_vug4R0/YELX92fIBwAJ

On parle quand même d'un changement représentant 51 patchs et qui, au 18 décembre, en était à la version 163.
Autrement dit c'est pas du tout trivial.

La question du parano en suspens est: cette faille était-elle connue avant par certains gouvernements et l'ont ils utilisé?

La vraie question parano/complotiste serait de se demander si la faille n'a pas été minutieusement conçue et sciemment introduite par des ingénieurs qui seraient payés par des officines gouvernementales étasuniennes. Un canal caché permettant de trouer toutes les machines sous CPU Intel c'est le rêve absolu pour la NSA.

Il reste donc aux OS à corriger ce souci (Linux, Windows, FreeBSD, MacOS, et tous les autres).

C'est peut-là que les devs OpenBSD vont se mordre les doigts de ne pas vouloir jouer le jeu des embargos. Cela fait plus de 2 mois que les devs Linux bossent sur KAISER/KPTI car c'est un changement fondamental dans le fonctionnement du sous-système de gestion de la mémoire. Et le travail n'est pas complètement terminé.
Si les devs OpenBSD, lors de la levée de l'embargo, doivent pondre en seulement quelques heures une correction ça risque d'être chaud.