SamWang_le_retour_7 a écrit 191 commentaires

  • [^] # Re: journal -> dépêche

    Posté par . En réponse au journal Lancement du projet Open Compute Toolchain. Évalué à -7.

    Il y a une dernière petite chose à régler. Le titre actuel est :

    Lancement du projet Open Compute Toolchain

    Or, d'un côté on a ces deux informations qui tendent à invalider un tel titre :

    • le sous-groupe qui s'est constitué est nommé « Software Toolchain », faisant partie du projet Open Compute (projet dit OCP, pour « Open Compute Project ») ;
    • l'expression « Open Compute Toolchain » n'apparait pas dans l'annonce qu'a relayée vejmarie, si ce n'est sous une forme typographique légèrement différente, en tant que nom de la liste de diffusion, nommée « opencompute-toolchain ».

    De l'autre côté, on a cette information (moins pertinente) qui tend à le valider :

    En conclusion, je propose, au choix :

    a) renommer la dépêche ainsi (choix plus valide au sens strict, très grande cohérence, mais plus long et peut-être moins accrocheur) :

    Lancement de la branche « Software Toolchain » de l'Open Compute Project

    Note : j'ai choisi le mot branche plutôt que sous-groupe pour réduire la longueur du titre, rendre l'expression moins lourde, considérant que la nuance est très ténue et sans conséquence.

    b) laisser le nom de la dépêche tel qu'est le nom du journal (choix moins valide au sens strict, mais court et assez accrocheur, finalement bien compréhensible, relativement cohérent)

    Je fais le choix de a) pour le bien de la communauté (considérant que c'est le meilleur choix et qu'un modérateur pourrait valider la dépêche sans m'avoir lu préalablement), mais, évidemment, sur ce point comme sur tout autre point de cet dépêche, je ne prétends être décideur de rien en dernier ressort.

  • [^] # Re: journal -> dépêche

    Posté par . En réponse au journal Lancement du projet Open Compute Toolchain. Évalué à -9.

    Je me suis permis une dernière petite série de retouches du plus bel effet :)

    Toutes les corrections sont finalisées, toutes les expressions sont contrôlées, tous les liens sont vérifiés, les enrichissements de caractères sont rendus homogènes. La dépêche est dans un état de grande perfection.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -7.

    Ci-dessus, je n'avais pas su traduire "Golden chips".

    Un "golden chip" est une puce de référence, par exemple celle qui sert pour comparer avec celles de production de masse pour le réglage des processus de dopage. On parle aussi de "golden sample". Cela peut aussi être un "trusted sample" dans le cadre de la sécurité. Voici une source qui aborde le sujet, en anglais.

    La phrase qui comporte l'expression "golden chip" dans le résumé de l'article peut donc être traduite ainsi :

    « Puisque le circuit modifié apparaît légitime sur toutes les couches gravées (incluant métal et silicium), notre famille de chevaux de Troie est résistante à la plupart des techniques de détection, incluant l'inspection optique à une granularité fine et la vérification par rapport à des puces de référence [NdT : puces de référence dites "Golden chips", entre guillemets dans le texte, selon l'expression consacrée en anglais] ».

  • [^] # Re: journal -> dépêche

    Posté par . En réponse au journal Lancement du projet Open Compute Toolchain. Évalué à -7.

    J'ai apporté une petite correction au premier des deux paragraphes mentionnés ci-avant. J'avais écrit que la preuve formelle de conformité du code par rapport aux spécifications n'est possible que si la chaîne de compilation est réalisée en sources ouvertes.

    J'ai corrigé dans la dépêche pour remplacer « n'est possible » par « n'a de sens, en terme de confiance, », car il reste toujours possible de vanter les mérites d'un logiciel propriétaire mais la confiance dans une prétention de preuve de code ne peut venir qu'avec la capacité d'audit des sources.

  • [^] # Re: journal -> dépêche

    Posté par . En réponse au journal Lancement du projet Open Compute Toolchain. Évalué à -6.

    En plus du travail précédent aboutissant à une dépêche de qualitaÿ, je me suis permis de rajouter les 3e et 4e paragraphes en partant de la fin. Je ne sais pas si vejmarie< voudra endosser la responsabilité de ces propos (qui sont tout à fait valides, raisonnables et sourcés) dans le cadre de sa communication, étant donné sa position somme toute formelle, je suppose, au sein de OCP (« Open Compute Project » — site www.opencompute.org).

    Si les paragraphes n'étaient pas retenus, les voici déjà en avant première :


    Prenez conscience également que via ce projet — au-delà de la possibilité donnée à chacun de contribuer à la définition de matériel libre dans le cadre de OCP (ou en dehors) — s'ouvrent des perspectives d'audit renforcé des sources ainsi que de production de preuve formelle sur le code définissant le matériel libre, particulièrement la preuve formelle de conformité du code par rapport aux spécifications (ce qui n'est possible que si la chaîne de compilation est réalisée en sources ouvertes), voire d'autres preuves formelles comme la robustesse des spécifications relativement à des types d'attaques répertoriées.

    Même si d'une part des chevaux de Troie resteront intégrables par les fabricants — par exemple des portes dérobées matérielles furtives réalisées au niveau du dopage du substrat de silicium des circuits intégrés (cf. ce commentaire de Misc< référençant des résultats de recherches), incitant éventuellement la communauté à superviser la fabrication, même si d'autre part la substitution malveillante du matériel restera possible pendant la phase de distribution, incitant là aussi la communauté à organiser une forme de supervision, il est déjà acquis que la direction prise est la bonne.

  • [^] # Re: journal -> dépêche

    Posté par . En réponse au journal Lancement du projet Open Compute Toolchain. Évalué à -6.

    J'ai apporté ce que je pouvais. J'ai l'impression que c'est très bien, tel quel, prêt à être publié. Je l'écris ici car du fait de mon karma (au sens de Linuxfr), je ne peux contribuer sur aucune tribune de rédaction.

  • [^] # Re: Petit avis.

    Posté par . En réponse au journal Désolé, la Quadrature, mais tu fais fausse route. Évalué à -10. Dernière modification le 03/12/16 à 11:35.

    De toutes les contributions que j'ai lues (je reconnais n'avoir lu que la moitié du gros volume de commentaires), celle qui m'a semblé la plus pertinente, par rapport au coeur du débat, est signée benoar<.

  • # Tags

    Posté par . En réponse au journal Lancement du projet Open Compute Toolchain. Évalué à -5.

    vejmarie<, je t'invite à prendre l'habitude de rajouter les mots-clé (les « tags ») qui conviennent par toi-même. Tu peux le faire à la création du journal ou postérieurement (en cliquant sur le lien « Tagger » qui t'ouvre un champ de saisie — il faut séparer les mots-clé par des espaces).

    Pour beaucoup de tes contributions sur le sujet, c'est pour l'instant moi qui ait fait le boulot, par respect pour ton travail et pour les lecteurs du site, et je ne le dis pas pour m'en honorer (quoique je suis content d'aider) mais pour préciser que ça ne me semble pas une bonne chose que l'accessibilité de tes journaux à postériori dépende de ma présence d'esprit.

    Par exemple, voici la page du mot-clé « opencompute ».

    Bien cordialement,

    SamWang, promoteur des audits et de la production de preuve formelle sur le code définissant le matériel libre (particulièrement la preuve formelle de conformité du code par rapport aux spécifications, voire d'autres preuves formelles comme la robustesse des spécifications relativement à des types d'attaques répertoriées) / promoteur de la fabrication (et distribution partiellement) supervisée pour éviter les chausse-trapes comme les portes dérobées matérielles furtives réalisées au niveau du dopage.

  • [^] # Re: aveu d'échec

    Posté par . En réponse au journal Désolé, la Quadrature, mais tu fais fausse route. Évalué à -10. Dernière modification le 02/12/16 à 19:37.

    La partie de mon commentaire à laquelle tu réagis porte sur la question du mal ressenti par le fœtus (sous-entendu en cas d'avortement), qu'il soit physique ou émotionnel, mais pas du mal au sens de la morale.

    Tu étends la question du mal au sens moral en posant la question de l'humanité du fœtus (et même déjà de son caractère vivant ou non, ajouterai-je) et je pense que tu fais bien, ça me semble légitime.

    Vois-tu, en réagissant à ton propos, je réalise que je n'apprécierais pas d'ôter la vie à un fœtus éléphant (à supposer que cela ne génère aucune souffrance chez ses parents éléphants ou à d'autres êtres vivants de l'environnement, comme l'aide-soignant d'un zoo qui aurait assisté la maman éléphant pendant sa grossesse), quand bien même saurais-je par la science que ce fœtus éléphant ne serait soumis à aucune souffrance potentielle (physique ou émotionnelle).

    Ainsi, plus que la question du respect du à un fœtus du fait de son humanité (en gestation, ou déjà actualisée, cela peut être discuté), je considère maintenant la question du respect du à un fœtus du fait de son caractère vivant.

    Pour éviter de tomber dans l'extrémisme, je tiens à préciser que tout en respectant les végétaux vivants (du moins j'ai l'impression de les respecter), parfois, je détache une feuille et je la mange, même. Serais-je jardinier qu'il m'arriverait peut-être de détacher des feuilles sans les manger, pour une question d'harmonie d'ensemble. La feuille n'est pas soumise à la souffrance physique (du moins d'après ce que je connais de la science dans son état actuel), je ne suis pas certain qu'elle ne soit pas sensible (je suis plutôt persuadé du contraire par tout un faisceau d'indices), de même que le végétal qui la porte. Elle est vivante avant que je la détache (et après, en combien de temps meurt-elle ?).

    Si l'avortement ne génère pas de souffrance physique ni émotionnelle au fœtus, alors je considère que c'est moins grave que si ça lui génère de la souffrance.

    Si j'adopte la perspective bouddhiste que j'ai longuement étudiée, retirer la vie à un fœtus c'est retirer une occasion extrêmement rare à une conscience d'obtenir le véhicule humain, le plus propice pour atteindre l'éveil ultime, c'est à dire un véhicule très précieux.

    Finalement, en toute chose, je préfère m'en remettre à la science, qu'elle soit bouddhiste ou non. Qu'il soit statué sur la souffrance physique, psychique et même spirituelle du fœtus et je pourrai dire si dans le binôme mère--fœtus l'un seul (la mère) ou les deux ont à y perdre dans l'avortement (y perdre de la paix physique, de la paix émotionnelle, voire du potentiel de cheminement vers l'éveil réputé être le bonheur ultime).

    Cette discussion peut sembler compliquée. Elle l'est. On ne joue pas avec la vie comme on joue avec un tabouret avant de s'assoir dessus pour pratiquer un avortement…

    Bonus : et c'est parce qu'on ne joue pas avec la vie que je ne lâcherai jamais mon travail de dévoilement des racines réelles du sionisme.

  • [^] # Re: aveu d'échec

    Posté par . En réponse au journal Désolé, la Quadrature, mais tu fais fausse route. Évalué à -8. Dernière modification le 02/12/16 à 17:47.

    Un mal personnel contre un mal partagé.

    L'avortement serait un mal personnel et la grossesse involontaire qui pourrait être dramatique serait (dans un tel cas) un mal partagé ?

    Je suis demandeur de publications scientifiques tendant à démontrer que le fœtus n'a pas encore de conscience pouvant l'amener à ressentir des sensations (douleur physique) ou des émotions (peur) en deçà de 12 semaines.

    Par ailleurs, j'ai connu un père dont la compagne a avorté, les deux étant d'accord, et les deux l'ont mal vécu (ils avaient en commun la sensation de malaise et de culpabilité).

  • [^] # Re: Fausse route

    Posté par . En réponse au journal Désolé, la Quadrature, mais tu fais fausse route. Évalué à -8.

    La symbiose et le parasitisme impliquent une relation entre deux espèces…

    • distinctes ?
    • de cons ?
    • trébuchantes, voire sonnantes  ?

    Je pense que c'est le premier choix, mais si c'est deux espèces de cons, est-ce à dire que la symbiose et le parasitisme sont interdits aux homosexuels mâles ?

    Là, je crois que je vais à nouveau --> []

  • [^] # Re: J'ai moinsé

    Posté par . En réponse au journal Désolé, la Quadrature, mais tu fais fausse route. Évalué à -2. Dernière modification le 02/12/16 à 17:10.

    *fais ou fasse?

    C'est peut-être entre les deux (faisse) ?

    Ok --> []

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -9. Dernière modification le 02/12/16 à 14:21.

    En regardant sur Tension_électrique, je lis que « voltage » est considéré dans l'article comme étant un anglicisme (et par là incorrect) et renvoie en notes de bas de page à plusieurs recherches menées en 2015 sur différents dictionnaires en ligne. Je considère que CNRTL qui est cité comme une preuve validant l'usage de voltage est une bien meilleure référence que les autres proposées, que je préfère ne pas citer tellement elles sont inférieures en qualité.

    Pendant mes études d'électronique, je privilégiais le mot tension, mais j'étais dans un cadre où seule cette acception avait cours, ou presque, menant à préciser quand l'usage était dans un autre champ de la connaissance (en utilisant, par exemple, l'expression tension mécanique).

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10. Dernière modification le 02/12/16 à 14:04.

    Correction : dans le commentaire parent, lorsque je fais référence au "commentaire parent", il s'agit en fait de mon commentaire précédent de même niveau (présentant le premier de la série des trois articles proposés par Misc<). Je pensais initialement publier le commentaire parent en tant que commentaire fils du précédent et je me suis ravisé pour laisser la place à des commentaires réagissant spécifiquement au précédent.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -8.

    Détrompe-toi, on dit tension ou voltage. Voici la preuve pour voltage : http://www.cnrtl.fr/definition/voltage
    J'ai choisi voltage pour éviter d'utiliser tension seul qui prête à confusion avec d'autres acceptions, notamment dans la mécanique. J'aurais pu utiliser tension électrique pour lever toute ambiguïté mais tant qu'à faire, j'ai choisi la version la plus courte.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -9. Dernière modification le 02/12/16 à 13:00.

    Vous avez été sage, voici la suite :

    2) Le deuxième article est titré "Reversing Stealthy Dopant-Level Circuits", ce qui peut se traduire par « rétro-ingénierie sur des circuits furtifs réalisés par dopage ».

    Il a été publié en 2014 (reçu le 27 Juin 2014 sur la plateforme d'archivage "Cryptology ePrint Archive", cf. source). Je note que l'article en lui-même n'est pas daté ; l'article le plus récent cité à la fin, en référence, date de 2014).

    Le titre est explicite dans la mesure où les circuits furtifs réalisés par dopage ont été présentés au commentaire parent.

    Voici la traduction (personnelle) du résumé de l'article en français :

    « Une détection réussie du circuit furtif réalisé par dopage (cheval de Troie), circuit proposé par Becker et ses coéquipiers au CHES 2013 [NdT : c'est une référence à l'article présenté dans le commentaire parent], est annoncée. Contrairement à une supposition faite par Becker et ses coéquipiers, les types de dopant dans les régions actives sont visibles sur les images obtenues soit par microscope à balayage électronique (dit SEM, pour "Scanning Electron Microscopy"), soit par faisceau concentré d'ions (dit FIB, pour "focused ion beam"). La mesure réussie est expliquée par une technique d'analyse de défaut sur circuit intégré LSI [NdT : cf. (1)] appelée contraste de voltage passif [NdT : de l'anglais "passive voltage contrast", ou PVC, cf. (2)]. Les expériences sont conduites en mesurant une puce spécialisée. La puce utilise le dispositif programmable de diffusion : une technique empêchant la rétro-ingénierie via le même principe que celui utilisé dans le cheval de Troie furtif réalisé au niveau du dopage. De la puce sont retirées les couches supérieures jusqu'à la couche de contact [NdT : cf. (3)] et des images sont prises avec un microscope optique d'une part, SEM d'autre part, et enfin FIB. Sur les images SEM, on peut distinguer quatre combinaisons possibles de dopants [NdT : le résumé les nomme, sans détailler, p+/n-well, p+/p-well, n+/n-well et n+/p-well]. Une détection partielle mais suffisante est réalisée par FIB. Bien que les circuits furtifs réalisés au niveau du dopage soient visibles, ils rendent potentiellement la détection plus difficile. C'est parce que la couche de contact devrait être mesurée. Nous montrons que rendre en images la couche de contact est au moins 16 fois plus coûteux en nombre d'images que pour une couche métal ».

    (1) LSI signifie "large-scale integration" et définit une échelle d'intégration sortie en 1971, correspondant à 500 à 20.000 transistors par boitier, soit 100 à 9.999 portes logiques — cf. source.

    (2) Dans la section 3.2 du document, la technique PVC est présentée. Elle a été développée dans les années 1990. Elle est maintenant largement utilisée.

    (3) la couche de contact fait l'interface entre le substrat de silicium (dopé par endroits) et les multiples couches de conducteurs métalliques qui sont au-dessus. Vous pourrez vous reporter au schéma présenté à la Fig. 1 en tête de la page 3 du document pour constater l'empilement des couches.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -6.

    Merci Misc<. Ce que tu présentes là est important.

    On va expliciter pour les moules non encore farcies de portes dérobées matérielles furtives réalisées au niveau du dopage ! C'est compliqué ? Je t'explique.

    Il y a trois articles présentés, tous en anglais. Dans ce commentaire, je vais traiter du premier. C'est pour ça qu'il n'y a qu'un "1)" et pas de suite en "2)" ni en "3)" à ce stade. Si vous êtes tous sages et si les augures sont propices, je livrerai la suite à la prochaine lune souriante. Si quelqu'un d'autre veut rédiger la suite avec le même niveau d'exigence, qu'il s'exécute sans tarder, car c'est propice pour la communauté des moules, en terme de pré-formation… pour pouvoir opérer une surveillance du processus de fabrication à base de balayage par microscopie électronique ou par rayons ciblés d'ions (mais là, nous anticipons le deuxième article) :)

    1) le premier est titré "Stealthy dopant-level hardware trojans", ce qui peut se traduire par « Cheval de Troie matériel furtif réalisé au niveau du dopage ».

    Il a été rédigé postérieurement à février 2013 (l'article en lui-même n'est pas daté mais l'article le plus récent cité à la fin, en référence, date de février 2013).

    a) Pour expliciter à partir du titre, il y est question de cheval de Troie, au niveau du matériel, mais sans ajout de circuits (pas de transistors supplémentaires gravés dans le silicium, le résumé de l'article décrit cela en disant que c'est "sous le niveau des portes logiques"), rendant la malveillance furtive (du moins ça ne se voit pas au microscope optique) et ça se passe en modifiant le dopage des transistors (en changeant la polarité des dopants au sein des transistors existants), pour réaliser des fonctions non prévues par le concepteur du schéma de gravure légitime du circuit intégré.

    b) J'explicite la question du dopage :

    • bien qu'il y ait différentes variantes de transistors (cf. Transistor), prenons simplement le cas classique d'un transistor bipolaire (cf. Transistor_bipolaire) pour présenter la problématique.

    • le Wikipédia francophone (dans son état actuel) nous dit — dans l'article sur les transistors — que ce dernier est « un dispositif électronique à base de semi-conducteur dont le principe de fonctionnement est basé sur deux jonctions PN (cf. Jonction_P-N), l'une en direct et l'autre en inverse ».

    • bon, pour t'éviter de cliquer sur chaque lien, et parce que les articles ne sont que des ébauches pour l'instant, il s'agit en fait de trois couches de matériau semi-conducteur (par exemple du silicium), dopées chacune (le dopage, c'est un apport d'un matériaux tiers qui est diffusé dans la couche de silicium à la fabrication), soit en positif (noté P, du fait que le matériau diffusé dans le silicium n'est pas électroniquement neutre mais chargé positivement, parce qu'il comporte une déficience d'électrons, c'est à dire un surplus de "trous"), soit en négatif (noté N, du fait que le matériau diffusé dans le silicium est chargé négativement, parce qu'il comporte un surplus d'électrons).

    • le Wikipédia francophone (dans son état actuel) nous dit aussi — toujours dans l'article sur les transistors — qu' « un transistor bipolaire se compose de deux parties de substrat semiconducteur dopées identiquement (P ou N) séparées par une mince tranche de semiconducteur dopée inversement ; on a ainsi deux types : N-P-N et P-N-P. »

    Voilà présenté ce qu'est le dopage, une jonction PN (c'est à dire une diode, en fait) et le transistor bipolaire classique.

    c) voici la traduction (personnelle) du résumé de l'article en français :

    « Dans les années récentes, les chevaux de Troie matériels ont attiré l'attention des gouvernements et de l'industrie aussi bien que de la communauté scientifique. Une des préoccupations principales est que les circuits intégrés, par exemple, dans le domaine militaire ou des applications d'infrastructure critique, pourraient être manipulés malicieusement pendant le processus de fabrication, qui a souvent lieu à l'étranger. Cependant, puisqu'il n'y a pas encore eu de cheval de Troie matériel qui ait été découvert jusqu'alors, nous en savons peu sur l'allure que prendrait un tel cheval de Troie et à quel point il serait difficile en pratique d'en implémenter un.
    Dans cet article, nous proposons une approche extrêmement furtive pour implémenter des chevaux de Troie matériels sous le niveau des portes logiques et nous évaluons leur impact sur la sécurité du dispositif cible. Au lieu d'ajouter des circuits additionnels au schéma de conception ciblé, nous insérons nos chevaux de Troie matériels en changeant la polarité des dopants aux transistors existants. Puisque le circuit modifié apparaît légitime sur toutes les couches gravées (incluant métal et silicium), notre famille de chevaux de Troie est résistante à la plupart des techniques de détection, incluant l'inspection optique à une granularité fine et la vérification pour détecter des "circuits dorés" [NdT : je ne sais pas traduire autrement "Golden chips" (qui est entre guillemets dans le texte) - j'observe que c'est une marque de frites, semble-t-il]. Nous démontrons l'efficacité de notre approche en insérant des chevaux de Troie dans deux schémas de conception — un post-traitement numérique dérivé du schéma d'Intel, dit RNG sécurisé de façon cryptographique, utilisé dans les processeurs Ivy Bridge, et une implémentation SBox résistante à [NDT : une attaque par ?] canal latéral — et en explorant leur détectabilité et leurs effets sur la sécurité ».

    d) épilogue temporaire :

    Alors, la moule, heureuse ? Tu as appris quelque chose ? Tant mieux, car nous sommes là pour nous accompagner mutuellement jusqu'à prendre possession de ce monde. Notre sort n'est pas de finir en bouchées accompagnées de "golden chips", mais de reprendre le contrôle sur le matériel, d'obtenir du matériel de confiance de notre point de vue, pas de celui des industriels aux ordres des financiers, de l'oligarchie, ou d'une quelconque coterie ;)

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10.

    Pour faire de la preuve formelle sur les schémas des circuits intégrés numériques, il faut les schémas. File-moi les schémas (ou mieux, le code Bluespec (1) et la licence du soft à 100.000 dollars) des processeurs AMD, Intel, ou ARM, et on en reparle. Et s'il te plait, fais-le légalement (bonne chance), je n'ai pas envie d'avoir les chinois du FBI sur le dos, j'en ai assez avec le Mossad et les sayanim pour avoir seulement participé au hacking des racines kabbalistes (2) du sionisme.

    (1) Bluespec est un langage de description matérielle qui nécessite une phase d'apprentissage non négligeable notamment sur la gestion des preuves formelles, cf. par exemple ce journal.

    (2) J'ai relayé par ici ce que révèle l'historien Youssef Hindi, à savoir l'influence néfaste de la kabbale dans le judaïsme, kabbale qui l'a largement perverti de l'intérieur et constitue les racines historiques du sionisme, autour du 13e siècle et au-delà, menant à un projet messianique apocalyptique hégémonique dans lequel il est conseillé d'inverser les valeurs et d'ainsi hâter la venue du Messie. Ah, désolé, là non plus je ne suis pas complotiste, c'est documenté et sourcé.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10. Dernière modification le 30/11/16 à 11:24.

    Microsoft Mangement Engine

    Correction : Intel Mangement Engine, bien sûr. Je n'aime vraiment pas Microsoft… C'est à un tel point que ça me joue des tours !

    Pour ceux qui découvriraient ça, voici un lien.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10.

    Du fait que je prends l'essentiel de mes informations sur Linuxfr, tu as certainement déjà découvert les gens et les projets intéressants que je pourrais citer. Jusqu'ici, je pensais notamment à Martoni<, mais je commence à me poser des questions ;)

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10.

    Où vois-tu du "complotisme" dans mes propos, Martoni ? Tu as confiance, toi, par exemple, dans le Microsoft Mangement Engine ?

    Bon, admettons que je sois complotiste en considérant le risque d'implantation de porte dérobée au niveau matériel (LOL poutré), j'ajouterai ceci :

    À quand les captchas sur les commentaires linuxfr ?
    Histoire d'éviter ce genre de robot pipotron-anti-complotiste.

  • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10. Dernière modification le 30/11/16 à 09:16.

    Qui désigne ces hackers ?

    • ça peut être moi qui suis quasi omniscient. Que je sorte ? Déjà ? Snif…
    • ça peut être une coterie comme les franc-maçons, comme ça on maximise le potentiel d'échec.
    • entre les deux, ça peut être tous les terriens reconnus par leurs pairs comme ayant porté un intérêt un peu soutenu sur le sujet du matériel libre.

    Je développe sur le pouce la troisième hypothèse qui me semble plus raisonnable, en assumant le fait que le protocole nécessite d'être muri :

    a) les terriens désignent leurs semblables reconnus comme ayant porté un intérêt un peu soutenu sur le sujet du matériel libre, intérêt identifiable idéalement par des sources (des commentaires sur le net, par exemple). Voici un protocole envisageable : chacun des terriens peut désigner jusqu'à 10 personnes et fournit pour chacune quelques sources pour justifier le choix, si possible. On pourra envisager d'étendre les critères à la simple implication dans une activité professionnelle sur le sujet de la fabrication du matériel (notamment la gravure des circuits intégrés), mais il faudra prévoir des garde-fous comme un quota de témoignages de probité morale…

    b) dans la liste de noms obtenus avec un nombre de citations défini pour chacun, on pourra appliquer différents protocoles pour s'assurer de leur compétence et de leur intégrité. Une possibilité est de garder uniquement les 80 centiles au centre du panel (écartant les 10 centiles les moins nommés, pour écarter ceux probablement moins compétents, à l'arrache, et les 10 centiles les plus nommés, pour écarter les biais liés à la sur-médiatisation et l'exposition aux pressions que cela peut impliquer, à l'arrache).

    Parmis ceux nommés et retenus à ce stade, on identifiera ceux qui acceptent de s'impliquer dans la suite du protocole de désignation et ceux qui acceptent l'éventualité de s'impliquer comme assesseur technique après tirage au sort.

    Pour compenser les défaillances de la sélection des 80 centiles du milieu, on pourra accorder un repêchage de façon ciblée et justifiée (des sources), qui puisse être opéré par la majorité absolue (ou un autre mode de votation) des 80 centiles du milieu.

    La compétence des futurs tirés au sort devra être évaluée pour dépasser un seuil minimum, avec des critères choisis par l'ensemble des hackers retenus à ce stade, le choix des critères étant réalisé par vote (à la majorité absolue, par exemple, ou par vote plus subtil comme le vote de valeur — cf. Vote_par_valeurs et ).

    c) Le tirage au sort a lieu parmi ceux retenus. La compétence de ceux tirés au sort est évaluée selon les critères définis. Ceux qui n'atteignent pas le seuil de compétence ne sont finalement pas retenus et un nouveau tirage au sort a lieu pour atteindre le nombre d'assesseurs techniques nécessaires. Dans ce cas, la compétence des nouveaux tirés au sort est évaluée, et s'il y en a qui ne sont pas qualifiés, on reprend le processus de tirage au sort, et ainsi de suite.

    d) pour les hackers nommés puis tirés au sort et reconnus compétents au-dessus d'un certain seuil, une formation complémentaire a lieu, que ce soit pour acquérir quelques bases manquantes ou que ce soit plus spécifiquement pour opérer la supervision de la fabrication.

  • # Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. Évalué à -10.

    Le projet présenté ici me semble très intéressant. Cependant, il convient de noter que des portes dérobées peuvent toujours se glisser :

    • dans la conception, surtout tant qu'il n'y a pas de preuve formelle sur les schémas de conception (conformité des schémas avec les spécifications, ce qui revient à de la preuve formelle sur le code Chisel/Verilog). Les spécifications étant disponibles, l'audit et la preuve formelle peuvent être réalisés à postériori ;
    • particulièrement à la fabrication, tant qu'elle n'est pas opérée ou au moins supervisée par une communauté de confiance ;
    • pendant la distribution du matériel, par substitution malveillante.

    Pour aller plus loin, je propose la lecture de ce commentaire (et des commentaires source, dans lesquels je propose des pistes comme, entre autres et à minima, la supervision de la fabrication par une équipe d'assesseurs techniques tirés au sort parmi la communauté de hackers compétents, supervision rendue possible contractuellement avec l'industriel).

    Même en supposant la conception non malveillante, je considère qu'il n'est pas sérieux de faire confiance aveuglément à un fabricant sans supervision approfondie, du fait qu'il est lié par des intérêts financiers à des donneurs d'ordre, donc potentiellement à des pressions d'ordre politique et géostratégique. La distribution du matériel est également une phase critique.

  • [^] # Re: Nuance

    Posté par . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à -7. Dernière modification le 28/11/16 à 17:05.

    [remarque sur la typographie - pas sur le fond]

    bluestorm< (alias gasche), j'apprécie grandement les efforts pédagogiques que tu fais pour rendre accessible l'état de la recherche. Merci. Concernant la forme, je te propose quelques conseils de typographe amateur :

    • le tiret long (ou tiret quadratin) que tu utilises à bon escient nécessite un espace avant et après. Pour l'obtenir, une façon de faire sur Linuxfr est de placer deux espaces puis deux tirets puis à nouveau deux espaces — ceci permettant de produire ce que tu vois ici — ce que j'ai découvert par l'expérience.
    • pour les signes de ponctuation point virgule et deux points, il convient de placer un espace avant (idéalement c'est un espace insécable) et après, au moins en français. Il me semble que tu utilises l'usage qui a cours en anglais, sans doute par la mauvaise influence de tes lectures ;) Je précise à toute fin utile que, de même, si en anglais on ne met pas d'espace avant le point d'interrogation ni le point d'exclamation, il convient d'en mettre un en français.

    Bien cordialement,
    SamWang, amateur de typographie à ses heures.

  • [^] # Re: Verified toolchain

    Posté par . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à -6.

    Je rappelle que la preuve formelle de code pour la conception matérielle est un atout important dans la production de matériel libre :

    Je me cite :

    la libération [des spécifications matérielles] amènera la capacité d'audit communautaire et la capacité de répliquer l'expérience en produisant des versions alternatives et dérivées, or la diversité importe pour des raisons de sécurité.

    Notons que dans ces conditions, des failles de sécurité dans la conception sont plus facilement identifiables par des groupes malveillants qui garderaient pour eux leurs découvertes, de manière à les exploiter dans le secret. Cette question aura vocation a être traitée par de la preuve formelle de programme couvrant la plus grande surface possible du code (l'architecture des portes logiques peut être considérée comme étant du code).

    [source]

    Plus loin, dans le même fil de discussion, j'abordais le problème associé du coût de la preuve formelle :

    si le coût de conception pourrait être réduit du fait de l'activité pour partie bénévole et s'appuyant sur un existant déjà sous licence libre, par contre l'investissement intellectuel devrait être plus important que l'usage courant, pour tendre à produire un cadre de preuves formelles de code. Ensuite, le coût lié à la supervision de la production et pour partie de la distribution (je ne rentre pas dans le détail) est nouveau par rapport aux usages et représente un coût.

    [source]